proposition: Lemma intro_mxsemisimple (I : Type) r (P : pred I) W V : (\sum_(i <- r | P i) W i :=: V)%MS -> (forall i, P i -> W i != 0 -> mxsimple (W i)) -> mxsemisimple V.
proof: Proof. move=> defV simW; pose W_0 := [pred i | W i == 0]. have [-> | nzV] := eqVneq V 0; first exact: mxsemisimple0. case def_r: r => [| i0 r'] => [|{r' def_r}]. by rewrite -mxrank_eq0 -defV def_r big_nil mxrank0 in nzV. move: defV; rewrite (bigID W_0) /= addsmxC -big_filter !(big_nth i0) !big_mkord. rewrite addsmxC big1 ?adds0mx_id => [|i /andP[_ /eqP] //]. set tI := 'I_(_); set r_ := nth _ _ => defV. have{simW} simWr (i : tI) : mxsimple (W (r_ i)). case: i => m /=; set Pr := fun i => _ => lt_m_r /=. suffices: (Pr (r_ m)) by case/andP; apply: simW. apply: all_nthP m lt_m_r; apply/all_filterP. by rewrite -filter_predI; apply: eq_filter => i; rewrite /= andbb. have [J []] := sum_mxsimple_direct_sub simWr defV. case: (set_0Vmem J) => [-> V0 | [j0 Jj0]]. by rewrite -mxrank_eq0 -V0 big_set0 mxrank0 in nzV. pose K := {j | j \in J}; pose k0 : K := Sub j0 Jj0. have bij_KJ: {on J, bijective (sval : K -> _)}. by exists (insubd k0) => [k _ | j Jj]; rewrite ?valKd ?insubdK. have J_K (k : K) : sval k \in J by apply: valP k. rewrite mxdirectE /= !(reindex _ bij_KJ) !(eq_bigl _ _ J_K) -mxdirectE /= -/tI. exact: MxSemisimple. 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)