proposition: Corollary cent1_nreg_sigma_uniq M (Ms := M`_\sigma) x : M \in 'M -> x \in M^# -> \tau2(M).-elt x -> 'C_Ms[x] != 1 -> 'M('C[x]) = [set M].
proof: Proof. move=> maxM /setD1P[ntx]; rewrite -cycle_subG => sMX t2x. apply: contraNeq => MCx_neqM. have{MCx_neqM} [H maxCxH neqHM]: exists2 H, H \in 'M('C[x]) & H \notin [set M]. apply/subsetPn; have [H MCxH] := mmax_exists (mFT_cent1_proper ntx). by rewrite eqEcard cards1 (cardD1 H) MCxH andbT in MCx_neqM. have sCxH: 'C[x] \subset H by case/setIdP: maxCxH. have s'x: \sigma(M)^'.-elt x by apply: sub_pgroup t2x => p; case/andP. have [E hallE sXE] := Hall_superset (mmax_sol maxM) sMX s'x. have [sEM solE] := (pHall_sub hallE, sigma_compl_sol hallE). have{sXE} [E2 hallE2 sXE2] := Hall_superset solE sXE t2x. pose p := pdiv #[x]. have t2p: p \in \tau2(M) by rewrite (pnatPpi t2x) ?pi_pdiv ?order_gt1. have [A Ep2A sAE2]: exists2 A, A \in 'E_p^2(M) & A \subset E2. have [A Ep2A_E EpA] := ex_tau2Elem hallE t2p. have [sAE abelA _] := pnElemP Ep2A_E; have [pA _] := andP abelA. have [z Ez sAzE2] := Hall_Jsub solE hallE2 sAE (pi_pnat pA t2p). by exists (A :^ z)%G; rewrite // -(normsP (normsG sEM) z Ez) pnElemJ. have cE2E2: abelian E2 := tau2_compl_abelian maxM hallE hallE2. have cxA: A \subset 'C[x] by rewrite -cent_cycle (sub_abelian_cent2 cE2E2). have maxAH: H \in 'M(A) :\ M by rewrite inE neqHM (subsetP (mmax_ofS cxA)). have [_ _ _ tiMsMA _] := tau2_context maxM t2p Ep2A. by rewrite -subG1 -(tiMsMA H maxAH) setIS. 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)