proposition: Lemma morphimGI G A : 'ker f \subset G -> f @* (G :&: A) = f @* G :&: f @* A.
proof: Proof. move=> sKG; apply/eqP; rewrite eqEsubset morphimI setIC. apply/subsetP=> _ /setIP[/morphimP[x Dx Ax ->] /morphimP[z Dz Gz]]. case/ker_rcoset=> {Dz}// y Ky def_x. have{z Gz y Ky def_x} Gx: x \in G by rewrite def_x groupMl // (subsetP sKG). by rewrite imset_f ?inE // Dx Gx Ax. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)