proposition: Lemma non_disjoint_signalizer_Frobenius x M : \ell_\sigma(x) == 1%N -> #|'M_\sigma[x]| > 1 -> M \in 'M_\sigma[x] -> ~~ (\sigma('N[x])^'.-group M) -> M \in 'M_'F /\ \tau2(M)^'.-group M.
proof: Proof. move=> ell1x ntR SMxM; have [maxM Ms_x] := setIdP SMxM. rewrite negb_and cardG_gt0 all_predC negbK => /hasP[q /= piMq sNq]. have [Q EqQ]: exists Q, Q \in 'E_q^1(M) by apply/p_rank_geP; rewrite p_rank_gt0. have [ntQ [sQM abelQ dimQ]] := (nt_pnElem EqQ isT, pnElemP EqQ). have [[qQ _] q_pr] := (andP abelQ, pnElem_prime EqQ). have [_ [//| uniqN _ t2Nx _]] := FT_signalizer_context ell1x. case/(_ M SMxM)=> _ st2NsM spM_sbN _; have [maxN sCxN] := mem_uniq_mmax uniqN. have bNq: q \in \beta('N[x]) by rewrite spM_sbN //=; do 2!rewrite inE /= ?piMq. have bGq: q \in \beta(G) by move: bNq; rewrite -predI_sigma_beta // inE /= sNq. set p := pdiv #[x]; have pi_p: p \in \pi(#[x]). by rewrite pi_pdiv order_gt1 (sameP eqP (ell_sigma0P _)) (eqP ell1x). have sMp: p \in \sigma(M) := pnatPpi (pcore_pgroup _ _) (piSg Ms_x pi_p). have t2Np: p \in \tau2('N[x]) := pnatPpi t2Nx pi_p. have notMGN: gval 'N[x] \notin M :^: G. apply: contraL t2Np => /imsetP[a _ ->]. by rewrite negb_and negbK /= sigmaJ sMp. have sM'q: q \in \sigma(M)^'. by apply: contraFN (sigma_partition maxM maxN notMGN q) => sMq; apply/andP. have [g sQNg]: exists g, Q \subset 'N[x] :^ g. have [Q1 sylQ1] := Sylow_exists q 'N[x]. have [g _ sQQ1g] := Sylow_subJ (sigma_Sylow_G maxN sNq sylQ1) (subsetT Q) qQ. by exists g; rewrite (subset_trans sQQ1g) // conjSg (pHall_sub sylQ1). have EqNQ: Q \in 'E_q^1('N[x] :^ g) by apply/pnElemP. have uniqNg: 'M('C(Q)) = [set 'N[x] :^ g]%G. by case/cent_der_sigma_uniq: EqNQ; rewrite ?mmaxJ 1?betaJ ?bNq. have b'Mp: p \notin \beta(M). by rewrite -predI_sigma_beta // inE /= sMp /=; case/tau2_not_beta: t2Np. have{p pi_p sMp t2Np b'Mp} FmaxM: M \in 'M_'F. have [P1maxM | notP1maxM] := boolP (M \in 'M_'P1); last first. have [K hallK] := Hall_exists \kappa(M) (mmax_sol maxM). apply: contraR b'Mp => notFmaxM; have PmaxM: M \in 'M_'P by apply/setDP. by have [_ _ _ _ [|<- //]] := Ptype_structure PmaxM hallK; apply/setDP. have [PmaxM skM] := setIdP P1maxM. have kMq: q \in \kappa(M). by case/orP: (pnatPpi skM piMq) => //= sMq; case/negP: sM'q. have [K hallK sQK] := Hall_superset (mmax_sol maxM) sQM (pi_pnat qQ kMq). have EqKQ: Q \in 'E_q^1(K) by apply/pnElemP. have [L _ [uniqL [kLhallKs sMhallKs] _ _ _]] := Ptype_embedding PmaxM hallK. set Ks := 'C_(_)(K) in kLhallKs sMhallKs. have{uniqL} defL: 'N[x] :^ g = L. apply: congr_group; apply: set1_inj; rewrite -uniqNg uniqL //. by apply/nElemP; exists q. have rpL: 'r_p(L) = 2. by apply/eqP; case/andP: t2Np => _; rewrite -defL p_rankJ. suffices piKs_p: p \in \pi(Ks). by rewrite rank_kappa // (pnatPpi (pHall_pgroup kLhallKs)) in rpL. have [P sylP] := Sylow_exists p [group of Ks]. have sylP_L: p.-Sylow(L) P := subHall_Sylow sMhallKs sMp sylP. by rewrite -p_rank_gt0 -(rank_Sylow sylP) (rank_Sylow sylP_L) ?rpL. split=> //; apply: sub_pgroup (pgroup_pi _) => p piMp; apply/negP=> /= t2Mp. have rpN: 'r_p('N[x]) <= 1. have: p \notin \beta('N[x]). rewrite -(predI_sigma_beta maxN) negb_and /= orbC. by have [-> _] := tau2_not_beta maxM t2Mp. apply: contraR; rewrite -ltnNge => rpN; rewrite spM_sbN // inE /= piMp. have: p \in \pi('N[x]) by rewrite -p_rank_gt0 ltnW. rewrite (partition_pi_mmax maxN) orbCA => /orP[t2Np | ]. by case/andP: t2Mp => /negP[]; apply: st2NsM. by rewrite orbA -!andb_orr eqn_leq leqNgt rpN andbF. have [E hallE sQE] := Hall_superset (mmax_sol maxM) sQM (pi_pgroup qQ sM'q). have [A Ep2A _] := ex_tau2Elem hallE t2Mp; have [_ abelA dimA] := pnElemP Ep2A. pose A0 := [~: A, Q]%G; pose A1 := 'C_A(Q)%G. have sCQNg: 'C(Q) \subset 'N[x] :^ g by have [] := mem_uniq_mmax uniqNg. have ntA0: A0 :!=: 1. rewrite (sameP eqP commG1P); apply: contraL rpN => cQA. rewrite -ltnNge -(p_rankJ p _ g); apply/p_rank_geP. by exists A; apply/pnElemP; rewrite (subset_trans cQA). have t1Mq: q \in \tau1(M). have [_ nsCEA_E t1Eb] := tau1_cent_tau2Elem_factor maxM hallE t2Mp Ep2A. rewrite (pnatPpi t1Eb) // (piSg (quotientS _ sQE)) // -p_rank_gt0. rewrite -rank_pgroup ?quotient_pgroup // rank_gt0 -subG1. rewrite quotient_sub1 ?(subset_trans _ (normal_norm nsCEA_E)) //. by rewrite subsetI sQE centsC (sameP commG1P eqP). have EqEQ: Q \in 'E_q^1(E) by apply/pnElemP. have regMsQ: 'C_(M`_\sigma)(Q) = 1. apply: contraTeq FmaxM => nregMsQ; apply/FtypeP=> [[_]]; move/(_ q). by rewrite unlock inE /= inE /= t1Mq; case/exists_inP; exists Q. have [[]] := tau1_act_tau2 maxM hallE t2Mp Ep2A t1Mq EqEQ regMsQ ntA0. rewrite -/A0 -/A1 => EpA0 cMsA0 _ notA1GA0 [EpA1 _]. have [sA0A abelA0 oA0] := pnElemPcard EpA0; have [pA0 _] := andP abelA0. have [sA1A abelA1 oA1] := pnElemPcard EpA1; have [pA1 _] := andP abelA1. have sA0N: A0 \subset 'N[x]. rewrite -cMsA0 (subset_trans _ sCxN) //= -cent_cycle (centsS Ms_x) //. exact: subsetIr. have [P sylP sA0P] := Sylow_superset sA0N pA0; have [_ pP _] := and3P sylP. have cycP: cyclic P. by rewrite (odd_pgroup_rank1_cyclic pP) ?mFT_odd ?(p_rank_Sylow sylP). have sA1gN: A1 :^ g^-1 \subset 'N[x] by rewrite sub_conjgV subIset ?sCQNg ?orbT. have [|z _ sA1gzP] := Sylow_Jsub sylP sA1gN; first by rewrite pgroupJ. case/imsetP: notA1GA0; exists (g^-1 * z); rewrite ?inE // conjsgM. by apply/eqP; rewrite (eq_subG_cyclic cycP) // !cardJg oA0 oA1. 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)