proposition: Corollary cent_norm_tau13_mmax p P H : (p \in \tau1(M)) || (p \in \tau3(M)) -> P \subset M -> p.-group P -> H \in 'M('N(P)) -> [/\ forall P1, P1 \subset M :&: H -> p.-group P1 -> P1 \subset 'C(M`_\sigma :&: H), forall X, X \subset E :&: H -> \tau1(H)^'.-group X -> X \subset 'C(M`_\sigma :&: H) & [~: M`_\sigma :&: H, M :&: H] != 1 -> p \in \sigma(H) /\ (p \in \tau1(M) -> p \in \beta(H))].
proof: Proof. move=> t13Mp sPM pP /setIdP[maxH sNP_H]. have ntP: P :!=: 1. by apply: contraTneq sNP_H => ->; rewrite norm1 proper_subn ?mmax_proper. have st2Hp: (p \in \sigma(H)) || (p \in \tau2(H)). exact: (prime_class_mmax_norm maxH pP sNP_H). have not_MGH: gval H \notin M :^: G. apply: contraL st2Hp => /imsetP[x _ ->]; rewrite sigmaJ tau2J negb_or. by have:= t13Mp; rewrite -2!andb_orr !inE => /and3P[-> /eqP->]. set R := [~: _, _]; have [/commG1P | ntR] := altP (R =P 1). rewrite centsC => cMH; split=> // X sX_EH _; apply: subset_trans cMH => //. by rewrite (subset_trans sX_EH) ?setSI. have piEp: p \in \pi(E). by rewrite (partition_pi_sigma_compl maxM) // orbCA t13Mp orbT. have piHp: p \in \pi(H). by rewrite (partition_pi_mmax maxH) orbCA orbC -!orbA st2Hp !orbT. have t1H'p: p \notin \tau1(H). by apply: contraL st2Hp; rewrite negb_or !inE => /and3P[-> /eqP->]. case: (Msigma_setI_mmax_central maxH piEp) => // cMsH t2H'p b_p. split=> // [X sX_EH t1'X | _]. have [sXE sXH] := subsetIP sX_EH. rewrite -(Sylow_gen X) gen_subG; apply/bigcupsP=> Q; case/SylowP=> q _ sylQ. have [-> | ntQ] := eqsVneq Q 1; first exact: sub1G. have piXq: q \in \pi(X) by rewrite -p_rank_gt0 -(rank_Sylow sylQ) rank_gt0. have [[piEq piHq] t1H'q] := (piSg sXE piXq, piSg sXH piXq, pnatPpi t1'X piXq). have [sQX qQ _] := and3P sylQ; have sXM := subset_trans sXE sEM. case: (Msigma_setI_mmax_central maxH piEq) => // -> //. by rewrite subsetI !(subset_trans sQX). rewrite (negPf t2H'p) orbF in st2Hp. by rewrite -predI_sigma_beta // {3}/in_mem /= st2Hp. 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 frobenius) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection12)