proposition: Lemma tau13_nonregular_sigma M E p P : M \in 'M -> \sigma(M)^'.-Hall(M) E -> P \in 'E_p^1(E) -> (p \in \tau1(M)) || (p \in \tau3(M)) -> 'C_(M`_\sigma)(P) != 1 -> {in 'M('N(P)), forall Mstar, p \in \sigma(Mstar)}.
proof: Proof. move=> maxM hallE EpP t13Mp ntCMsP L maxNL /=. have [maxL sNL] := setIdP maxNL. have [sPE abelP dimP] := pnElemP EpP; have [pP _] := andP abelP. have [solE ntP] := (sigma_compl_sol hallE, nt_pnElem EpP isT). have /orP[// | t2Lp] := prime_class_mmax_norm maxL pP sNL. have:= ntCMsP; rewrite -rank_gt0 => /rank_geP[Q /nElemP[q EqQ]]. have [sQcMsP abelQ dimQ] := pnElemP EqQ; have [sQMs cPQ] := subsetIP sQcMsP. have piQq: q \in \pi(Q) by rewrite -p_rank_gt0 p_rank_abelem ?dimQ. have sMq: q \in \sigma(M) := pnatPpi (pgroupS sQMs (pcore_pgroup _ M)) piQq. have rpM: 'r_p(M) = 1%N by move: t13Mp; rewrite -2!andb_orr andbCA; case: eqP. have sL'q: q \notin \sigma(L). have notMGL: gval L \notin M :^: G. by apply: contraL t2Lp => /imsetP[x _ ->]; rewrite tau2J 2!inE rpM andbF. by apply: contraFN (sigma_partition maxM maxL notMGL q) => sLq; apply/andP. have [[sL'p _] [qQ _]] := (andP t2Lp, andP abelQ). have sL'PQ: \sigma(L)^'.-group (P <*> Q). by rewrite cent_joinEr // pgroupM (pi_pgroup pP) // (pi_pgroup qQ). have sPQ_L: P <*> Q \subset L. by rewrite (subset_trans _ sNL) // join_subG normG cents_norm. have{sPQ_L sL'PQ} [F hallF sPQF] := Hall_superset (mmax_sol maxL) sPQ_L sL'PQ. have{sPQF} [sPF sQF] := joing_subP sPQF. have [A Ep2A _] := ex_tau2Elem hallF t2Lp. have [[nsAF defA1] _ _ _] := tau2_compl_context maxL hallF t2Lp Ep2A. have EpAP: P \in 'E_p^1(A) by rewrite -defA1; apply/pnElemP. have{EpAP} sPA: P \subset A by case/pnElemP: EpAP. have sCQM: 'C(Q) \subset M. suffices: 'M('C(Q)) = [set M] by case/mem_uniq_mmax. have [t1Mp | t3Mp] := orP t13Mp. have [E1 hallE1 sPE1] := Hall_superset solE sPE (pi_pgroup pP t1Mp). by have [] := cent_cent_Msigma_tau1_uniq maxM hallE hallE1 sPE1 ntP EqQ. have [E3 hallE3 sPE3] := Hall_superset solE sPE (pi_pgroup pP t3Mp). have [[E1 hallE1] _] := ex_tau13_compl hallE; have [sE1E _] := andP hallE1. have [E2 _ complEi] := ex_tau2_compl hallE hallE1 hallE3. have [regE3 | ntE1 _ prE _] := tau13_nonregular maxM complEi. by rewrite (cent_semiregular regE3 sPE3 ntP) eqxx in ntCMsP. rewrite /= (cent_semiprime prE) // -(cent_semiprime prE sE1E ntE1) in EqQ. by have [] := cent_cent_Msigma_tau1_uniq maxM hallE hallE1 _ ntE1 EqQ. have not_cQA: ~~ (A \subset 'C(Q)). have [_ abelA dimA] := pnElemP Ep2A; apply: contraFN (ltnn 1) => cQA. by rewrite -dimA -p_rank_abelem // -rpM p_rankS ?(subset_trans cQA sCQM). have t1Lq: q \in \tau1(L). have [_ nsCF t1Fb] := tau1_cent_tau2Elem_factor maxL hallF t2Lp Ep2A. rewrite (pnatPpi (pgroupS (quotientS _ sQF) t1Fb)) //. rewrite -p_rank_gt0 -rank_pgroup ?quotient_pgroup // rank_gt0. rewrite -subG1 quotient_sub1 ?(subset_trans _ (normal_norm nsCF)) //. by rewrite subsetI sQF centsC. have defP: 'C_A(Q) = P. apply/eqP; rewrite eq_sym eqEcard subsetI sPA centsC cPQ /=. have [_ abelA dimA] := pnElemP Ep2A; have [pA _] := andP abelA. rewrite (card_pgroup (pgroupS _ pA)) ?subsetIl // (card_pgroup pP) dimP. rewrite leq_exp2l ?prime_gt1 ?(pnElem_prime EpP) //. by rewrite -ltnS -dimA properG_ltn_log // /proper subsetIl subsetIidl. have EqFQ: Q \in 'E_q^1(F) by apply/pnElemP. have regQLs: 'C_(L`_\sigma)(Q) = 1. by rewrite (tau12_regular maxL hallF t1Lq EqFQ t2Lp Ep2A) // defP. have ntAQ: [~: A, Q] != 1 by rewrite (sameP eqP commG1P). have [_ _ [_]] := tau1_act_tau2 maxL hallF t2Lp Ep2A t1Lq EqFQ regQLs ntAQ. by case/negP; rewrite /= defP (subset_trans (cent_sub P)). 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)