proposition: Lemma hom_mxsemisimple_iso I P U W f : let V := (\sum_(i : I | P i) W i)%MS in mxsimple U -> (forall i, P i -> W i != 0 -> mxsimple (W i)) -> (V <= dom_hom_mx f)%MS -> (U <= V *m f)%MS -> {i | P i & mx_iso (W i) U}.
proof: Proof. move=> V simU simW homVf sUVf; have [modU nzU _] := simU. have ssimVf: mxsemisimple (V *m f). exact: hom_mxsemisimple (intro_mxsemisimple (eqmx_refl V) simW) homVf. have [U' modU' defVf] := mxsemisimple_reducible ssimVf modU sUVf. move/mxdirect_addsP=> dxUU'; pose p := f *m proj_mx U U'. case: (pickP (fun i => P i && (W i *m p != 0))) => [i /andP[Pi nzWip] | no_i]. have sWiV: (W i <= V)%MS by rewrite (sumsmx_sup i). have sWipU: (W i *m p <= U)%MS by rewrite mulmxA proj_mx_sub. exists i => //; apply: (mx_Schur_iso (simW i Pi _) simU _ sWipU nzWip). by apply: contraNneq nzWip => ->; rewrite mul0mx. apply: (submx_trans sWiV); apply/hom_mxP=> x Gx. by rewrite mulmxA [_ *m p]mulmxA 2?(hom_mxP _) -?defVf ?proj_mx_hom. case/negP: nzU; rewrite -submx0 -[U](proj_mx_id dxUU') //. rewrite (submx_trans (submxMr _ sUVf)) // -mulmxA -/p sumsmxMr. by apply/sumsmx_subP=> i Pi; move/negbT: (no_i i); rewrite Pi negbK submx0. 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)