proposition: Lemma morphim_pprodm A B : A \subset H -> B \subset K -> f @* (A * B) = fH @* A * fK @* B.
proof: Proof. move=> sAH sBK; rewrite [f @* _]morphimEsub /=; last first. by rewrite norm_joinEr // mulgSS. apply/setP=> y; apply/imsetP/idP=> [[_ /mulsgP[x a Ax Ba ->] ->{y}] |]. have Hx := subsetP sAH x Ax; have Ka := subsetP sBK a Ba. by rewrite pprodmE // imset2_f ?mem_morphim. case/mulsgP=> _ _ /morphimP[x Hx Ax ->] /morphimP[a Ka Ba ->] ->{y}. by exists (x * a); rewrite ?mem_mulg ?pprodmE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)