proposition: Lemma primes_non_Fitting_Ftype M E q Q : M \in 'M_'F -> \sigma(M)^'.-Hall(M) E -> Q \in 'E_q^1(E) -> ~~ (Q \subset 'F(E)) -> exists2 Mstar, Mstar \in 'M & [\/ q \in \tau2(Mstar) /\ 'M('C(Q)) = [set Mstar] | q \in \kappa(Mstar) /\ Mstar \in 'M_'P1 ].
proof: Proof. move=> FmaxM hallE EqQ notsFE_Q; have [maxM k'M] := FtypeP _ FmaxM. have [sQE abelQ dimQ] := pnElemP EqQ; have [qQ _] := andP abelQ. have [q_pr oQ] := (pnElem_prime EqQ, card_pnElem EqQ : #|Q| = q). have t1Mq: q \in \tau1(M). have: q \in \pi(E) by rewrite -p_rank_gt0; apply/p_rank_geP; exists Q. rewrite (partition_pi_sigma_compl maxM hallE) => /or3P[// | t2q | t3q]. have [A EqA _] := ex_tau2Elem hallE t2q. have [[nsAE defA1] _ _ _] := tau2_compl_context maxM hallE t2q EqA. have sQA: Q \subset A by move: EqQ; rewrite defA1 => /pnElemP[]. rewrite (subset_trans sQA) ?Fitting_max // ?abelian_nil // in notsFE_Q. by have [_ abelA _] := pnElemP EqA; apply: abelem_abelian abelA. have [[E1 hallE1] [E3 hallE3]] := ex_tau13_compl hallE. have [E2 _ complEi] := ex_tau2_compl hallE hallE1 hallE3. have [[_ nsE3E] _ [_ cycE3] _ _] := sigma_compl_context maxM complEi. have sQE3: Q \subset E3 by rewrite (sub_normal_Hall hallE3) ?(pi_pgroup qQ). rewrite (subset_trans sQE3) ?Fitting_max ?abelian_nil // in notsFE_Q. exact: cyclic_abelian cycE3. have q'FE: q^'.-group 'F(E). have [R sylR sQR] := Sylow_superset sQE qQ; have [sRE qR _] := and3P sylR. have cycR: cyclic R. rewrite (odd_pgroup_rank1_cyclic qR) ?mFT_odd // (p_rank_Sylow sylR) //. by move: t1Mq; rewrite (tau1E maxM hallE) eqn_leq; case/and4P. rewrite -partG_eq1 -(card_Hall (Hall_setI_normal (Fitting_normal E) sylR)). have sRFER: R :&: 'F(E) \subset R := subsetIl _ _. apply: contraR notsFE_Q; rewrite -trivg_card1 => ntRFE. rewrite (subset_trans _ (subsetIr R _)) // -(cardSg_cyclic cycR) // oQ. by have [] := pgroup_pdiv (pgroupS sRFER qR) ntRFE. have cE'E': abelian E^`(1) := der_mmax_compl_abelian maxM hallE. pose K := [~: E, Q]; have cKK: abelian K by rewrite (abelianS (commgS E sQE)). have nsKE: K <| E by rewrite /normal commg_norml comm_subG. have q'K: q^'.-group K by rewrite (pgroupS _ q'FE) // Fitting_max ?abelian_nil. have [sKE nKE] := andP nsKE; have nKQ := subset_trans sQE nKE. have defKQ: [~: K, Q] = K. have nsKQ_E: K <*> Q <| E. rewrite -(quotientGK nsKE) -(quotientYK nKQ) cosetpre_normal /= -/K. by rewrite /normal quotientS // cents_norm // quotient_cents2r. have [_ sylQ] := coprime_mulGp_Hall (esym (norm_joinEr nKQ)) q'K qQ. have defE: K * 'N_E(Q) = E. rewrite -{2}(Frattini_arg nsKQ_E sylQ) /= norm_joinEr //= -/K -mulgA. by congr (K * _); rewrite mulSGid // subsetI sQE normG. have cQ_NEQ: [~: 'N_E(Q), Q] = 1. apply/trivgP; rewrite -(coprime_TIg (pnat_coprime qQ q'K)) subsetI. by rewrite commg_subr subsetIr commSg ?subsetIl. by rewrite {2}/K -defE commMG ?cQ_NEQ ?mulg1 1?normsR ?subsetIr ?subIset ?nKE. have [sEM s'E _] := and3P hallE; have sQM := subset_trans sQE sEM. have [sKM s'K] := (subset_trans sKE sEM, pgroupS sKE s'E). have regQ: 'C_(M`_\sigma)(Q) = 1. apply/eqP; apply: contraFT (k'M q) => nregQ. have EqQ_M: Q \in 'E_q^1(M) by apply/pnElemP. by rewrite unlock inE /= inE /= t1Mq; apply/exists_inP; exists Q. have nsKM: K <| M. have [s'q _] := andP t1Mq. have EqQ_NK: Q \in 'E_q^1('N_M(K)) by apply/pnElemP; rewrite subsetI sQM. have:= commG_sigma'_1Elem_cyclic maxM sKM s'K s'q EqQ_NK regQ q'K cKK. by rewrite defKQ; case. have ntK: K != 1. apply: contraNneq notsFE_Q => /commG1P cQE. by rewrite Fitting_max ?(pgroup_nil qQ) // /normal sQE cents_norm. pose p := pdiv #|K|; have p_pr: prime p by rewrite pdiv_prime ?cardG_gt1. have piKp: p \in \pi(K) by rewrite pi_pdiv cardG_gt1. have t2Mp: p \in \tau2(M). have s'p := pnatPpi s'K piKp. have sylKp: p.-Sylow(K) 'O_p(K) := nilpotent_pcore_Hall p (abelian_nil cKK). have ntKp: 'O_p(K) != 1 by rewrite -rank_gt0 (rank_Sylow sylKp) p_rank_gt0. rewrite inE /= s'p ?(sigma'_norm_mmax_rank2 maxM s'p (pHall_pgroup sylKp)) //. by rewrite (mmax_normal maxM) ?gFnormal_trans. have [A EpA _] := ex_tau2Elem hallE t2Mp. have [sAE /andP[pA _] dimA] := pnElemP EpA. have [[nsAE _] _ _ _] := tau2_compl_context maxM hallE t2Mp EpA. have nAQ := subset_trans sQE (normal_norm nsAE). have [S sylS sAS]:= Sylow_superset (subsetT A) pA. have not_cSS: ~~ abelian S. apply: contra notsFE_Q => cSS; rewrite Fitting_max ?(pgroup_nil qQ) //. have solE := sigma_compl_sol hallE. have [E1 hallE1 sQE1] := Hall_superset solE sQE (pi_pgroup qQ t1Mq). have [_ [E3 hallE3]] := ex_tau13_compl hallE. have [E2 _ complEi] := ex_tau2_compl hallE hallE1 hallE3. have [_ _ _ sQZ] := abelian_tau2 maxM complEi t2Mp EpA sylS sAS cSS. by rewrite sub_center_normal ?{}sQZ //; apply/nElemP; exists q; apply/pnElemP. have [] := nonabelian_tau2 maxM hallE t2Mp EpA (pHall_pgroup sylS) not_cSS. set A0 := 'C_A(M`_\sigma)%G => _ [oA0 defFM] _ _. have defA0: A0 :=: K. have sA0E: A0 \subset E by rewrite subIset ?sAE. have sKA0: K \subset A0. have [_ _ _ tiMsE] := sdprodP (sdprod_sigma maxM hallE). rewrite -(mul1g A0) -tiMsE setIC group_modr // subsetI sKE. by have [_ -> _ _] := dprodP defFM; rewrite Fitting_max ?abelian_nil. by apply/eqP; rewrite eqEsubset prime_meetG ?(setIidPr sKA0) ?oA0. have ntA: A :!=: 1 := nt_pnElem EpA isT. have [H maxNH] := mmax_exists (mFT_norm_proper ntA (mFT_pgroup_proper pA)). have [maxH sNH] := setIdP maxNH; have sQH := subset_trans nAQ sNH. exists H => //. have: p \in [predD \sigma(H) & \beta(H)] /\ q \in [predU \tau1(H) & \tau2(H)]. have [-> // piAb _] := primes_norm_tau2Elem maxM hallE t2Mp EpA maxNH. rewrite (pnatPpi piAb) // (piSg (quotientS _ sQE)) //=. have piQq: q \in \pi(Q) by rewrite -p_rank_gt0 p_rank_abelem ?dimQ. rewrite /= card_quotient ?normsI ?norms_cent // ?normsG //. rewrite -indexgI setIA (setIidPl sQE) prime_TIg ?indexg1 // ?oQ //. rewrite (sameP commG1P eqP) (subG1_contra _ ntK) //= -/K -defKQ commGC. by rewrite -defA0 commgS ?subsetIl. case=> /andP[/= b'Hp sHP] t12Hq. have nregQHs: 'C_(H`_\sigma)(Q) != 1. apply: subG1_contra (setSI _ _) (_ : 'C_A(Q) != 1). rewrite (sub_Hall_pcore (Msigma_Hall maxH)) ?(pi_pgroup pA) //. exact: subset_trans (normG A) sNH. apply: contraTneq (leqnn 1) => regQA; rewrite -ltnNge -dimA. rewrite -(leq_exp2l _ _ (prime_gt1 p_pr)) -card_pgroup // -oA0 defA0. have coAQ := pnat_coprime (pi_pnat pA t2Mp) (pi_pnat qQ (tau2'1 t1Mq)). rewrite subset_leq_card // -(coprime_cent_prod nAQ) ?(pgroup_sol pA) //. by rewrite regQA mulg1 commSg. have{t12Hq} [/= t1Hq | /= t2Hq] := orP t12Hq. have EqQ_H: Q \in 'E_q^1(H) by apply/pnElemP. have kHq: q \in \kappa(H). by rewrite unlock inE /= inE /= t1Hq; apply/exists_inP; exists Q. right; split=> //; apply: contraR b'Hp => notP1maxH. have PmaxH: H \in 'M_'P by apply/PtypeP; split=> //; exists q. have [L hallL] := Hall_exists \kappa(H) (mmax_sol maxH). by have [_ _ _ _ [|<- //]] := Ptype_structure PmaxH hallL; apply/setDP. left; split=> //. have [x defQ]: exists x, Q :=: <[x]> by apply/cyclicP; rewrite prime_cyclic ?oQ. rewrite defQ cent_cycle in nregQHs *; rewrite (cent1_nreg_sigma_uniq maxH) //. by rewrite 2!inE -cycle_eq1 -cycle_subG -defQ (nt_pnElem EqQ). by rewrite /p_elt /order -defQ oQ pnatE. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype bigop order) mathcomp(finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall frobenius) mathcomp(ssralg ssrnum ssrint rat) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection12 BGsection13)