proposition: Theorem plength1_norm_pmaxElem gT p (G E L : {group gT}) : E \in 'E*_p(G) -> odd p -> solvable G -> p.-length_1 G -> L \subset G -> E \subset 'N(L) -> p^'.-group L -> L \subset 'O_p^'(G).
proof: Proof. move=> maxE p_odd solG pl1G sLG nEL p'L. case p_pr: (prime p); last first. by rewrite pcore_pgroup_id // p'groupEpi mem_primes p_pr. wlog Gp'1: gT G E L maxE solG pl1G sLG nEL p'L / 'O_p^'(G) = 1. set K := 'O_p^'(G); have [sKG nKG] := andP (pcore_normal _ G : K <| G). move/(_ _ (G / K) (E / K) (L / K))%G; rewrite morphim_sol ?plength1_quo //. rewrite morphimS ?morphim_norms ?quotient_pgroup // trivg_pcore_quotient. rewrite (quotient_sub1 (subset_trans sLG nKG)) => -> //. have [EpE _] := pmaxElemP maxE; have{EpE} [sEG abelE] := pElemP EpE. apply/pmaxElemP; rewrite inE quotient_abelem ?quotientS //. split=> // Fb; case/pElemP=> sFbG abelFb; have [pFb _ _] := and3P abelFb. have [S sylS sES] := Sylow_superset sEG (abelem_pgroup abelE). have [sSG pS _] := and3P sylS; have nKS := subset_trans sSG nKG. have: (E / K)%G \in 'E*_p(S / K). have: E \in 'E*_p(S) by rewrite (subsetP (pmaxElemS p sSG)) // inE maxE inE. have coKS: coprime #|K| #|S| := p'nat_coprime (pcore_pgroup _ _) pS. have [injK imK] := isomP (quotient_isom nKS (coprime_TIg coKS)). by rewrite -(injm_pmaxElem injK) ?imK ?inE //= morphim_restrm (setIidPr _). case/pmaxElemP=> _; apply; rewrite inE abelFb andbT. rewrite (sub_normal_Hall (quotient_pHall _ sylS)) //= -quotientMidl /= -/K. by rewrite plength1_Sylow_prod // quotient_pseries2 pcore_normal. have [EpE _] := pmaxElemP maxE; have{EpE} [sEG abelE] := pElemP EpE. have [S sylS sES] := Sylow_superset sEG (abelem_pgroup abelE). have [sSG pS _] := and3P sylS; have oddS: odd #|S| := odd_pgroup_odd p_odd pS. have defS: S :=: 'O_p(G) by apply eq_Hall_pcore; rewrite -?plength1_pcore_Sylow. have coSL: coprime #|S| #|L| := pnat_coprime pS p'L. have tiSL: S :&: L = 1 := coprime_TIg coSL. have{solG} scSG: 'C_G(S) \subset S. by rewrite defS -Fitting_eq_pcore ?cent_sub_Fitting. rewrite Gp'1 -tiSL subsetIidr (subset_trans _ scSG) // subsetI sLG /=. have nSL: L \subset 'N(S) by rewrite (subset_trans sLG) // defS gFnorm. have cLE: L \subset 'C(E). by rewrite (sameP commG1P trivgP) -tiSL setIC commg_subI ?(introT subsetIP). have maxES: E \in 'E*_p(S) by rewrite (subsetP (pmaxElemS p sSG)) ?(maxE, inE). have EpE: E \in 'E_p(S) by apply/setIdP. by rewrite (coprime_odd_faithful_cent_abelem EpE) ?(pmaxElem_LdivP p_pr maxES). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq div fintype finset) mathcomp(prime fingroup morphism automorphism quotient gproduct gfunctor) mathcomp(cyclic center commutator pgroup nilpotent sylow abelian hall) mathcomp(maximal) odd_order(BGsection1 BGappendixAB)