proposition: Lemma mx_rsim_dsum (I : finType) (P : pred I) U rU (W : 'M_n) (modU : forall i, mxmodule rG (U i)) (modW : mxmodule rG W) : let S := (\sum_(i | P i) U i)%MS in (S :=: W)%MS -> mxdirect S -> (forall i, mx_rsim (submod_repr (modU i)) (rU i : representation)) -> mx_rsim (submod_repr modW) (\big[dadd_grepr/grepr0]_(i | P i) rU i).
proof: Proof. move=> /= defW dxW rsimU. rewrite mxdirectE /= -!(big_filter _ P) in dxW defW *. elim: {P}(filter P _) => [|i e IHe] in W modW dxW defW *. rewrite !big_nil /= in defW *. by exists 0 => [||? _]; rewrite ?mul0mx ?mulmx0 // /row_free -defW !mxrank0. rewrite !big_cons /= in dxW defW *. rewrite 2!(big_nth i) !big_mkord /= in IHe dxW defW. set Wi := (\sum_i _)%MS in defW dxW IHe. rewrite -mxdirectE mxdirect_addsE !mxdirectE eqxx /= -/Wi in dxW. have modWi: mxmodule rG Wi by apply: sumsmx_module. case/andP: dxW; move/(IHe Wi modWi) {IHe}; move/(_ (eqmx_refl _))=> rsimWi. by move/eqP; move/mxdirect_addsP=> dxUiWi; apply: mx_rsim_dadd (rsimU i) rsimWi. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype choice ssrnat seq) mathcomp(path div fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset gproduct fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup nilpotent sylow) mathcomp(abelian matrix mxalgebra mxpoly mxrepresentation) mathcomp(vector ssrnum algC classfun archimedean)