proposition: Corollary cent_der_sigma_uniq M p X (Ms := M`_\sigma) : M \in 'M -> X \in 'E_p^1(M) -> (p \in \beta(M)) || (X \subset Ms^`(1)) -> 'M('C(X)) = [set M] /\ (forall P, p.-Sylow(Ms) P -> 'M(P) = [set M]).
proof: Proof. move=> maxM EpX bMp_sXMs'; have p_pr := pnElem_prime EpX. have [sXM abelX oX] := pnElemPcard EpX; have [pX _] := andP abelX. have ntX: X :!=: 1 := nt_pnElem EpX isT; have ltCXG := mFT_cent_proper ntX. have sMp: p \in \sigma(M). have [bMp | sXMs'] := orP bMp_sXMs'; first by rewrite beta_sub_sigma. rewrite -pnatE // -[p]oX; apply: pgroupS (subset_trans sXMs' (der_sub 1 _)) _. exact: pcore_pgroup. have hallMs: \sigma(M).-Hall(M) Ms by apply: Msigma_Hall. have sXMs: X \subset Ms by rewrite (sub_Hall_pcore hallMs) // /pgroup oX pnatE. have [P sylP sXP]:= Sylow_superset sXMs pX. have sylP_M: p.-Sylow(M) P := subHall_Sylow hallMs sMp sylP. have sylP_G := sigma_Sylow_G maxM sMp sylP_M. have [sPM pP _] := and3P sylP_M; have ltPG := mFT_pgroup_proper pP. suffices [-> uniqP]: 'M('C(X)) = [set M] /\ 'M(P) = [set M]. split=> // Py sylPy; have [y Ms_y ->] := Sylow_trans sylP sylPy. rewrite (def_uniq_mmaxJ _ uniqP) (group_inj (conjGid _)) //. exact: subsetP (pcore_sub _ _) y Ms_y. have [rCPXgt2 | rCPXle2] := ltnP 2 'r_p('C_P(X)). have [sCPX_P sCPX_CX] := subsetIP (subxx 'C_P(X)). have [ltP ltCX] := (mFT_pgroup_proper pP, mFT_cent_proper ntX). have sCPX_M := subset_trans sCPX_P sPM. have ltCPX_G := sub_proper_trans sCPX_P ltPG. suff uniqCPX: 'M('C_P(X)) = [set M] by rewrite !(def_uniq_mmaxS _ _ uniqCPX). apply: (def_uniq_mmax (rank3_Uniqueness _ _)) => //. exact: leq_trans (p_rank_le_rank p _). have nnP: p.-narrow P. apply: wlog_neg; rewrite negb_imply; case/andP=> rP _. by apply/narrow_centP; rewrite ?mFT_odd //; exists X. have{bMp_sXMs'} [bM'p sXMs']: p \notin \beta(M) /\ X \subset Ms^`(1). move: bMp_sXMs'; rewrite !inE -negb_exists_in. by case: exists_inP => // [[]]; exists P. have defMs: 'O_p^'(Ms) ><| P = Ms. by have [_ hallMp' _] := beta_max_pdiv maxM bM'p; apply/sdprod_Hall_p'coreP. have{defMs} sXP': X \subset P^`(1). have{defMs} [_ defMs nMp'P tiMp'P] := sdprodP defMs. have [injMp'P imMp'P] := isomP (quotient_isom nMp'P tiMp'P). rewrite -(injmSK injMp'P) // morphim_der // {injMp'P}imMp'P morphim_restrm. rewrite (setIidPr sXP) /= -quotientMidl defMs -quotient_der ?quotientS //. by rewrite -defMs mul_subG ?normG. have [rPgt2 | rPle2] := ltnP 2 'r_p(P). case/eqP: ntX; rewrite -(setIidPl sXP'). by case/(narrow_cent_dprod pP (mFT_odd P)): rCPXle2. have not_cPP: ~~ abelian P. by rewrite (sameP derG1P eqP) (subG1_contra sXP') ?ntX. have sXZ: X \subset 'Z(P). rewrite -rank_pgroup // in rPle2. have := mFT_rank2_Sylow_cprod sylP_G rPle2 not_cPP. case=> Q [not_cQQ dimQ _] [R]; move/cyclic_abelian=> cRR [defP _]. have [_ mulQR _] := cprodP defP; have [sQP _] := mulG_sub mulQR. rewrite (subset_trans sXP') // -(der_cprod 1 defP) (derG1P cRR) cprodg1. have{} dimQ: logn p #|Q| <= 3 by rewrite dimQ. have [[_ ->] _] := p3group_extraspecial (pgroupS sQP pP) not_cQQ dimQ. by case/cprodP: (center_cprod defP) => _ <- _; apply: mulG_subl. have uniqP: 'M(P) = [set M]. exact: def_uniq_mmax (nonabelian_Uniqueness pP not_cPP) maxM sPM. rewrite (def_uniq_mmaxS _ ltCXG uniqP) //. by rewrite centsC (subset_trans sXZ) // subsetIr. 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)