proposition: Lemma mx_second_rsim U V (modU : modG U) (modV : modG V) : let modI := capmx_module modU modV in let modA := addsmx_module modU modV in mx_rsim (section_repr modI modU) (section_repr modV modA).
proof: Proof. move=> modI modA; set nI := {1}(\rank _). have sIU := capmxSl U V; have sVA := addsmxSr U V. pose valI := val_factmod (val_submod (1%:M : 'M_nI)). have UvalI: (valI <= U)%MS. rewrite -(addsmx_idPr sIU) (submx_trans _ (proj_factmodS _ _)) //. by rewrite submxMr // val_submod1 genmxE. exists (valI *m in_factmod _ 1%:M *m in_submod _ 1%:M) => [||x Gx]. - apply: (@addIn (\rank (U :&: V) + \rank V)%N); rewrite genmxE addnA addnCA. rewrite /nI genmxE !{1}mxrank_in_factmod 2?(addsmx_idPr _) //. by rewrite -mxrank_sum_cap addnC. - rewrite -kermx_eq0; apply/rowV0P=> u; rewrite (sameP sub_kermxP eqP). rewrite mulmxA -in_submodE mulmxA -in_factmodE -(inj_eq val_submod_inj). rewrite linear0 in_submodK ?in_factmod_eq0 => [Vvu|]; last first. by rewrite genmxE addsmxC in_factmod_addsK submxMr // mulmx_sub. apply: val_submod_inj; apply/eqP; rewrite linear0 -[val_submod u]val_factmodK. rewrite val_submodE val_factmodE -mulmxA -val_factmodE -/valI. by rewrite in_factmod_eq0 sub_capmx mulmx_sub. symmetry; rewrite -{1}in_submodE -{1}in_submodJ; last first. by rewrite genmxE addsmxC in_factmod_addsK -in_factmodE submxMr. rewrite -{1}in_factmodE -{1}in_factmodJ // mulmxA in_submodE; congr (_ *m _). apply/eqP; rewrite mulmxA -in_factmodE -subr_eq0 -linearB in_factmod_eq0. apply: submx_trans (capmxSr U V); rewrite -in_factmod_eq0 linearB /=. rewrite subr_eq0 {1}(in_factmodJ modI) // val_factmodK eq_sym. rewrite /valI val_factmodE mulmxA -val_factmodE val_factmodK. by rewrite -[submod_mx _ _]mul1mx -val_submodE val_submodJ. 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)