proposition: Corollary tau2_compl_context M E p A (Ms := M`_\sigma) : M \in 'M -> \sigma(M)^'.-Hall(M) E -> p \in \tau2(M) -> A \in 'E_p^2(E) -> [/\ A <| E /\ 'E_p^1(E) = 'E_p^1(A), [/\ 'C(A) \subset E, 'N_M(A) = E & ~~ ('N(A) \subset M)], forall X, X \in 'E_p^1(E) -> 'C_Ms(X) != 1 -> 'M('C(X)) = [set M] & forall Mstar, Mstar \in 'M -> gval Mstar \notin M :^: G -> Ms :&: Mstar`_\sigma = 1 /\ [predI \sigma(M) & \sigma(Mstar)] =i pred0].
proof: Proof. move=> maxM hallE t2Mp Ep2A; have [sEM sM'E _] := and3P hallE. have [p_pr [sM'p _]] := (pnElem_prime Ep2A, andP t2Mp). have [sAE abelA dimA] := pnElemP Ep2A; have [pA cAA _] := and3P abelA. have [_ mulMsE nMsE tiMsE] := sdprodP (sdprod_sigma maxM hallE). have Ep2A_M: A \in 'E_p^2(M) by rewrite (subsetP (pnElemS _ _ sEM)). have [syl_p_M nsMsAM regA tiMsMA _] := tau2_context maxM t2Mp Ep2A_M. have nMsA: A \subset 'N(Ms) := subset_trans sAE nMsE. have nsAE: A <| E. rewrite /normal sAE -(mul1g A) -tiMsE setIC group_modr // normsI ?normG //. by rewrite (subset_trans sEM) // -(norm_joinEr nMsA) normal_norm. have sAsylE P: p.-Sylow(E) P -> 'Ohm_1(P) = A /\ ~~ ('N(P) \subset M). move=> sylP; have sylP_M: p.-Sylow(M) P by apply: (subHall_Sylow hallE). have [_] := syl_p_M P sylP_M; apply. exact: subset_trans (pcore_max pA nsAE) (pcore_sub_Hall sylP). have not_sNA_M: ~~ ('N(A) \subset M). have [P sylP] := Sylow_exists p E; have [<-]:= sAsylE P sylP. exact/contra/subset_trans/gFnorms. have{sAsylE syl_p_M} defEpE: 'E_p^1(E) = 'E_p^1(A). apply/eqP; rewrite eqEsubset andbC pnElemS //. apply/subsetP=> X /pnElemP[sXE abelX dimX]; apply/pnElemP; split=> //. have [pX _ eX] := and3P abelX; have [P sylP sXP] := Sylow_superset sXE pX. have [<- _]:= sAsylE P sylP; have [_ pP _] := and3P sylP. by rewrite (OhmE 1 pP) sub_gen // subsetI sXP sub_LdivT. have defNMA: 'N_M(A) = E. rewrite -mulMsE setIC -group_modr ?normal_norm //= setIC. rewrite coprime_norm_cent ?regA ?mul1g //. exact: (pnat_coprime (pcore_pgroup _ _) (pi_pnat pA _)). have [sCAM _]: 'C(A) \subset M /\ _ := p2Elem_mmax maxM Ep2A_M. have sCAE: 'C(A) \subset E by rewrite -defNMA subsetI sCAM cent_sub. split=> // [X EpX | H maxH not_MGH]; last first. by case/sigma_disjoint: not_MGH => // _ _; apply; apply: tau2_Msigma_nil t2Mp. rewrite defEpE in EpX; have [sXA abelX dimX] := pnElemP EpX. have ntX: X :!=: 1 by rewrite -rank_gt0 (rank_abelem abelX) dimX. apply: contraNeq => neq_maxCX_M. have{neq_maxCX_M} [H]: exists2 H, H \in 'M('C(X)) & H \notin [set M]. apply/subsetPn; rewrite subset1 negb_or neq_maxCX_M. by have [H maxH]:= mmax_exists (mFT_cent_proper ntX); apply/set0Pn; exists H. case/setIdP=> maxH sCXH neqHM. rewrite -subG1 -(tiMsMA H) ?setIS // inE neqHM inE maxH. exact: subset_trans (sub_abelian_cent cAA sXA) sCXH. 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)