proposition: Theorem cent_alpha'_uniq X : X \subset M -> \alpha(M)^'.-group X -> 'r('C_(M`_\alpha)(X)) >= 2 -> 'C_M(X)%G \in 'U.
proof: Proof. have ltM_G := sub_proper_trans (subsetIl M _) ltMG. move=> sXM a'X; have [p p_pr -> rCX] := rank_witness 'C_(M`_\alpha)(X). have{rCX} [B EpB] := p_rank_geP rCX; have{EpB} [sBCX abelB dimB] := pnElemP EpB. have [[sBMa cXB] [pB cBB _]] := (subsetIP sBCX, and3P abelB). have rMa: 1 < 'r_p(M`_\alpha) by rewrite -dimB -p_rank_abelem ?p_rankS. have{rMa} a_p: p \in \alpha(M) by rewrite (pnatPpi aMa) // -p_rank_gt0 ltnW. have nBX: X \subset 'N(B) by rewrite cents_norm // centsC. have coMaX: coprime #|M`_\alpha| #|X| := pnat_coprime aMa a'X. have [sMaM nMaM] := andP nsMaM; have solMa := solvableS sMaM solM. have nMaX := subset_trans sXM nMaM. have [P [sylP nPX sBP]] := coprime_Hall_subset nMaX coMaX solMa sBMa pB nBX. have [sPMa pP _] := and3P sylP; have sPM := subset_trans sPMa sMaM. have EpCB: B \in 'E_p^2('C_P(B)) by rewrite !inE subsetI sBP abelB dimB !andbT. have: 1 < 'r_p('C_P(B)) by apply/p_rank_geP; exists B. rewrite leq_eqVlt; case: ltngtP => // rCPB _. apply: (uniq_mmaxS (subset_trans sBCX (setSI _ sMaM))) => //=. have pCPB := pgroupS (subsetIl P 'C(B)) pP; rewrite -rank_pgroup // in rCPB. have: 2 < 'r('C(B)) by rewrite (leq_trans rCPB) ?rankS ?subsetIr. by apply: cent_rank3_Uniqueness; rewrite -dimB -rank_abelem. have cPX: P \subset 'C(X). have EpPB: B \in 'E_p(P) by apply/pElemP. have coPX: coprime #|P| #|X| := coprimeSg sPMa coMaX. rewrite centsC (coprime_odd_faithful_cent_abelem EpPB) ?mFT_odd //. rewrite -(setIid 'C(B)) setIA (pmaxElem_LdivP p_pr _) 1?centsC //. by rewrite (subsetP (p_rankElem_max _ _)) -?rCPB. have sylP_M := subHall_Sylow Malpha_Hall a_p sylP. have{sylP_M} rP: 2 < 'r(P) by rewrite (rank_Sylow sylP_M). by rewrite rank3_Uniqueness ?(leq_trans rP (rankS _)) //= subsetI sPM. 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) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9)