proposition: Theorem tau2_context M p A (Ms := M`_\sigma) : M \in 'M -> p \in \tau2(M) -> A \in 'E_p^2(M) -> [/\ forall P, p.-Sylow(M) P -> abelian P /\ (A \subset P -> 'Ohm_1(P) = A /\ ~~ ('N(P) \subset M)), Ms <*> A <| M, 'C_Ms(A) = 1, forall Mstar, Mstar \in 'M(A) :\ M -> Ms :&: Mstar = 1 & exists2 A1, A1 \in 'E_p^1(A) & 'C_Ms(A1) = 1].
proof: Proof. move=> maxM t2Mp Ep2A; have [sM'p _] := andP t2Mp. have [_]:= p2Elem_mmax maxM Ep2A; rewrite -negb_exists_in [p \in _](negPf sM'p). have [[A0 EpA0 /eqP/mem_uniq_mmax[_ sNA0M _]] | _ [] //] := exists_inP. have{EpA0 sNA0M} excM: exceptional_FTmaximal p M A0 A by []. have strM := exceptional_structure maxM excM. have [sAM abelA dimA] := pnElemP Ep2A; have [pA cAA _] := and3P abelA. have [P sylP sAP] := Sylow_superset sAM pA. have nsMsA_M : Ms <*> A <| M := exceptional_mul_sigma_normal maxM excM sylP sAP. have [_ regA [A1 EpA1 [_ _ [_ regA1 _]]]] := strM P sylP sAP. split=> // [P1 sylP1 | {P sylP sAP A0 excM}H| ]; last by exists A1. split=> [|sAP1]; first exact: (exceptional_Sylow_abelian _ excM sylP). split; first by case/strM: sylP1. by apply: contra sM'p => sNP1M; apply/exists_inP; exists P1; rewrite // ?inE. case/setD1P; rewrite -val_eqE /= => neqHM /setIdP[maxH sAH]. apply/trivgP; rewrite -regA subsetI subsetIl /=. have Ep2A_H: A \in 'E_p^2(H) by apply/pnElemP. have [_]:= p2Elem_mmax maxH Ep2A_H; rewrite -negb_exists_in. have [[A0 EpA0 /eqP/mem_uniq_mmax[_ sNA0H _]]|_ [//|sHp _ nilHs]] := exists_inP. have [cMSH_A _]:= nonuniq_p2Elem_cent_sigma maxM maxH neqHM Ep2A EpA0 sNA0H. by rewrite centsC cMSH_A. have [P sylP sAP] := Sylow_superset sAH pA; have [sPH pP _] := and3P sylP. have sylP_Hs: p.-Sylow(H`_\sigma) P. rewrite (pHall_subl _ (pcore_sub _ _) sylP) //. by rewrite (sub_Hall_pcore (Msigma_Hall maxH)) // (pi_pgroup pP). have nPH: H \subset 'N(P). by rewrite (nilpotent_Hall_pcore nilHs sylP_Hs) !gFnorm_trans ?normG. have coMsP: coprime #|M`_\sigma| #|P|. exact: pnat_coprime (pcore_pgroup _ _) (pi_pnat pP _). rewrite (sameP commG1P trivgP) -(coprime_TIg coMsP) commg_subI ?setIS //. by rewrite subsetI sAP (subset_trans sAM) ?gFnorm. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq choice div fintype) mathcomp(path bigop finset prime fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor pgroup cyclic commutator) mathcomp(center gseries nilpotent sylow abelian maximal hall frobenius) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection11)