proposition: Lemma cent_cent_Msigma_tau1_uniq E1 P q X (Ms := M`_\sigma) : \tau1(M).-Hall(E) E1 -> P \subset E1 -> P :!=: 1 -> X \in 'E_q^1('C_Ms(P)) -> 'M('C(X)) = [set M] /\ (forall S, q.-Sylow(Ms) S -> 'M(S) = [set M]).
proof: Proof. move=> hallE1 sPE1 ntP EqX; have [sE1E t1E1 _] := and3P hallE1. rewrite (cent_semiprime (tau1_primact_Msigma hallE1)) //= -/Ms in EqX. have{P ntP sPE1} ntE1 := subG1_contra sPE1 ntP. have /andP[sMsM nMsM]: Ms <| M := pcore_normal _ M. have coMsE: coprime #|Ms| #|E| := coprime_sigma_compl hallE. have [solMs nMsE] := (solvableS sMsM (mmax_sol maxM), subset_trans sEM nMsM). apply: cent_der_sigma_uniq => //. by move: EqX; rewrite -(setIidPr sMsM) -setIA pnElemI => /setIP[]. have{EqX} [[sXcMsE1 abelX _] ntX] := (pnElemP EqX, nt_pnElem EqX isT). apply: contraR ntX => /norP[b'q not_sXMs']; rewrite -subG1. have [S sylS nSE] := coprime_Hall_exists q nMsE coMsE solMs. have{abelX} [[sSMs qS _] [qX _]] := (and3P sylS, andP abelX). have sScMsE': S \subset 'C_Ms(E^`(1)). have [H hallH cHE'] := der_compl_cent_beta' maxM hallE. have [Q sylQ] := Sylow_exists q H; have [sQH qQ _] := and3P sylQ. have{cHE' sQH} cQE' := centsS sQH cHE'; have sE'E := der_sub 1 E. have [nMsE' coMsE'] := (coprimegS sE'E coMsE, subset_trans sE'E nMsE). have{H hallH} sylQ := subHall_Sylow hallH b'q sylQ. have nSE' := subset_trans sE'E nSE; have nQE' := cents_norm cQE'. have [x cE'x ->] := coprime_Hall_trans coMsE' nMsE' solMs sylS nSE' sylQ nQE'. by rewrite conj_subG // subsetI (pHall_sub sylQ) centsC. without loss{qX} sXS: X sXcMsE1 not_sXMs' / X \subset S. have [nMsE1 coMsE1 IH] := (subset_trans sE1E nMsE, coprimegS sE1E coMsE). have [nSE1 [sXMs cE1X]] := (subset_trans sE1E nSE, subsetIP sXcMsE1). have [|Q [sylQ nQE1 sXQ]] := coprime_Hall_subset nMsE1 coMsE1 solMs sXMs qX. by rewrite cents_norm // centsC. have [//|x cE1x defS] := coprime_Hall_trans nMsE1 _ solMs sylS nSE1 sylQ nQE1. have Ms_x: x \in Ms by case/setIP: cE1x. rewrite -(conjs1g x^-1) -sub_conjg IH //; last by rewrite defS conjSg. by rewrite -(conjGid cE1x) conjSg. by rewrite -(normsP (der_norm 1 _) x) ?conjSg. have [sXMs cE1X] := subsetIP sXcMsE1. have [_ [E3 hallE3]] := ex_tau13_compl hallE. have{hallE3} [E2 hallE2 complEi] := ex_tau2_compl hallE hallE1 hallE3. have{not_sXMs' E3 complEi} ntE2: E2 :!=: 1. apply: contraNneq not_sXMs' => E2_1. have [[sE3E' _] _ _ [defE _] _] := sigma_compl_context maxM complEi. have [sCMsE_Ms' _ _] := sigma_compl_embedding maxM hallE. have{defE} [_ defE _ _] := sdprodP defE; rewrite E2_1 sdprod1g in defE. rewrite (subset_trans _ sCMsE_Ms') // -defE centM setIA subsetI. by rewrite (subset_trans (subset_trans sXS sScMsE')) ?setIS ?centS. have{ntE2 E2 hallE2} [p p_pr t2p]: exists2 p, prime p & p \in \tau2(M). have [[p p_pr rE2] [_ t2E2 _]] := (rank_witness E2, and3P hallE2). by exists p; rewrite ?(pnatPpi t2E2) // -p_rank_gt0 -rE2 rank_gt0. have [A Ep2A Ep2A_M] := ex_tau2Elem hallE t2p. have [_ _ tiCMsA _ _] := tau2_context maxM t2p Ep2A_M. have [[nsAE _] _ _ _] := tau2_compl_context maxM hallE t2p Ep2A. have [sAE abelA _] := pnElemP Ep2A; have [pA cAA _] := and3P abelA. have cCAE1_X: X \subset 'C('C_A(E1)). rewrite centsC; apply/subsetP=> y; case/setIP=> Ay cE1y. have [-> | nty] := eqVneq y 1; first exact: group1. have oY: #[y] = p := abelem_order_p abelA Ay nty. have [r _ rE1] := rank_witness E1. have{} rE1: 'r_r(E1) > 0 by rewrite -rE1 rank_gt0. have [R ErR] := p_rank_geP rE1; have{ErR} [sRE1 abelR dimR] := pnElemP ErR. have t1r: r \in \tau1(M) by rewrite (pnatPpi t1E1) -?p_rank_gt0. have ErR: R \in 'E_r^1(E) by rewrite !inE abelR dimR (subset_trans sRE1). have EpY: <[y]>%G \in 'E_p^1('C_E(R)). rewrite p1ElemE // !inE -oY eqxx subsetI (centsS sRE1) cycle_subG //=. by rewrite (subsetP sAE). rewrite -sub_cent1 -cent_cycle (subset_trans sXcMsE1) //. apply: subset_trans (setIS _ (centS sRE1)) _. rewrite -subsetIidl setIAC subsetI subsetIr andbT. exact: cent_tau1Elem_Msigma t1r ErR EpY. have nAE1 := subset_trans sE1E (normal_norm nsAE). have coAE1: coprime #|A| #|E1|. by apply: pnat_coprime pA (pi_p'group t1E1 (contraL _ t2p)); apply: tau2'1. rewrite -tiCMsA -(coprime_cent_prod nAE1 coAE1) ?abelian_sol // centM setIA. rewrite subsetI cCAE1_X (subset_trans (subset_trans sXS sScMsE')) ?setIS //. by rewrite centS ?commgSS. 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)