proposition: Corollary sigma_Jsub M Y : M \in 'M -> \sigma(M).-group Y -> Y :!=: 1 -> [/\ exists x, Y :^ x \subset M`_\sigma & forall E p H, \sigma(M)^'.-Hall(M) E -> p \in \pi(E) -> p \notin \beta(G) -> H \in 'M(Y) -> gval H \notin M :^: G -> [/\ 'r_p('N_H(Y)) <= 1 & p \in \tau1(M) -> p \notin \pi(('N_H(Y))^`(1))]].
proof: Proof. move=> maxM sM_Y ntY. have ltYG: Y \proper G. have ltMsG: M`_\sigma \proper G. exact: sub_proper_trans (pcore_sub _ _) (mmax_proper maxM). rewrite properEcard subsetT (leq_ltn_trans _ (proper_card ltMsG)) //. rewrite dvdn_leq ?cardG_gt0 // (card_Hall (Msigma_Hall_G maxM)). by rewrite -(part_pnat_id sM_Y) partn_dvd // cardSg ?subsetT. have [q q_pr rFY] := rank_witness 'F(Y). have [X [ntX qX charX]]: exists X, [/\ gval X :!=: 1, q.-group X & X \char Y]. exists ('O_q(Y))%G; rewrite pcore_pgroup pcore_char //. rewrite -rank_gt0 /= -p_core_Fitting. rewrite (rank_Sylow (nilpotent_pcore_Hall q (Fitting_nil Y))) -rFY. by rewrite rank_gt0 (trivg_Fitting (mFT_sol ltYG)). have sXY: X \subset Y := char_sub charX. have sMq: q \in \sigma(M). apply: (pnatPpi (pgroupS sXY sM_Y)). by rewrite -p_rank_gt0 -(rank_pgroup qX) rank_gt0. without loss sXMs: M maxM sM_Y sMq / X \subset M`_\sigma. move=> IH; have [Q sylQ] := Sylow_exists q M`_\sigma. have sQMs := pHall_sub sylQ. have sylQ_G := subHall_Sylow (Msigma_Hall_G maxM) sMq sylQ. have [x Gx sXQx] := Sylow_subJ sylQ_G (subsetT X) qX. have: X \subset M`_\sigma :^ x by rewrite (subset_trans sXQx) ?conjSg. rewrite -MsigmaJ => /IH; rewrite sigmaJ mmaxJ (eq_pgroup _ (sigmaJ _ _)). case=> // [[y sYyMx] parts_ab]. split=> [|E p H hallE piEp bG'p maxY_H notMGH]. by exists (y * x^-1); rewrite conjsgM sub_conjgV -MsigmaJ. have:= parts_ab (E :^ x)%G p H; rewrite tau1J /= cardJg pHallJ2. rewrite (eq_pHall _ _ (eq_negn (sigmaJ _ _))). by rewrite 2!orbit_sym (orbit_eqP (mem_orbit _ _ _)) //; apply. have pre_part_a E p H: \sigma(M)^'.-Hall(M) E -> p \in \pi(E) -> H \in 'M(Y) -> gval H \notin M :^: G -> 'r_p(H :&: M) <= 1. - move=> hallE piEp /setIdP[maxH sYH] notMGH; rewrite leqNgt. apply: contra ntX => /p_rank_geP[A /pnElemP[/subsetIP[sAH sAM] abelA dimA]]. have{abelA dimA} Ep2A: A \in 'E_p^2(M) by apply/pnElemP. have rpMgt1: 'r_p(M) > 1 by apply/p_rank_geP; exists A. have t2Mp: p \in \tau2(M). move: piEp; rewrite (partition_pi_sigma_compl maxM hallE) orbCA orbC. by rewrite -2!andb_orr orNb eqn_leq leqNgt rpMgt1 !andbF. have sM'p := pnatPpi (pHall_pgroup hallE) piEp. have [_ _ _ tiMsH _] := tau2_context maxM t2Mp Ep2A. rewrite -subG1 -(tiMsH H); first by rewrite subsetI sXMs (subset_trans sXY). by rewrite 3!inE maxH (contra_orbit _ _ notMGH). have [sNX_M | not_sNX_M] := boolP ('N(X) \subset M). have sNY_M: 'N(Y) \subset M := subset_trans (char_norms charX) sNX_M. split=> [|E p H hallE piEp bG'p maxY_H notMGH]; last split. - exists 1; rewrite act1 (sub_Hall_pcore (Msigma_Hall maxM)) //. exact: subset_trans (normG Y) sNY_M. - rewrite (leq_trans (p_rankS p (setIS H sNY_M))) ?(pre_part_a E) //. case/and3P=> _ _; apply: contra; rewrite mem_primes => /and3P[_ _ pM']. by apply: dvdn_trans pM' (cardSg (dergS 1 _)); rewrite subIset ?sNY_M ?orbT. have [L maxNX_L] := mmax_exists (mFT_norm_proper ntX (mFT_pgroup_proper qX)). have [maxL sNX_L] := setIdP maxNX_L. have{} maxNX_L: L \in 'M('N(X)) :\ M. by rewrite 2!inE maxNX_L andbT; apply: contraNneq not_sNX_M => <-. have sXM := subset_trans sXMs (pcore_sub _ M). have [notMGL _ embedL] := sigma_subgroup_embedding maxM sMq sXM qX ntX maxNX_L. pose K := (if q \in \sigma(L) then L`_\beta else L`_\sigma)%G. have sM'K: \sigma(M)^'.-group K. rewrite orbit_sym in notMGL. rewrite /K; case: (boolP (q \in _)) embedL => [sLq _ | sL'q [t2Lq _ _]]. have [_ TIaLsM _] := sigma_disjoint maxL maxM notMGL. apply: sub_pgroup (pcore_pgroup _ _) => p bLp. by apply: contraFN (TIaLsM p) => /= sMp; rewrite inE /= beta_sub_alpha. have [F hallF] := ex_sigma_compl maxL. have [A Ep2A _] := ex_tau2Elem hallF t2Lq. have [_ _ _ TIsLs] := tau2_compl_context maxL hallF t2Lq Ep2A. have{TIsLs} [_ TIsLsM] := TIsLs M maxM notMGL. apply: sub_pgroup (pcore_pgroup _ _) => p sLp. by apply: contraFN (TIsLsM p) => /= sMp; rewrite inE /= sLp. have defL: K * (M :&: L) = L. rewrite /K; case: (q \in _) embedL => [] [] // _ _. by move/(sdprod_Hall_pcoreP (Msigma_Hall maxL)); case/sdprodP. have sYL := subset_trans (char_norm charX) sNX_L. have [x sYxMs]: exists x, Y :^ x \subset M`_\sigma. have solML := solvableS (subsetIl M L) (mmax_sol maxM). have [H hallH] := Hall_exists \sigma(M) solML. have [sHM sHL] := subsetIP (pHall_sub hallH). have hallH_L: \sigma(M).-Hall(L) H. rewrite pHallE sHL -defL -LagrangeMr partnM ?cardG_gt0 //. rewrite -(card_Hall hallH) part_p'nat ?mul1n //=. exact: pnat_dvd (dvdn_indexg _ _) sM'K. have [x _ sYxH]:= Hall_Jsub (mmax_sol maxL) hallH_L sYL sM_Y. exists x; rewrite (sub_Hall_pcore (Msigma_Hall maxM)) ?pgroupJ //. exact: subset_trans sYxH sHM. split=> [|E p H hallE piEp bG'p maxY_H notMGH]; first by exists x. have p'K: p^'.-group K. have bL'p: p \notin \beta(L). by rewrite -predI_sigma_beta // negb_and bG'p orbT. rewrite /K; case: (q \in _) embedL => [_ | [_ bLp _]]. by rewrite (pi_p'group (pcore_pgroup _ _)). rewrite (pi_p'group (pcore_pgroup _ _)) //; apply: contra bL'p => /= sLp. by rewrite bLp // inE /= (piSg (pHall_sub hallE)). have sNHY_L: 'N_H(Y) \subset L. by rewrite subIset ?(subset_trans (char_norms charX)) ?orbT. rewrite (leq_trans (p_rankS p sNHY_L)); last first. have [P sylP] := Sylow_exists p (M :&: L). have [_ sPL] := subsetIP (pHall_sub sylP). have{sPL} sylP_L: p.-Sylow(L) P. rewrite pHallE sPL -defL -LagrangeMr partnM ?cardG_gt0 //. rewrite -(card_Hall sylP) part_p'nat ?mul1n //=. exact: pnat_dvd (dvdn_indexg _ _) p'K. rewrite -(p_rank_Sylow sylP_L) {P sylP sylP_L}(p_rank_Sylow sylP). by rewrite /= setIC (pre_part_a E) // inE maxL. split=> // t1Mp; rewrite (contra ((piSg (dergS 1 sNHY_L)) p)) // -p'groupEpi. have nsKL: K <| L by rewrite /K; case: ifP => _; apply: pcore_normal. have [sKL nKL] := andP nsKL; have nKML := subset_trans (subsetIr M L) nKL. suffices: p^'.-group (K * (M :&: L)^`(1)). rewrite -norm_joinEr ?gFsub_trans //; apply: pgroupS => /=. rewrite norm_joinEr -?quotientSK ?gFsub_trans //= !quotient_der //. by rewrite -[in L / K]defL quotientMidl. rewrite pgroupM p'K (pgroupS (dergS 1 (subsetIl M L))) // p'groupEpi. by rewrite mem_primes andbA andbC negb_and; case/and3P: t1Mp => _ _ ->. 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)