proposition: Theorem tau13_regular M E E1 E2 E3 p P : M \in 'M -> sigma_complement M E E1 E2 E3 -> P \in 'E_p^1(E1) -> ~~ (P \subset 'C(E3)) -> [/\ semiregular E3 E1, semiregular M`_\sigma E3 & 'C_(M`_\sigma)(P) != 1].
proof: Proof. move=> maxM complEi EpP not_cE3P. have nsMsM: M`_\sigma <| M := pcore_normal _ M; have [sMsM nMsM] := andP nsMsM. have [hallMs sMaMs] := (Msigma_Hall maxM, Malpha_sub_Msigma maxM). have [[sE3E' nsE3E] _ [_ cycE3] _ _] := sigma_compl_context maxM complEi. have [hallE hallE1 _ hallE3] := complEi. have [[_ sM_Ms _] [sEM sM'E _]] := (and3P hallMs, and3P hallE). have [[sE1E t1E1 _] [sE3E t3E3 _] _] := (and3P hallE1, and3P hallE3). have [sPE1 abelP dimP] := pnElemP EpP; have [pP _ _] := and3P abelP. have [ntP t1MP] := (nt_pnElem EpP isT, pgroupS sPE1 t1E1). have sPE := subset_trans sPE1 sE1E; have sPM := subset_trans sPE sEM. have piPp: p \in \pi(P) by rewrite -p_rank_gt0 p_rank_abelem ?dimP. have t1Mp: p \in \tau1(M) := pnatPpi t1MP piPp. have [Q sylQ not_cPQ]: exists2 Q, Sylow E3 (gval Q) & ~~ (P \subset 'C(Q)). apply/exists_inP; rewrite -negb_forall_in; apply: contra not_cE3P. move/forall_inP=> cPE3; rewrite centsC -(Sylow_gen E3) gen_subG. by apply/bigcupsP=> Q sylQ; rewrite centsC cPE3. have{sylQ} [q q_pr sylQ] := SylowP _ _ sylQ; have [sQE3 qQ _] := and3P sylQ. have ntQ: Q :!=: 1 by apply: contraNneq not_cPQ => ->; apply: cents1. have t3Mq: q \in \tau3(M). by rewrite (pnatPpi t3E3) // -p_rank_gt0 -(rank_Sylow sylQ) rank_gt0. have nQP: P \subset 'N(Q). rewrite (subset_trans sPE) ?normal_norm //. by rewrite (char_normal_trans _ nsE3E) ?sub_cyclic_char. have regPQ: 'C_Q(P) = 1. apply: contraNeq not_cPQ; rewrite setIC => /meet_Ohm1. rewrite setIC => /prime_meetG/=/implyP. rewrite (Ohm1_cyclic_pgroup_prime (cyclicS sQE3 cycE3) qQ) // q_pr centsC. apply: (coprime_odd_faithful_Ohm1 qQ) nQP _ (mFT_odd _). exact: sub_pnat_coprime tau3'1 (pgroupS sQE3 t3E3) t1MP. have sQE' := subset_trans sQE3 sE3E'. have sQM := subset_trans (subset_trans sQE3 sE3E) sEM. have [L maxNL] := mmax_exists (mFT_norm_proper ntQ (mFT_pgroup_proper qQ)). have [maxL sNQL] := setIdP maxNL; have sQL := subset_trans (normG Q) sNQL. have notMGL: gval L \notin M :^: G. by apply: mmax_norm_notJ maxM maxL qQ sQM sNQL _; rewrite t3Mq !orbT. have [ntCMaP tiCMaQP]: 'C_(M`_\alpha)(P) != 1 /\ 'C_(M`_\alpha)(Q <*> P) = 1. have EpMP: P \in 'E_p^1(M) by apply/pnElemP. have p'q: q != p by apply: contraNneq (tau3'1 t1Mp) => <-. have [|_ [] //] := cent_Malpha_reg_tau1 maxM t1Mp p'q EpMP ntQ nQP regPQ. by apply: contraTneq maxNL => ->; rewrite inE (contra_orbit _ _ notMGL). have sM'q: q \in \sigma(M)^' by case/andP: t3Mq. exact: subHall_Sylow hallE sM'q (subHall_Sylow hallE3 t3Mq sylQ). split=> [x E1x | x E3x |]; last exact: subG1_contra (setSI _ sMaMs) ntCMaP. apply: contraNeq ntCMaP => ntCE3X. have prE31: semiprime M`_\sigma (E3 <*> E1). apply: tau13_primact_Msigma maxM complEi _ => regE13. by rewrite regE13 ?eqxx in ntCE3X. rewrite -subG1 -tiCMaQP /= -(setIidPl sMaMs) -!setIA setIS //. rewrite (cent_semiprime prE31 _ ntP) ?setIS ?centS //=. by rewrite -!genM_join genS ?mulgSS. by rewrite sub_gen // subsetU // sPE1 orbT. have prE3 := tau3_primact_Msigma maxM hallE hallE3. apply/eqP; apply/idPn; rewrite prE3 {x E3x}// -rank_gt0. have [u _ -> ruC] := rank_witness 'C_(M`_\sigma)(E3). have sCMs := subsetIl M`_\sigma 'C(E3). have sMu: u \in \sigma(M) by rewrite (pnatPpi (pgroupS sCMs _)) -?p_rank_gt0. have nCE: E \subset 'N('C_(M`_\sigma)(E3)). by rewrite normsI ?norms_cent ?(normal_norm nsE3E) // (subset_trans sEM). have coCE := coprimeSg sCMs (pnat_coprime (pcore_pgroup _ _) sM'E). have solC := solvableS (subset_trans sCMs sMsM) (mmax_sol maxM). have{nCE coCE solC} [U sylU nUE] := coprime_Hall_exists u nCE coCE solC. have ntU: U :!=: 1 by rewrite -rank_gt0 (rank_Sylow sylU). have cMsL_Q: Q \subset 'C(M`_\sigma :&: L). have t13q: (q \in \tau1(M)) || (q \in \tau3(M)) by rewrite t3Mq orbT. have [-> //] := cent_norm_tau13_mmax maxM hallE t13q sQM qQ maxNL. by rewrite subsetI sQM. rewrite /= -(cent_semiprime prE3 sQE3 ntQ) in sylU. have [sUMs cQU] := subsetIP (pHall_sub sylU). have{cMsL_Q} sylU_MsL: u.-Sylow(M`_\sigma :&: L) U. apply: pHall_subl sylU; last by rewrite subsetI subsetIl centsC. by rewrite subsetI sUMs (subset_trans (cents_norm _) sNQL). have sylU_ML: u.-Sylow(M :&: L) U. apply: subHall_Sylow sMu sylU_MsL. by rewrite /= -(setIidPl sMsM) -setIA (setI_normal_Hall nsMsM) ?subsetIl. have [sUML uU _] := and3P sylU_ML; have{sUML} [sUM sUL] := subsetIP sUML. have [sNUM regPU]: 'N(U) \subset M /\ 'C_U(P) = 1. have [bMu | bM'u] := boolP (u \in \beta(M)). have [bM_U sMbMa] := (pi_pgroup uU bMu, Mbeta_sub_Malpha M). split; first by rewrite beta_norm_sub_mmax /psubgroup ?sUM. apply/trivgP; rewrite -tiCMaQP centY setIA setSI // subsetI cQU. by rewrite (subset_trans _ sMbMa) // (sub_Hall_pcore (Mbeta_Hall maxM)). have sylU_Ms: u.-Sylow(M`_\sigma) U. have [H hallH cHE'] := der_compl_cent_beta' maxM hallE. rewrite pHallE sUMs (card_Hall sylU) eqn_dvd. rewrite partn_dvd ?cardG_gt0 ?cardSg ?subsetIl //=. rewrite -(@partn_part u \beta(M)^') => [|v /eqnP-> //]. rewrite -(card_Hall hallH) partn_dvd ?cardG_gt0 ?cardSg //. by rewrite subsetI (pHall_sub hallH) centsC (subset_trans sQE'). split; first exact: norm_sigma_Sylow (subHall_Sylow hallMs sMu sylU_Ms). apply: contraNeq (contra_orbit _ _ notMGL); rewrite -rank_gt0. rewrite (rank_pgroup (pgroupS _ uU)) ?subsetIl // => /p_rank_geP[X] /=. rewrite -(setIidPr sUMs) setIAC pnElemI -setIdE => /setIdP[EuX sXU]. have [_ uniqU] := cent_cent_Msigma_tau1_uniq maxM hallE hallE1 sPE1 ntP EuX. by rewrite (eq_uniq_mmax (uniqU U sylU_Ms) maxL). have sPL := subset_trans nQP sNQL. have sPML: P \subset M :&: L by apply/subsetIP. have t1Lp: p \in \tau1(L). have not_cMsL_P: ~~ (P \subset 'C(M`_\sigma :&: L)). apply: contra ntU => cMsL_P; rewrite -subG1 -regPU subsetIidl. by rewrite centsC (centsS (pHall_sub sylU_MsL)). apply: contraR (not_cMsL_P) => t1L'p. have [piEp piLp] := (piSg sPE piPp, piSg sPL piPp). case: (Msigma_setI_mmax_central maxM hallE maxL piEp piLp) => // [|->] //. apply: contraNneq not_cMsL_P => /commG1P. by rewrite centsC; apply: subset_trans sPML. have EpMLP: P \in 'E_p^1(M :&: L) by apply/pnElemP. case: (@tau1_mmaxI_asymmetry M L p P q Q u U) => //. have [sylQ_E [sM'q _]] := (subHall_Sylow hallE3 t3Mq sylQ, andP t3Mq). have sylQ_M := subHall_Sylow hallE sM'q sylQ_E. have sQML: Q \subset M :&: L by apply/subsetIP. by rewrite (subset_trans sPE nUE) (pHall_subl sQML _ sylQ_M) ?subsetIl. 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)