proposition: Lemma Phi_joing : 'Phi(P) = P^`(1) <*> 'Mho^1(P).
proof: Proof. have [sPhiP nPhiP] := andP (Phi_normal P). apply/eqP; rewrite eqEsubset join_subG. case: (eqsVneq P 1) => [-> | ntP] in sPhiP *. by rewrite /= (trivgP sPhiP) sub1G der_subS Mho_sub. have [p_pr _ _] := pgroup_pdiv pP ntP. have [abP x1P] := abelemP p_pr Phi_quotient_abelem. apply/andP; split. have nMP: P \subset 'N(P^`(1) <*> 'Mho^1(P)) by rewrite normsY // !gFnorm. rewrite -quotient_sub1 ?gFsub_trans //=. suffices <-: 'Phi(P / (P^`(1) <*> 'Mho^1(P))) = 1 by apply: morphimF. apply/eqP; rewrite (trivg_Phi (morphim_pgroup _ pP)) /= -quotientE. apply/abelemP=> //; rewrite [abelian _]quotient_cents2 ?joing_subl //. split=> // _ /morphimP[x Nx Px ->] /=. rewrite -morphX //= coset_id // (MhoE 1 pP) joing_idr expn1. by rewrite mem_gen //; apply/setUP; right; apply: imset_f. rewrite -quotient_cents2 // [_ \subset 'C(_)]abP (MhoE 1 pP) gen_subG /=. apply/subsetP=> _ /imsetP[x Px ->]; rewrite expn1. have nPhi_x: x \in 'N('Phi(P)) by apply: (subsetP nPhiP). by rewrite coset_idr ?groupX ?morphX ?x1P ?mem_morphim. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism quotient) mathcomp(action commutator gproduct gfunctor ssralg) mathcomp(countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule)