proposition: Proposition sub'cent_sigma_rank1 K : K \subset M -> sigma'.-group K -> 'r('C_K(M`_\sigma)) <= 1.
proof: Proof. move=> sKM sg'K; rewrite leqNgt; apply/rank_geP=> [[A /nElemP[p Ep2A]]]. have p_pr := pnElem_prime Ep2A. have [sACKMs abelA dimA] := pnElemP Ep2A; rewrite subsetI centsC in sACKMs. have{sACKMs} [sAK cAMs]: A \subset K /\ M`_\sigma \subset 'C(A) := andP sACKMs. have sg'p: p \in sigma'. by rewrite (pgroupP (pgroupS sAK sg'K)) // (card_pnElem Ep2A) dvdn_mull. have [Ms1 | [q q_pr q_dvd_Ms]] := trivgVpdiv M`_\sigma. by case/eqP: (Msigma_neq1 maxM). have sg_q: q \in \sigma(M) := pgroupP (pcore_pgroup _ _) _ q_pr q_dvd_Ms. have neq_pq: p != q by apply: contraNneq sg'p => ->. have [Q sylQ] := Sylow_exists q M`_\sigma; have [sQMs qQ _] := and3P sylQ. have cAQ: Q \subset 'C(A) := subset_trans sQMs cAMs. have{q_dvd_Ms} q_dv_CA: q %| #|'C(A)|. rewrite (dvdn_trans _ (cardSg cAQ)) // -(part_pnat_id (pnat_id q_pr)). by rewrite (card_Hall sylQ) partn_dvd. have{cAQ} maxQ: Q \in |/|*(A; q). rewrite inE; apply/maxgroupP; rewrite qQ cents_norm 1?centsC //. split=> // Y /andP[qY _] sQY; apply: sub_pHall qY sQY (subsetT Y). by rewrite (subHall_Sylow (Msigma_Hall_G maxM)). have sNQM: 'N(Q) \subset M. by rewrite (norm_sigma_Sylow sg_q) // (subHall_Sylow hallMs). have rCAle2: 'r('C(A)) <= 2. apply: contraR (sigma'_not_uniq sKM sg'K); rewrite -ltnNge => rCAgt2. apply: uniq_mmaxS sAK (sub_mmax_proper maxM sKM) _. by apply: cent_rank3_Uniqueness rCAgt2; rewrite (rank_abelem abelA) dimA. have max2A: A \in 'E_p^2(G) :&: 'E*_p(G). rewrite 3!inE subsetT abelA dimA; apply/pmaxElemP; rewrite inE subsetT. split=> // Y /pElemP[_ abelY /eqVproper[]//ltAY]. have [pY cYY _] := and3P abelY. suffices: 'r_p('C(A)) > 2 by rewrite ltnNge (leq_trans (p_rank_le_rank p _)). rewrite -dimA (leq_trans (properG_ltn_log pY ltAY)) //. by rewrite logn_le_p_rank // inE centsC (subset_trans (proper_sub ltAY)). have{rCAle2 cAMs} Ma1: M`_\alpha = 1. apply: contraTeq rCAle2; rewrite -rank_gt0 -ltnNge. have [r _ ->] := rank_witness M`_\alpha; rewrite p_rank_gt0. move/(pnatPpi (pcore_pgroup _ _))=> a_r; apply: (leq_trans a_r). have [R sylR] := Sylow_exists r M`_\sigma. have sylR_M: r.-Sylow(M) R. by rewrite (subHall_Sylow (Msigma_Hall maxM)) ?alpha_sub_sigma. rewrite -(p_rank_Sylow sylR_M) (p_rank_Sylow sylR). by rewrite (leq_trans (p_rank_le_rank r _)) // rankS // centsC. have{Ma1} nilM': nilpotent M^`(1). by rewrite (isog_nil (quotient1_isog _)) -Ma1 Malpha_quo_nil. have{max2A maxQ neq_pq q_dv_CA} [P [sylP sAP] sPNQ']: exists2 P : {group gT}, p.-Sylow(G) P /\ A \subset P & P \subset 'N(Q)^`(1). - by case/(max_normed_2Elem_signaliser neq_pq): maxQ => // P ? []; exists P. have{sNQM} defP: 'O_p(M^`(1)) = P. rewrite (nilpotent_Hall_pcore nilM' (pHall_subl _ _ sylP)) ?subsetT //. by rewrite (subset_trans sPNQ') ?dergS. have nsPM: P <| M by rewrite -defP !gFnormal_trans. have sPM := normal_sub nsPM. case/exists_inP: sg'p; exists P; first exact: pHall_subl (subsetT M) sylP. by rewrite (mmax_normal maxM) // -rank_gt0 ltnW // -dimA -rank_abelem ?rankS. 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)