proposition: Lemma tau12_regular M E p q P A : M \in 'M -> \sigma(M)^'.-Hall(M) E -> p \in \tau1(M) -> P \in 'E_p^1(E) -> q \in \tau2(M) -> A \in 'E_q^2(E) -> 'C_A(P) != 1 -> 'C_(M`_\sigma)(P) = 1.
proof: Proof. move=> maxM hallE t1p EpP t2q Eq2A ntCAP; apply: contraNeq (ntCAP) => ntCMsP. have [[nsAE _] _ uniq_cMs _] := tau2_compl_context maxM hallE t2q Eq2A. have [sPE abelP dimP] := pnElemP EpP; have [pP _] := andP abelP. have ntP: P :!=: 1 by apply: nt_pnElem EpP _. have [solE t1P] := (sigma_compl_sol hallE, pi_pgroup pP t1p). have [E1 hallE1 sPE1] := Hall_superset solE sPE t1P. have [_ [E3 hallE3]] := ex_tau13_compl hallE. have [E2 _ complEi] := ex_tau2_compl hallE hallE1 hallE3. have not_cAP: ~~ (P \subset 'C(A)). have [_ regCE1A _] := tau2_regular maxM complEi t2q Eq2A. apply: contra ntCMsP => cAP; rewrite (cent_semiregular regCE1A _ ntP) //. exact/subsetIP. have [sAE abelA dimA] := pnElemP Eq2A; have [qA _] := andP abelA. pose Y := 'C_A(P)%G; have{abelA dimA} EqY: Y \in 'E_q^1('C_E(P)). have sYA: Y \subset A := subsetIl A _; have abelY := abelemS sYA abelA. rewrite !inE setSI // abelY eqn_leq -{2}rank_abelem // rank_gt0 -ltnS -dimA. by rewrite properG_ltn_log //= /proper subsetIl subsetIidl centsC. have ntCMsY: 'C_(M`_\sigma)(Y) != 1. by apply: subG1_contra ntCMsP; apply: cent_tau1Elem_Msigma t1p EpP EqY. have EqEY: Y \in 'E_q^1(E) by rewrite pnElemI in EqY; case/setIP: EqY. have uniqCY := uniq_cMs _ EqEY ntCMsY. have [ntA nAE] := (nt_pnElem Eq2A isT, normal_norm nsAE). have [L maxNL] := mmax_exists (mFT_norm_proper ntA (mFT_pgroup_proper qA)). have [sLq t12Lp]: q \in \sigma(L) /\ (p \in \tau1(L)) || (p \in \tau2(L)). have [sLt2 t12cA' _] := primes_norm_tau2Elem maxM hallE t2q Eq2A maxNL. split; first by have /andP[] := sLt2 q t2q. apply: pnatPpi (pgroupS (quotientS _ sPE) t12cA') _. rewrite -p_rank_gt0 -rank_pgroup ?quotient_pgroup // rank_gt0. rewrite -subG1 quotient_sub1 ?subsetI ?sPE // (subset_trans sPE) //. by rewrite normsI ?normG ?norms_cent. have [maxL sNL] := setIdP maxNL; have sEL := subset_trans nAE sNL. have sL'p: p \in \sigma(L)^' by move: t12Lp; rewrite -andb_orr => /andP[]. have [sPL sL'P] := (subset_trans sPE sEL, pi_pgroup pP sL'p). have{sL'P} [F hallF sPF] := Hall_superset (mmax_sol maxL) sPL sL'P. have solF := sigma_compl_sol hallF. have [sAL sL_A] := (subset_trans (normG A) sNL, pi_pgroup qA sLq). have sALs: A \subset L`_\sigma by rewrite (sub_Hall_pcore (Msigma_Hall maxL)). have neqLM: L != M by apply: contraTneq sLq => ->; case/andP: t2q. have{t12Lp} [t1Lp | t2Lp] := orP t12Lp. have [F1 hallF1 sPF1] := Hall_superset solF sPF (pi_pgroup pP t1Lp). have EqLsY: Y \in 'E_q^1('C_(L`_\sigma)(P)). by rewrite !inE setSI //; case/pnElemP: EqY => _ -> ->. have [defL _] := cent_cent_Msigma_tau1_uniq maxL hallF hallF1 sPF1 ntP EqLsY. by rewrite -in_set1 -uniqCY defL set11 in neqLM. have sCPL: 'C(P) \subset L. have [B Ep2B _] := ex_tau2Elem hallF t2Lp. have EpFP: P \in 'E_p^1(F) by apply/pnElemP. have [_ _ uniq_cLs _] := tau2_compl_context maxL hallF t2Lp Ep2B. by case/mem_uniq_mmax: (uniq_cLs _ EpFP (subG1_contra (setSI _ sALs) ntCAP)). have Eq2MA: A \in 'E_q^2(M). by move: Eq2A; rewrite -(setIidPr (pHall_sub hallE)) pnElemI => /setIP[]. have [_ _ _ tiMsL _] := tau2_context maxM t2q Eq2MA. by case/negP: ntCMsP; rewrite -subG1 -(tiMsL L) ?setIS // 3!inE neqLM maxL. 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)