proposition: Theorem exceptional_Sylow_abelian P1 : p.-Sylow(M) P1 -> abelian P1.
proof: Proof. have nregA Q: gval Q != 1 -> A \subset 'N(Q) -> coprime #|Q| #|A| -> exists2 X, X \in 'E_p^1(A) & 'C_Q(X) != 1. - move=> ntQ nQA coQA; apply/exists_inP; apply: contraR ntQ. rewrite negb_exists_in -subG1; move/forall_inP=> regA. have ncycA: ~~ cyclic A by rewrite (abelem_cyclic abelA) oA pfactorK. rewrite -(coprime_abelian_gen_cent1 _ _ nQA) // gen_subG. apply/bigcupsP=> x /setD1P[ntx Ax]. apply/negPn; rewrite /= -cent_cycle subG1 regA // p1ElemE // !inE. by rewrite cycle_subG Ax /= -orderE (abelem_order_p abelA). suffices{P1} cPP: abelian P. by move=> sylP1; have [m _ ->] := Sylow_trans sylP sylP1; rewrite abelianJ. have [g nPg notMg] := subsetPn not_sNP_M. pose Ms := M`_\sigma; pose q := pdiv #|Ms|; have pP := pHall_pgroup sylP. have nMsP: P \subset 'N(Ms) by rewrite (subset_trans sPM) ?gFnorm. have coMsP: coprime #|Ms| #|P|. exact: pnat_coprime (pcore_pgroup _ _) (pi_pnat pP sM'p). have [Q1 sylQ1 nQ1P]:= sol_coprime_Sylow_exists q (pgroup_sol pP) nMsP coMsP. have ntQ1: Q1 :!=: 1. rewrite -cardG_gt1 (card_Hall sylQ1) p_part_gt1 pi_pdiv cardG_gt1. by rewrite Msigma_neq1. have nQ1A: A \subset 'N(Q1) := subset_trans sAP nQ1P. have coQ1A: coprime #|Q1| #|A|. by rewrite (coprimeSg (pHall_sub sylQ1)) // (coprimegS sAP). have [X1 EpX1 nregX11] := nregA _ ntQ1 nQ1A coQ1A. pose Q2 := Q1 :^ g; have sylQ2: q.-Sylow(Ms :^ g) Q2 by rewrite pHallJ2. have{ntQ1} ntQ2: Q2 != 1 by rewrite -!cardG_gt1 cardJg in ntQ1 *. have nQ2A: A \subset 'N(Q2) by rewrite (subset_trans sAP) ?norm_conj_norm. have{coQ1A} coQ2A: coprime #|Q2| #|A| by rewrite cardJg. have{nregA ntQ2 coQ2A} [X2 EpX2 nregX22] := nregA _ ntQ2 nQ2A coQ2A. have [|_ regA]:= exceptional_TIsigmaJ notMg _ sylQ1 nQ1A sylQ2 nQ2A. by rewrite (subset_trans sAP) // -(normP nPg) conjSg. have regX21: 'C_Q1(X2) = 1 by case: (regA X2) nregX22 => // ->; rewrite eqxx. have regX12: 'C_Q2(X1) = 1 by case: (regA X1) nregX11 => // ->; rewrite eqxx. pose X := 'Ohm_1('Z(P))%G. have eqCQ12_X: ('C_Q1(X) == 1) = ('C_Q2(X) == 1). rewrite -(inj_eq (@conjsg_inj _ g)) conjs1g conjIg -/Q2 -centJ (normP _) //. by rewrite (subsetP (gFnorm_trans _ _) g nPg) ?gFnorms. have{} EpX1: X1 \in 'E_p^1(A) :\ X. rewrite 2!inE EpX1 andbT; apply: contraNneq nregX11 => defX1. by rewrite defX1 eqCQ12_X -defX1 regX12. have{eqCQ12_X} EpX2: X2 \in 'E_p^1(A) :\ X. rewrite 2!inE EpX2 andbT; apply: contraNneq nregX22 => defX2. by rewrite defX2 -eqCQ12_X -defX2 regX21. apply: contraR nregX11 => not_cPP. have{not_cPP} transNPA: [transitive 'N_P(A), on 'E_p^1(A) :\ X | 'JG]. have [|_ _]:= basic_p2maxElem_structure _ pP sAP not_cPP; last by []. by rewrite inE (subsetP (pnElemS p 2 (subsetT M))). have [y PnAy ->] := atransP2 transNPA EpX2 EpX1; have [Py _] := setIP PnAy. by rewrite centJ -(normsP nQ1P y Py) -conjIg regX21 conjs1g. 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 BGsection10)