proposition: Lemma capmx_subSocle m (M : 'M_(m, n)) : mxmodule M -> (M :&: S :=: \sum_(W : sG | P W) (M :&: W))%MS.
proof: Proof. move=> modM; apply/eqmxP/andP; split; last first. by apply/sumsmx_subP=> W P_W; rewrite capmxS // (sumsmx_sup W). have modMS: mxmodule (M :&: S)%MS by rewrite capmx_module ?subSocle_module. have [J /= U simU defMS _] := mxsemisimpleS modMS (capmxSr M S) ssimS. rewrite -defMS; apply/sumsmx_subP=> j _. have [sUjV sUjS]: (U j <= M /\ U j <= S)%MS. by apply/andP; rewrite -sub_capmx -defMS (sumsmx_sup j). have [W P_W isoWU] := subSocle_iso (simU j) sUjS. rewrite (sumsmx_sup W) // sub_capmx sUjV mx_iso_component //. exact: socle_simple. 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)