proposition: Corollary beta'_cent_Sylow p q X : p \notin \beta(M) -> q \notin \beta(M) -> q.-group X -> (p != q) && (X \subset M^`(1)) || (p < q) && (X \subset M) -> [/\ exists2 P, p.-Sylow(M`_\sigma) (gval P) & X \subset 'C(P), p \in \alpha(M) -> 'C_M(X)%G \in 'U & q.-Sylow(M^`(1)) X -> exists2 P, p.-Sylow(M^`(1)) (gval P) & P \subset 'N_M(X)^`(1)].
proof: Proof. move=> b'p b'q qX q'p_sXM'; pose pq : nat_pred := pred2 p q. have [q'p sXM]: p \in q^' /\ X \subset M. case/orP: q'p_sXM' => /andP[q'p /subset_trans-> //]. by rewrite !inE neq_ltn q'p. have sXM'M: X <*> M^`(1) \subset M by rewrite join_subG sXM. have solXM': solvable (X <*> M^`(1)) := solvableS sXM'M solM. have pqX: pq.-group X by rewrite (pi_pgroup qX) ?inE ?eqxx ?orbT. have{solXM' pqX} [W /= hallW sXW] := Hall_superset solXM' (joing_subl _ _) pqX. have [sWXM' pqW _] := and3P hallW; have sWM := subset_trans sWXM' sXM'M. have{b'q} b'W: \beta(M)^'.-group W. by apply: sub_pgroup pqW => r /pred2P[]->; [apply: b'p | apply: b'q]. have nilM'W: nilpotent (M^`(1) :&: W). by rewrite beta'_der1_nil ?subsetIl ?(pgroupS (subsetIr _ _)). have{nilM'W} nilW: nilpotent W. do [case/orP: q'p_sXM'=> /andP[]] => [_ sXM' | lt_pq _]. by rewrite -(setIidPr sWXM') (joing_idPr sXM'). pose Wq := 'O_p^'(M) :&: W; pose Wp := 'O_p(M^`(1) :&: W). have nMp'M := char_norm (pcore_char p^' M). have nMp'W := subset_trans sWM nMp'M. have sylWq: q.-Sylow(W) Wq. have [sWqMp' sWp'W] := subsetIP (subxx Wq). have [Q sylQ] := Sylow_exists q W; have [sQW qQ _] := and3P sylQ. rewrite [Wq](sub_pHall sylQ _ _ (subsetIr _ W)) //= -/Wq. apply/pgroupP=> r r_pr r_dv_Wp'. have:= pgroupP (pgroupS sWqMp' (pcore_pgroup _ _)) r r_pr r_dv_Wp'. by apply/implyP; rewrite implyNb; apply: (pgroupP (pgroupS sWp'W pqW)). have [[_ _ max_p] sQM] := (beta_max_pdiv b'p, subset_trans sQW sWM). rewrite subsetI sQW -quotient_sub1 ?(subset_trans sQM nMp'M) //. apply: contraLR lt_pq; rewrite -leqNgt andbT subG1 -rank_gt0. rewrite (rank_pgroup (quotient_pgroup _ qQ)) p_rank_gt0 => piQb_q. exact: max_p (piSg (quotientS _ sQM) piQb_q). have nM'W: W \subset 'N(M^`(1)) by rewrite (subset_trans sWM) ?der_norm. have qWWM': q.-group (W / (M^`(1) :&: W)). rewrite (isog_pgroup _ (second_isog _)) ?(pgroupS (quotientS _ sWXM')) //=. by rewrite (quotientYidr (subset_trans sXW nM'W)) quotient_pgroup. have{qWWM'} sylWp: p.-Sylow(W) Wp. rewrite /pHall pcore_pgroup gFsub_trans ?subsetIr //=. rewrite -(Lagrange_index (subsetIr _ _) (pcore_sub _ _)) pnatM //. rewrite -(divgS (pcore_sub _ _)) -card_quotient ?normsI ?normG //= -pgroupE. rewrite (pi_p'group qWWM') //= -(dprod_card (nilpotent_pcoreC p nilM'W)). by rewrite mulKn ?cardG_gt0 // -pgroupE pcore_pgroup. have [[sWqW qWq _] [sWpW pWp _]] := (and3P sylWq, and3P sylWp). have <-: Wp * Wq = W. apply/eqP; rewrite eqEcard mul_subG //= -(partnC q (cardG_gt0 W)). rewrite (coprime_cardMg (p'nat_coprime (pi_pnat pWp _) qWq)) //. rewrite (card_Hall sylWp) (card_Hall sylWq) -{2}(part_pnat_id pqW) -partnI. rewrite mulnC (@eq_partn _ p) // => r. by rewrite !inE andb_orl andbN orbF; apply: andb_idr; move/eqP->. apply: nilpotentS (mul_subG _ _) (Fitting_nil W). rewrite Fitting_max ?(pgroup_nil pWp) //. by rewrite gFnormal_trans //= setIC norm_normalI. by rewrite Fitting_max ?(pgroup_nil qWq) //= setIC norm_normalI. have part1: exists2 P : {group gT}, p.-Sylow(M`_\sigma) P & X \subset 'C(P). have sMsXM' := subset_trans sMsM' (joing_subr X _). have nsMsXM': M`_\sigma <| X <*> M^`(1) := normalS sMsXM' sXM'M nsMsM. have sylWp: p.-Hall(M`_\sigma) ('O_p(W) :&: M`_\sigma). rewrite setIC (Sylow_setI_normal nsMsXM') //. exact: subHall_Sylow hallW (predU1l _ _) (nilpotent_pcore_Hall p nilW). have [_ _ cWpWp' _] := dprodP (nilpotent_pcoreC p nilW). exists ('O_p(W) :&: M`_\sigma)%G; rewrite ?(centSS _ _ cWpWp') ?subsetIl //. by rewrite (sub_Hall_pcore (nilpotent_pcore_Hall _ _)) ?(pi_p'group qX). split=> // [a_p | {part1}sylX]. have ltCMX_G := sub_proper_trans (subsetIl M 'C(X)) ltMG. have [P sylP cPX] := part1; have s_p := alpha_sub_sigma maxM a_p. have{} sylP := subHall_Sylow hallMs s_p sylP. apply: rank3_Uniqueness ltCMX_G (leq_trans a_p _). by rewrite -(rank_Sylow sylP) rankS //= subsetI (pHall_sub sylP) // centsC. do [move: sWXM'; rewrite (joing_idPr (pHall_sub sylX)) => sWM'] in hallW. have nMbX: X \subset 'N(M`_\beta) := subset_trans sXM (normal_norm nsMbM). have nsMbXM : M`_\beta <*> X <| M. rewrite -{2}(quotientGK nsMbM) -quotientYK ?cosetpre_normal //=. rewrite (eq_Hall_pcore _ (quotient_pHall nMbX sylX)); last first. exact: nilpotent_pcore_Hall Mbeta_quo_nil. by rewrite gFnormal_trans ?quotient_normal ?gFnormal. pose U := 'N_M(X); have defM: M`_\beta * U = M. have sXU : X \subset U by rewrite subsetI sXM normG. rewrite -[U](mulSGid sXU) /= -/U mulgA -norm_joinEr //. apply: Frattini_arg nsMbXM (pHall_subl (joing_subr _ X) _ sylX). by rewrite join_subG Mbeta_der1 (pHall_sub sylX). have sWpU: 'O_p(W) \subset U. rewrite gFsub_trans // subsetI sWM normal_norm //=. have sylX_W: q.-Sylow(W) X := pHall_subl sXW sWM' sylX. by rewrite (eq_Hall_pcore (nilpotent_pcore_Hall q nilW) sylX_W) pcore_normal. have sylWp: p.-Sylow(M^`(1)) 'O_p(W). exact: subHall_Sylow hallW (predU1l _ _) (nilpotent_pcore_Hall p nilW). exists 'O_p(W)%G; rewrite //= -(setIidPl (pHall_sub sylWp)). rewrite (pprod_focal_coprime defM) ?pcore_normal ?subsetIr //. exact: pnat_coprime (pcore_pgroup _ _) (pi_pnat (pcore_pgroup _ _) _). 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)