proposition: Lemma basic_p2maxElem_structure p A P : A \in 'E_p^2(G) :&: 'E*_p(G) -> p.-group P -> A \subset P -> ~~ abelian P -> let Z0 := ('Ohm_1('Z(P)))%G in [/\ Z0 \in 'E_p^1(A), exists Y : {group gT}, [/\ cyclic Y, Z0 \subset Y & forall A0, A0 \in 'E_p^1(A) :\ Z0 -> A0 \x Y = 'C_P(A)] & [transitive 'N_P(A), on 'E_p^1(A) :\ Z0| 'JG]].
proof: Proof. case/setIP=> Ep2A maxA pP sAP not_cPP Z0; set E1A := 'E_p^1(A). have p_pr: prime p := pnElem_prime Ep2A; have [_ abelA dimA] := pnElemP Ep2A. have [oA [pA cAA _]] := (card_pnElem Ep2A, and3P abelA). have [p_gt0 p_gt1] := (prime_gt0 p_pr, prime_gt1 p_pr). have{} maxA S: p.-group S -> A \subset S -> A \in 'E*_p(S) /\ 'Ohm_1('C_S(A)) = A. - move=> pS sAS; suff maxAS: A \in 'E*_p(S) by rewrite (Ohm1_cent_max maxAS). by rewrite (subsetP (pmaxElemS p (subsetT S))) // inE maxA inE. have [S sylS sPS] := Sylow_superset (subsetT P) pP. pose Z1 := 'Ohm_1('Z(S))%G; have sZ1Z: Z1 \subset 'Z(S) := Ohm_sub 1 _. have [pS sAS] := (pHall_pgroup sylS, subset_trans sAP sPS). have [maxAS defC1] := maxA S pS sAS; set C := 'C_S(A) in defC1. have sZ0A: Z0 \subset A by rewrite -defC1 OhmS // setISS // centS. have sZ1A: Z1 \subset A by rewrite -defC1 OhmS // setIS // centS. have [pZ0 pZ1]: p.-group Z0 /\ p.-group Z1 by split; apply: pgroupS pA. have sZ10: Z1 \subset Z0. rewrite -[gval Z1]Ohm_id OhmS // subsetI (subset_trans sZ1A) //=. by rewrite (subset_trans sZ1Z) // subIset // centS ?orbT. have ntZ1: Z1 :!=: 1. have: A :!=: 1 by rewrite -cardG_gt1 oA (ltn_exp2l 0). apply: contraNneq; rewrite -subG1 -(setIidPr sZ1Z) => /TI_Ohm1. by rewrite setIid => /(trivg_center_pgroup pS) <-. have EpZ01: abelian C -> Z1 = Z0 /\ Z0 \in E1A. move=> cCC; have [eqZ0A | ltZ0A] := eqVproper sZ0A. rewrite (abelianS _ cCC) // in not_cPP. by rewrite subsetI sPS centsC -eqZ0A gFsub_trans ?subsetIr. have leZ0p: #|Z0| <= p ^ 1. by rewrite (card_pgroup pZ0) leq_exp2l // -ltnS -dimA properG_ltn_log. have [_ _ [e oZ1]] := pgroup_pdiv pZ1 ntZ1. have{e oZ1}: #|Z1| >= p by rewrite oZ1 (leq_exp2l 1). rewrite (geq_leqif (leqif_trans (subset_leqif_card sZ10) (leqif_eq leZ0p))). rewrite [E1A]p1ElemE // !inE sZ0A; case/andP=> sZ01 ->. by split=> //; apply/eqP; rewrite -val_eqE eqEsubset sZ10. have [A1 neqA1Z EpA1]: exists2 A1, A1 != Z1 & #|Z1| = p -> A1 \in E1A. have [oZ1 |] := #|Z1| =P p; last by exists 1%G; rewrite // eq_sym. have [A1 defA]:= abelem_split_dprod abelA sZ1A. have{defA} [_ defA _ tiA1Z1] := dprodP defA. have EpZ1: Z1 \in E1A by rewrite [E1A]p1ElemE // !inE sZ1A /= oZ1. suffices: A1 \in E1A by exists A1; rewrite // eq_sym; apply/(TIp1ElemP EpZ1). rewrite [E1A]p1ElemE // !inE -defA mulG_subr /=. by rewrite -(mulKn #|A1| p_gt0) -{1}oZ1 -TI_cardMg // defA oA mulKn. pose cplA1C Y := [/\ cyclic Y, Z0 \subset Y, A1 \x Y = C & abelian C]. have [Y [{cplA1C} cycY sZ0Y defC cCC]]: exists Y, cplA1C Y. have [rSgt2 | rSle2] := ltnP 2 'r(S). rewrite (rank_pgroup pS) in rSgt2; have oddS := mFT_odd S. have max2AS: A \in 'E_p^2(S) :&: 'E*_p(S) by rewrite 3!inE sAS abelA dimA. have oZ1: #|Z1| = p by case/Ohm1_ucn_p2maxElem: max2AS => // _ []. have{} EpA1 := EpA1 oZ1; have [sA1A abelA1 oA1] := pnElemPcard EpA1. have EpZ1: Z1 \in E1A by rewrite [E1A]p1ElemE // !inE sZ1A /= oZ1. have [_ defA cA1Z tiA1Z] := dprodP (p2Elem_dprodP Ep2A EpA1 EpZ1 neqA1Z). have defC: 'C_S(A1) = C. rewrite /C -defA centM setICA setIC ['C_S(Z1)](setIidPl _) // centsC. by rewrite (subset_trans sZ1Z) ?subsetIr. have rCSA1: 'r_p('C_S(A1)) <= 2. by rewrite defC -p_rank_Ohm1 defC1 (p_rank_abelem abelA) dimA. have sA1S := subset_trans sA1A sAS. have nnS: p.-narrow S by apply/implyP=> _; apply/set0Pn; exists A. have [] := narrow_cent_dprod pS oddS rSgt2 nnS oA1 sA1S rCSA1. set Y := _ :&: _; rewrite {}defC => cycY _ _ defC; exists [group of Y]. have cCC: abelian C; last split=> //. apply/center_idP; rewrite -(center_dprod defC). rewrite (center_idP (abelem_abelian abelA1)). by rewrite (center_idP (cyclic_abelian cycY)). have{EpZ01} [<- _] := EpZ01 cCC; rewrite subsetI (subset_trans sZ1Z) //. by rewrite setIS ?centS ?gFsub_trans. have not_cSS := contra (abelianS sPS) not_cPP. have:= mFT_rank2_Sylow_cprod sylS rSle2 not_cSS. case=> E [_ dimE3 eE] [Y cycY [defS defY1]]. have [[_ mulEY cEY] cYY] := (cprodP defS, cyclic_abelian cycY). have defY: 'Z(S) = Y. case/cprodP: (center_cprod defS) => _ <- _. by rewrite (center_idP cYY) -defY1 mulSGid ?Ohm_sub. have pY: p.-group Y by rewrite -defY (pgroupS (center_sub S)). have sES: E \subset S by rewrite -mulEY mulG_subl. have pE := pgroupS sES pS. have defS1: 'Ohm_1(S) = E. apply/eqP; rewrite (OhmE 1 pS) eqEsubset gen_subG andbC. rewrite sub_gen; last by rewrite subsetI sES sub_LdivT. apply/subsetP=> ey /LdivP[]; rewrite -mulEY. case/imset2P=> e y Ee Yy -> eyp; rewrite groupM //. rewrite (subsetP (center_sub E)) // -defY1 (OhmE 1 pY) mem_gen //. rewrite expgMn in eyp; last by red; rewrite -(centsP cEY). by rewrite (exponentP eE) // mul1g in eyp; rewrite !inE Yy eyp eqxx. have sAE: A \subset E by rewrite -defS1 -(Ohm1_id abelA) OhmS. have defC: A * Y = C. rewrite /C -mulEY setIC -group_modr; last first. by rewrite -defY subIset // orbC centS. congr (_ * _); apply/eqP; rewrite /= setIC eqEcard subsetI sAE. have pCEA: p.-group 'C_E(A) := pgroupS (subsetIl E _) pE. rewrite -abelianE cAA (card_pgroup pCEA) oA leq_exp2l //= leqNgt. apply: contraL cycY => dimCEA3. have sAZE: A \subset 'Z(E). rewrite subsetI sAE // centsC (sameP setIidPl eqP) eqEcard subsetIl /=. by rewrite (card_pgroup pE) (card_pgroup pCEA) dimE3 leq_exp2l. rewrite abelian_rank1_cyclic // -ltnNge (rank_pgroup pY). by rewrite (p_rank_abelian p cYY) defY1 -dimA lognSg. have cAY: Y \subset 'C(A) by apply: centSS cEY. have cCC: abelian C by rewrite -defC abelianM cAA cYY. have{EpZ01} [eqZ10 EpZ1] := EpZ01 cCC; rewrite -eqZ10 in EpZ1. have sZ0Y: Z0 \subset Y by rewrite -eqZ10 -defY Ohm_sub. have{} EpA1 := EpA1 (card_pnElem EpZ1). have [sA1A _ oA1] := pnElemPcard EpA1. have [_ defA _ tiA1Z] := dprodP (p2Elem_dprodP Ep2A EpA1 EpZ1 neqA1Z). exists Y; split; rewrite // dprodE ?(centSS _ sA1A cAY) ?prime_TIg ?oA1 //. by rewrite -(mulSGid sZ0Y) -eqZ10 mulgA defA. apply: contraL cycY => sA1Y; rewrite abelian_rank1_cyclic // -ltnNge. by rewrite -dimA -rank_abelem ?rankS // -defA eqZ10 mul_subG. have{EpZ01} [eqZ10 EpZ0] := EpZ01 cCC; have oZ0 := card_pnElem EpZ0. have{} EpA1: A1 \in E1A by rewrite EpA1 ?eqZ10. have [sA1A _ oA1] := pnElemPcard EpA1; rewrite {}eqZ10 in neqA1Z. have [_ defA _ tiA1Z] := dprodP (p2Elem_dprodP Ep2A EpA1 EpZ0 neqA1Z). split=> //; first exists (P :&: Y)%G. have sPY_Y := subsetIr P Y; rewrite (cyclicS sPY_Y) //. rewrite subsetI (subset_trans sZ0A) //= sZ0Y. split=> // A0 /setD1P[neqA0Z EpA0]; have [sA0A _ _] := pnElemP EpA0. have [_ mulA0Z _ tiA0Z] := dprodP (p2Elem_dprodP Ep2A EpA0 EpZ0 neqA0Z). have{defC} [_ defC cA1Y tiA1Y] := dprodP defC. rewrite setIC -{2}(setIidPr sPS) setIAC. apply: dprod_modl (subset_trans sA0A sAP); rewrite -defC dprodE /=. - by rewrite -(mulSGid sZ0Y) !mulgA mulA0Z defA. - rewrite (centSS (subxx Y) sA0A) // -defA centM subsetI cA1Y /=. by rewrite sub_abelian_cent ?cyclic_abelian. rewrite setIC -(setIidPr sA0A) setIA -defA -group_modr //. by rewrite (setIC Y) tiA1Y mul1g setIC. apply/imsetP; exists A1; first by rewrite 2!inE neqA1Z. apply/eqP; rewrite eq_sym eqEcard; apply/andP; split. apply/subsetP=> _ /imsetP[x /setIP[Px nAx] ->]. rewrite 2!inE /E1A -(normP nAx) pnElemJ EpA1 andbT -val_eqE /=. have nZ0P: P \subset 'N(Z0) by rewrite !gFnorm_trans. by rewrite -(normsP nZ0P x Px) (inj_eq (@conjsg_inj _ x)). have pN: p.-group 'N_P(_) := pgroupS (subsetIl P _) pP. have defCPA: 'N_('N_P(A))(A1) = 'C_P(A). apply/eqP; rewrite eqEsubset andbC subsetI setIS ?cent_sub //. rewrite subIset /=; last by rewrite orbC cents_norm ?centS. rewrite setIAC (subset_trans (subsetIl _ _)) //= subsetI subsetIl /=. rewrite -defA centM subsetI andbC subIset /=; last first. by rewrite centsC gFsub_trans ?subsetIr. have nC_NP: 'N_P(A1) \subset 'N('C(A1)) by rewrite norms_cent ?subsetIr. rewrite -quotient_sub1 // subG1 trivg_card1. rewrite (pnat_1 (quotient_pgroup _ (pN _))) //. rewrite -(card_isog (second_isog nC_NP)) /= (setIC 'C(A1)). by apply: p'group_quotient_cent_prime; rewrite ?subsetIr ?oA1. have sCN: 'C_P(A) \subset 'N_P(A) by rewrite setIS ?cent_sub. have nA_NCPA: 'N_P('C_P(A)) \subset 'N_P(A). have [_ defCPA1] := maxA P pP sAP. by rewrite -[in 'N(A)]defCPA1 setIS // gFnorm_trans. rewrite card_orbit astab1JG /= {}defCPA. rewrite -(leq_add2l (Z0 \in E1A)) -cardsD1 EpZ0 (card_p1Elem_p2Elem Ep2A) ltnS. rewrite dvdn_leq ?(pfactor_dvdn 1) ?indexg_gt0 // -divgS // logn_div ?cardSg //. rewrite subn_gt0 properG_ltn_log ?pN //= (proper_sub_trans _ nA_NCPA) //. rewrite (nilpotent_proper_norm (pgroup_nil pP)) // properEneq subsetIl andbT. by apply: contraNneq not_cPP => <-; rewrite (abelianS (setSI _ sPS)). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype) mathcomp(bigop finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9)