proposition: Lemma morphim_Zgroup G : Zgroup G -> Zgroup (f @* G).
proof: Proof. move=> zgG; wlog sGD: G zgG / G \subset D. by rewrite -morphimIdom; apply; rewrite (ZgroupS _ zgG, subsetIl) ?subsetIr. apply/forall_inP=> fV /SylowP[p pr_p sylfV]. have [P sylP] := Sylow_exists p G. have [|z _ ->] := @Sylow_trans p _ _ (f @* P)%G _ _ sylfV. by apply: morphim_pHall (sylP); apply: subset_trans (pHall_sub sylP) sGD. by rewrite cyclicJ morphim_cyclic ?(forall_inP zgG) //; apply/SylowP; exists p. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype prime bigop finset fingroup morphism) mathcomp(automorphism quotient action cyclic gproduct) mathcomp(gfunctor commutator pgroup center nilpotent)