proposition: Lemma mx_rsim_dadd (U V W : 'M_n) (rU rV : representation) (modU : mxmodule rG U) (modV : mxmodule rG V) (modW : mxmodule rG W) : (U + V :=: W)%MS -> mxdirect (U + V) -> mx_rsim (submod_repr modU) rU -> mx_rsim (submod_repr modV) rV -> mx_rsim (submod_repr modW) (dadd_grepr rU rV).
proof: Proof. case: rU; case: rV=> nV rV nU rU defW dxUV /=. have tiUV := mxdirect_addsP dxUV. move=> [fU def_nU]; rewrite -{nU}def_nU in rU fU * => inv_fU hom_fU. move=> [fV def_nV]; rewrite -{nV}def_nV in rV fV * => inv_fV hom_fV. pose pU := in_submod U (proj_mx U V) *m fU. pose pV := in_submod V (proj_mx V U) *m fV. exists (val_submod 1%:M *m row_mx pU pV) => [||g Gg]. - by rewrite -defW (mxdirectP dxUV). - apply/row_freeP. pose pU' := invmx fU *m val_submod 1%:M. pose pV' := invmx fV *m val_submod 1%:M. exists (in_submod _ (col_mx pU' pV')). rewrite in_submodE mulmxA -in_submodE -mulmxA mul_row_col mulmxDr. rewrite -[pU *m _]mulmxA -[pV *m _]mulmxA !mulKVmx -?row_free_unit //. rewrite addrC (in_submodE V) 2![val_submod 1%:M *m _]mulmxA -in_submodE. rewrite addrC (in_submodE U) 2![val_submod 1%:M *m _ in X in X + _]mulmxA. rewrite -in_submodE -!val_submodE !in_submodK ?proj_mx_sub //. by rewrite add_proj_mx ?val_submodK // val_submod1 defW. rewrite mulmxA -val_submodE -[submod_repr _ g]mul1mx val_submodJ //. rewrite -(mulmxA _ (rG g)) mul_mx_row -[in RHS]mulmxA mul_row_block. rewrite !mulmx0 addr0 add0r !mul_mx_row. set W' := val_submod 1%:M; congr (row_mx _ _). rewrite 3!mulmxA in_submodE mulmxA. have hom_pU: (W' <= dom_hom_mx rG (proj_mx U V))%MS. by rewrite val_submod1 -defW proj_mx_hom. rewrite (hom_mxP hom_pU) // -in_submodE (in_submodJ modU) ?proj_mx_sub //. rewrite -(mulmxA _ _ fU) hom_fU // in_submodE -2!(mulmxA W') -in_submodE. by rewrite -mulmxA (mulmxA _ fU). rewrite 3!mulmxA in_submodE mulmxA. have hom_pV: (W' <= dom_hom_mx rG (proj_mx V U))%MS. by rewrite val_submod1 -defW addsmxC proj_mx_hom // capmxC. rewrite (hom_mxP hom_pV) // -in_submodE (in_submodJ modV) ?proj_mx_sub //. rewrite -(mulmxA _ _ fV) hom_fV // in_submodE -2!(mulmxA W') -in_submodE. by rewrite -mulmxA (mulmxA _ fV). 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)