proposition: Lemma hom_mxP m f (W : 'M_(m, n)) : reflect (forall x, x \in G -> W *m rG x *m f = W *m f *m rG x) (W <= dom_hom_mx f)%MS.
proof: Proof. apply: (iffP row_subP) => [cGf x Gx | cGf i]. apply/row_matrixP=> i; apply/eqP; rewrite -subr_eq0 -!mulmxA -!linearB /=. have:= sub_kermxP (cGf i); rewrite mul_rV_lin1 /=. move/(canRL mxvecK)/row_matrixP/(_ (enum_rank_in Gx x))/eqP; rewrite !linear0. by rewrite !row_mul rowK mul_vec_lin /= mul_vec_lin_row enum_rankK_in. apply/sub_kermxP; rewrite mul_rV_lin1 /=; apply: (canLR vec_mxK). apply/row_matrixP=> j; rewrite !row_mul rowK mul_vec_lin /= mul_vec_lin_row. by rewrite -!row_mul mulmxBr !mulmxA cGf ?enum_valP // subrr !linear0. 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)