proposition: Corollary pi_of_cent_sigma M x x' : M \in 'M -> x \in (M`_\sigma)^# -> x' \in ('C_M[x])^# -> \sigma(M)^'.-elt x' -> \kappa(M).-elt x' /\ 'C[x] \subset M \/ [/\ \tau2(M).-elt x', \ell_\sigma(x') == 1%N & 'M('C[x']) = [set M]].
proof: Proof. move: x' => y maxM /setD1P[ntx Ms_x] /setD1P[nty cMxy] s'y. have [My cxy] := setIP cMxy. have [t2y | not_t2y] := boolP (\tau2(M).-elt y); [right | left]. have uniqCy: 'M('C[y]) = [set M]; last split=> //. apply: cent1_nreg_sigma_uniq; rewrite // ?inE ?nty //. by apply/trivgPn; exists x; rewrite // inE Ms_x cent1C. pose p := pdiv #[y]; have piYp: p \in \pi(#[y]) by rewrite pi_pdiv order_gt1. have t2p := pnatPpi t2y piYp; have [E hallE] := ex_sigma_compl maxM. have [A Ep2A _] := ex_tau2Elem hallE t2p. have pA: p.-group A by case/pnElemP: Ep2A => _ /andP[]. have ntA: A :!=: 1 by rewrite (nt_pnElem Ep2A). have [H maxNH] := mmax_exists (mFT_norm_proper ntA (mFT_pgroup_proper pA)). have [st2MsH _ _] := primes_norm_tau2Elem maxM hallE t2p Ep2A maxNH. have [maxH _] := setIdP maxNH. have sHy: \sigma(H).-elt y by apply: sub_p_elt t2y => q /st2MsH/andP[]. rewrite /sigma_length (cardsD1 y.`_(\sigma(H))). rewrite mem_sigma_decomposition //; last by rewrite constt_p_elt. rewrite eqSS -sigma_decomposition_constt' //. by apply/ell_sigma0P; rewrite (constt1P _) ?p_eltNK. have{not_t2y} [p piYp t2'p]: exists2 p, p \in \pi(#[y]) & p \notin \tau2(M). by apply/allPn; rewrite negb_and cardG_gt0 in not_t2y. have sYM: <[y]> \subset M by rewrite cycle_subG. have piMp: p \in \pi(M) := piSg sYM piYp. have t13p: p \in [predU \tau1(M) & \tau3(M)]. move: piMp; rewrite partition_pi_mmax // (negPf t2'p) /= orbA. by case/orP=> // sMy; case/negP: (pnatPpi s'y piYp). have [X]: exists X, X \in 'E_p^1(<[y]>) by apply/p_rank_geP; rewrite p_rank_gt0. rewrite -(setIidPr sYM) pnElemI -setIdE => /setIdP[EpX sXy]. have kp: p \in \kappa(M). rewrite unlock; apply/andP; split=> //; apply/exists_inP; exists X => //. apply/trivgPn; exists x; rewrite // inE Ms_x (subsetP (centS sXy)) //. by rewrite cent_cycle cent1C. have [sXM abelX dimX] := pnElemP EpX; have [pX _] := andP abelX. have [K hallK sXK] := Hall_superset (mmax_sol maxM) sXM (pi_pgroup pX kp). have PmaxM: M \in 'M_'P. by rewrite 2!inE maxM andbT; apply: contraL kp => k'M; apply: (pnatPpi k'M). have [_ [defNK defNX] [_ uniqCKs] _ _] := Ptype_structure PmaxM hallK. have{defNX} sCMy_nMK: 'C_M[y] \subset 'N_M(K). have [|<- _] := defNX X. by apply/nElemP; exists p; rewrite !inE sXK abelX dimX. by rewrite setIS // cents_norm // -cent_cycle centS. have [[sMK kK _] [_ mulKKs cKKs _]] := (and3P hallK, dprodP defNK). have s'K: \sigma(M)^'.-group K := sub_pgroup (@kappa_sigma' M) kK. have sMs: \sigma(M).-group M`_\sigma := pcore_pgroup _ M. have sKs: \sigma(M).-group 'C_(M`_\sigma)(K) := pgroupS (subsetIl _ _) sMs. have{s'K sKs} [hallK_N hallKs] := coprime_mulGp_Hall mulKKs s'K sKs. split. rewrite (mem_p_elt kK) // (mem_normal_Hall hallK_N) ?normal_subnorm //. by rewrite (subsetP sCMy_nMK) // inE My cent1id. have Mx: x \in M := subsetP (pcore_sub _ _) x Ms_x. have sxKs: <[x]> \subset 'C_(M`_\sigma)(K). rewrite cycle_subG (mem_normal_Hall hallKs) ?(mem_p_elt sMs) //=. by rewrite -mulKKs /normal mulG_subr mulG_subG normG cents_norm // centsC. by rewrite (subsetP sCMy_nMK) // inE Mx cent1C. have /rank_geP[Z]: 0 < 'r(<[x]>) by rewrite rank_gt0 cycle_eq1. rewrite /= -(setIidPr sxKs) nElemI -setIdE => /setIdP[E1KsZ sZx]. have [_ sCZM] := mem_uniq_mmax (uniqCKs Z E1KsZ). by rewrite (subset_trans _ sCZM) // -cent_cycle centS. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype bigop order) mathcomp(finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall frobenius) mathcomp(ssralg ssrnum ssrint rat) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection12 BGsection13)