proposition: Lemma morphimMl A B : A \subset D -> f @* (A * B) = f @* A * f @* B.
proof: Proof. move=> sAD; rewrite /morphim setIC -group_modl // (setIidPr sAD). apply/setP=> fxy; apply/idP/idP. case/imsetP=> _ /imset2P[x y Ax /setIP[Dy By] ->] ->{fxy}. by rewrite morphM // (subsetP sAD, imset2_f) // imset_f // inE By. case/imset2P=> _ _ /imsetP[x Ax ->] /morphimP[y Dy By ->] ->{fxy}. by rewrite -morphM // (subsetP sAD, imset_f) // mem_mulg // inE By. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)