proposition: Lemma dec_mx_reducible_semisimple U : mxmodule rG U -> mx_completely_reducible rG U -> mxsemisimple rG U.
proof: Proof. have [m] := ubnP (\rank U); elim: m U => // m IHm U leUm modU redU. have [U0 | nzU] := eqVneq U 0. have{} U0: (\sum_(i < 0) 0 :=: U)%MS by rewrite big_ord0 U0. by apply: (intro_mxsemisimple U0); case. have [V simV sVU] := dec_mxsimple_exists modU nzU; have [modV nzV _] := simV. have [W modW defVW dxVW] := redU V modV sVU. have [||I W_ /= simW defW _] := IHm W _ modW. - rewrite ltnS in leUm; apply: leq_trans leUm. by rewrite -defVW (mxdirectP dxVW) /= -add1n leq_add2r lt0n mxrank_eq0. - by apply: mx_reducibleS redU; rewrite // -defVW addsmxSr. suffices defU: (\sum_i oapp W_ V i :=: U)%MS. by apply: (intro_mxsemisimple defU) => [] [|i] //=. apply: eqmx_trans defVW; rewrite (bigD1 None) //=; apply/eqmxP. have [i0 _ | I0] := pickP I. by rewrite (reindex some) ?addsmxS ?defW //; exists (odflt i0) => //; case. rewrite big_pred0 //; last by case=> // /I0. by rewrite !addsmxS ?sub0mx // -defW big_pred0. 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)