proposition: Lemma mx_rsim_in_submod U V (modU : mG U) (modV : mG V) : let U' := <<in_submod V U>>%MS in (U <= V)%MS -> exists modU' : mxmodule (sr modV) U', mx_rsim (sr modU) (sr modU').
proof: Proof. move=> U' sUV; have modU': mxmodule (sr modV) U'. by rewrite (eqmx_module _ (genmxE _)) in_submod_module. have rankU': \rank U = \rank U' by rewrite genmxE mxrank_in_submod. pose v1 := val_submod 1%:M; pose U1 := v1 _ U. have sU1V: (U1 <= V)%MS by rewrite val_submod1. have sU1U': (in_submod V U1 <= U')%MS by rewrite genmxE submxMr ?val_submod1. exists modU', (in_submod U' (in_submod V U1)) => // [|x Gx]. apply/row_freeP; exists (v1 _ _ *m v1 _ _ *m in_submod U 1%:M). rewrite mulmxA [X in X *m _]mulmxA -in_submodE. by rewrite -!val_submodE !in_submodK ?val_submodK. rewrite -!in_submodJ // -(val_submodJ modU) // mul1mx. by rewrite 2!{1}in_submodE mulmxA (mulmxA _ U1) -val_submodE -!in_submodE. 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)