proposition: Lemma subSocle_iso M : mxsimple M -> (M <= S)%MS -> {W : sG | P W & mx_iso (socle_base W) M}.
proof: Proof. move=> simM sMS; have [modM nzM _] := simM. have [V /= modV defMV] := mxsemisimple_reducible ssimS modM sMS. move/mxdirect_addsP=> dxMV; pose p := proj_mx M V; pose Sp (W : sG) := W *m p. case: (pickP [pred i | P i & Sp i != 0]) => [/= W | Sp0]; last first. case/negP: nzM; rewrite -submx0 -[M](proj_mx_id dxMV) //. rewrite (submx_trans (submxMr _ sMS)) // sumsmxMr big1 // => W P_W. by apply/eqP; move/negbT: (Sp0 W); rewrite /= P_W negbK. rewrite {}/Sp /= => /andP[P_W nzSp]; exists W => //. have homWp: (W <= dom_hom_mx p)%MS. apply: submx_trans (proj_mx_hom dxMV modM modV). by rewrite defMV (sumsmx_sup W). have simWP := socle_simple W; apply: hom_component_mx_iso (homWp) _ => //. by rewrite (mx_Schur_onto _ simM) ?proj_mx_sub ?component_mx_module. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)