proposition: Lemma mxsemisimpleS U V : mxmodule U -> (U <= V)%MS -> mxsemisimple V -> mxsemisimple U.
proof: Proof. move=> modU sUV ssimV. have [W modW defUW dxUW]:= mxsemisimple_reducible ssimV modU sUV. move/mxdirect_addsP: dxUW => dxUW. have defU : (V *m proj_mx U W :=: U)%MS. by apply/eqmxP; rewrite proj_mx_sub -{1}[U](proj_mx_id dxUW) ?submxMr. apply: eqmx_semisimple defU _; apply: hom_mxsemisimple ssimV _. by rewrite -defUW proj_mx_hom. 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)