proposition: Lemma sum_mxsimple_direct_compl m I W (U : 'M_(m, n)) : let V := (\sum_(i : I) W i)%MS in (forall i : I, mxsimple (W i)) -> mxmodule U -> (U <= V)%MS -> {J : {set I} | let S := U + \sum_(i in J) W i in S :=: V /\ mxdirect S}%MS.
proof: Proof. move=> V simW modU sUV; pose V_ (J : {set I}) := (\sum_(i in J) W i)%MS. pose dxU (J : {set I}) := mxdirect (U + V_ J). have [J maxJ]: {J | maxset dxU J}; last case/maxsetP: maxJ => dxUVJ maxJ. apply: ex_maxset; exists set0. by rewrite /dxU mxdirectE /V_ /= !big_set0 addn0 addsmx0 /=. have modWJ: mxmodule (V_ J) by apply: sumsmx_module => i _; case: (simW i). exists J; split=> //; apply/eqmxP; rewrite addsmx_sub sUV; apply/andP; split. by apply/sumsmx_subP=> i Ji; rewrite (sumsmx_sup i). rewrite -/(V_ J); apply/sumsmx_subP=> i _. case Ji: (i \in J). by apply: submx_trans (addsmxSr _ _); apply: (sumsmx_sup i). have [modWi nzWi simWi] := simW i. rewrite (sameP capmx_idPl eqmxP) simWi ?capmxSl ?capmx_module ?addsmx_module //. apply: contraFT (Ji); rewrite negbK => dxWiUVJ. rewrite -(maxJ (i |: J)) ?setU11 ?subsetUr // /dxU. rewrite mxdirectE /= !big_setU1 ?Ji //=. rewrite addnCA addsmxA (addsmxC U) -addsmxA -mxdirectE /=. by rewrite mxdirect_addsE /= mxdirect_trivial -/(dxU _) dxUVJ. 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)