proposition: Theorem sigma_partition M Mstar : M \in 'M -> Mstar \in 'M -> gval Mstar \notin M :^: G -> [predI \sigma(M) & \sigma(Mstar)] =i pred0.
proof: Proof. move: Mstar => L maxM maxL notMGL q; apply/andP=> [[/= sMq sLq]]. have [E hallE] := ex_sigma_compl maxM; have [sEM sM'E _] := and3P hallE. have [_ _ nMsE _] := sdprodP (sdprod_sigma maxM hallE). have coMsE: coprime #|M`_\sigma| #|E| := pnat_coprime (pcore_pgroup _ _) sM'E. have [|S sylS nSE] := coprime_Hall_exists q nMsE coMsE. exact: solvableS (pcore_sub _ _) (mmax_sol maxM). have [sSMs qS _] := and3P sylS. have sylS_M := subHall_Sylow (Msigma_Hall maxM) sMq sylS. have ntS: S :!=: 1. by rewrite -rank_gt0 (rank_Sylow sylS_M) p_rank_gt0 sigma_sub_pi. without loss sylS_L: L maxL sLq notMGL / q.-Sylow(L) S. have sylS_G := sigma_Sylow_G maxM sMq sylS_M. have [T sylT] := Sylow_exists q L; have sylT_G := sigma_Sylow_G maxL sLq sylT. have [x Gx ->] := Sylow_trans sylT_G (sigma_Sylow_G maxM sMq sylS_M). case/(_ (L :^ x)%G); rewrite ?mmaxJ ?sigmaJ ?pHallJ2 //. by rewrite (orbit_transl _ (mem_orbit 'Js L Gx)). have [[sSL _] [[E1 hallE1] [E3 hallE3]]] := (andP sylS_L, ex_tau13_compl hallE). have [E2 hallE2 complEi] := ex_tau2_compl hallE hallE1 hallE3. have E2_1: E2 :==: 1. apply: contraR ntS; rewrite -rank_gt0; have [p _ ->] := rank_witness E2. rewrite p_rank_gt0 => /(pnatPpi (pHall_pgroup hallE2))t2p. have [A Ep2A _] := ex_tau2Elem hallE t2p. have [_ _ _ ti_sM] := tau2_compl_context maxM hallE t2p Ep2A. rewrite -subG1; have [<- _] := ti_sM L maxL notMGL; rewrite subsetI sSMs /=. by rewrite (sub_Hall_pcore (Msigma_Hall maxL) sSL) (pi_pgroup qS). have: E1 :!=: 1 by have [_ -> //] := sigma_compl_context maxM complEi. rewrite -rank_gt0; have [p _ ->] := rank_witness E1; case/p_rank_geP=> P EpP. have [[sPE1 abelP dimP] [sE1E t1E1 _]] := (pnElemP EpP, and3P hallE1). have ntP: P :!=: 1 by rewrite (nt_pnElem EpP). have piPp: p \in \pi(P) by rewrite -p_rank_gt0 ?p_rank_abelem ?dimP. have t1Mp: p \in \tau1(M) by rewrite (pnatPpi _ (piSg sPE1 _)). have sPE := subset_trans sPE1 sE1E; have sPM := subset_trans sPE sEM. have [sNM sNL] := (norm_sigma_Sylow sMq sylS_M, norm_sigma_Sylow sLq sylS_L). have nSP := subset_trans sPE nSE; have sPL := subset_trans nSP sNL. have regPS: 'C_S(P) = 1. apply: contraNeq (contra_orbit _ _ notMGL); rewrite -rank_gt0. rewrite (rank_pgroup (pgroupS _ qS)) ?subsetIl //; case/p_rank_geP=> Q /=. rewrite -(setIidPr sSMs) setIAC pnElemI; case/setIdP=> EqQ _. have [_ uniqSq] := cent_cent_Msigma_tau1_uniq maxM hallE hallE1 sPE1 ntP EqQ. by rewrite (eq_uniq_mmax (uniqSq S sylS) maxL sSL). have t1Lp: p \in \tau1(L). have not_cMsL_P: ~~ (P \subset 'C(M`_\sigma :&: L)). apply: contra ntS => cMsL_P; rewrite -subG1 -regPS subsetIidl centsC. by rewrite (subset_trans cMsL_P) ?centS // subsetI sSMs. apply: contraR (not_cMsL_P) => t1L'p. have [piEp piLp] := (piSg sPE piPp, piSg sPL piPp). have [] := Msigma_setI_mmax_central maxM hallE maxL piEp piLp t1L'p _ notMGL. apply: contraNneq not_cMsL_P; move/commG1P; rewrite centsC. by apply: subset_trans; rewrite subsetI sPM. by move->; rewrite ?(abelem_pgroup abelP) // subsetI sPM. case: (@tau1_mmaxI_asymmetry M L p P q S q S) => //. by rewrite !inE subsetI sPM sPL abelP dimP. by rewrite (pHall_subl _ (subsetIl M L) sylS_M) // subsetI (pHall_sub sylS_M). 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)