proposition: Theorem FT_signalizer_context x (N := 'N[x]) (R := 'R[x]) : \ell_\sigma(x) == 1%N -> [/\ [/\ [transitive R, on 'M_\sigma[x] | 'JG], #|R| = #|'M_\sigma[x]|, R <| 'C[x] & Hall 'C[x] R] & #|'M_\sigma[x]| > 1 -> [/\ 'M('C[x]) = [set N], R :!=: 1, \tau2(N).-elt x, N \in 'M_'F :|: 'M_'P2 & {in 'M_\sigma[x], forall M, [/\ R ><| 'C_(M :&: N)[x] = 'C[x], {subset \tau2(N) <= \sigma(M)}, {subset [predI \pi(M) & \sigma(N)] <= \beta(N)} & \sigma(N)^'.-Hall(N) (M :&: N)]}]].
proof: Proof. rewrite {}/N {}/R => ell1x; have [ntx ntMSx] := ell_sigma1P x ell1x. have [M MSxM] := set0Pn _ ntMSx; have [maxM Ms_x] := setIdP MSxM. rewrite cycle_subG in Ms_x; have sMx := mem_p_elt (pcore_pgroup _ M) Ms_x. have Mx: x \in M := subsetP (pcore_sub _ _) x Ms_x. have [MSx_le1 | MSx_gt1] := leqP _ 1. rewrite /'R[x] /'N[x] ltnNge MSx_le1 (trivgP (pcore_sub _ _)) setI1g normal1. have <-: [set M] = 'M_\sigma[x]. by apply/eqP; rewrite eqEcard sub1set MSxM cards1. by rewrite /Hall atrans_acts_card ?imset_set1 ?cards1 ?sub1G ?coprime1n. have [q pi_x_q]: exists q, q \in \pi(#[x]). by exists (pdiv #[x]); rewrite pi_pdiv order_gt1. have{sMx} sMq: q \in \sigma(M) := pnatPpi sMx pi_x_q. have [X EqX]: exists X, X \in 'E_q^1(<[x]>). by apply/p_rank_geP; rewrite p_rank_gt0. have [sXx abelX dimX] := pnElemP EqX; have [qX cXX _] := and3P abelX. have ntX: X :!=: 1 := nt_pnElem EqX isT. have sXM: X \subset M by rewrite (subset_trans sXx) ?cycle_subG. have [N maxNX_N] := mmax_exists (mFT_norm_proper ntX (mFT_pgroup_proper qX)). have [maxN sNX_N] := setIdP maxNX_N; pose R := 'C_(N`_\sigma)[x]%G. have sCX_N: 'C(X) \subset N := subset_trans (cent_sub X) sNX_N. have sCx_N: 'C[x] \subset N by rewrite -cent_cycle (subset_trans (centS sXx)). have sMSx_MSX: 'M_\sigma[x] \subset 'M_\sigma(X). apply/subsetP=> M1 /setIdP[maxM1 sxM1]. by rewrite inE maxM1 (subset_trans sXx). have nsRCx: R <| 'C[x] by rewrite /= setIC (normalGI sCx_N) ?pcore_normal. have hallR: \sigma(N).-Hall('C[x]) R. exact: setI_normal_Hall (pcore_normal _ _) (Msigma_Hall maxN) sCx_N. have transCX: [transitive 'C(X), on 'M_\sigma(X) | 'JG]. have [_ trCX _ ] := sigma_group_trans maxM sMq qX. case/imsetP: trCX => _ /setIdP[/imsetP[y _ ->] sXMy] trCX. have maxMy: (M :^ y)%G \in 'M by rewrite mmaxJ. have sXMys: X \subset (M :^ y)`_\sigma. by rewrite (sub_Hall_pcore (Msigma_Hall _)) // (pi_pgroup qX) ?sigmaJ. apply/imsetP; exists (M :^ y)%G; first exact/setIdP. apply/setP=> Mz; apply/setIdP/imsetP=> [[maxMz sXMzs] | [z cXz -> /=]]. suffices: gval Mz \in orbit 'Js 'C(X) (M :^ y). by case/imsetP=> z CXz /group_inj->; exists z. rewrite -trCX inE andbC (subset_trans sXMzs) ?pcore_sub //=. apply/idPn => /(sigma_partition maxM maxMz)/=/(_ q)/idP[]. rewrite inE /= sMq (pnatPpi (pgroupS sXMzs (pcore_pgroup _ _))) //. by rewrite -p_rank_gt0 p_rank_abelem ?dimX. by rewrite mmaxJ -(normP (subsetP (cent_sub X) z cXz)) MsigmaJ conjSg. have MSX_M: M \in 'M_\sigma(X) := subsetP sMSx_MSX M MSxM. have not_sCX_M: ~~ ('C(X) \subset M). apply: contraL MSx_gt1 => sCX_M. rewrite -leqNgt (leq_trans (subset_leq_card sMSx_MSX)) //. rewrite -(atransP transCX _ MSX_M) card_orbit astab1JG. by rewrite (setIidPl (normsG sCX_M)) indexgg. have neqNM: N :!=: M by apply: contraNneq not_sCX_M => <-. have maxNX'_N: N \in 'M('N(X)) :\ M by rewrite 2!inE neqNM. have [notMGN _] := sigma_subgroup_embedding maxM sMq sXM qX ntX maxNX'_N. have sN'q: q \notin \sigma(N). by apply: contraFN (sigma_partition maxM maxN notMGN q) => sNq; apply/andP. rewrite (negPf sN'q) => [[t2Nq s_piM_bN hallMN]]. have defN: N`_\sigma ><| (M :&: N) = N. exact/(sdprod_Hall_pcoreP (Msigma_Hall maxN)). have Nx: x \in N by rewrite (subsetP sCx_N) ?cent1id. have MNx: x \in M :&: N by rewrite inE Mx. have sN'x: \sigma(N)^'.-elt x by rewrite (mem_p_elt (pHall_pgroup hallMN)). have /andP[sNsN nNsN]: N`_\sigma <| N := pcore_normal _ _. have nNs_x: x \in 'N(N`_\sigma) := subsetP nNsN x Nx. have defCx: R ><| 'C_(M :&: N)[x] = 'C[x]. rewrite -{2}(setIidPr sCx_N) /= -cent_cycle (subcent_sdprod defN) //. by rewrite subsetI andbC normsG ?cycle_subG. have transR: [transitive R, on 'M_\sigma[x] | 'JG]. apply/imsetP; exists M => //; apply/setP=> L. apply/idP/imsetP=> [MSxL | [u Ru ->{L}]]; last first. have [_ cxu] := setIP Ru; rewrite /= -cent_cycle in cxu. by rewrite -(normsP (cent_sub _) u cxu) sigma_mmaxJ. have [u cXu defL] := atransP2 transCX MSX_M (subsetP sMSx_MSX _ MSxL). have [_ mulMN nNsMN tiNsMN] := sdprodP defN. have:= subsetP sCX_N u cXu; rewrite -mulMN -normC //. case/imset2P=> v w /setIP[Mv _] Ns_w def_u; exists w => /=; last first. by apply: group_inj; rewrite defL /= def_u conjsgM (conjGid Mv). rewrite inE Ns_w -groupV (sameP cent1P commgP) -in_set1 -set1gE -tiNsMN. rewrite setICA setIC (setIidPl sNsN) inE groupMl ?groupV //. rewrite memJ_norm // groupV Ns_w /= -(norm_mmax maxM) inE sub_conjg. rewrite invg_comm -(conjSg _ _ w) -{2}(conjGid Mx) -!conjsgM -conjg_Rmul. rewrite -conjgC conjsgM -(conjGid Mv) -(conjsgM M) -def_u. rewrite -[M :^ u](congr_group defL) conjGid // -cycle_subG. by have [_ Ls_x] := setIdP MSxL; rewrite (subset_trans Ls_x) ?pcore_sub. have oR: #|R| = #|'M_\sigma[x]|. rewrite -(atransP transR _ MSxM) card_orbit astab1JG (norm_mmax maxM). rewrite -setIAC /= -{3}(setIidPl sNsN) -(setIA _ N) -(setIC M). by have [_ _ _ ->] := sdprodP defN; rewrite setI1g indexg1. have ntR: R :!=: 1 by rewrite -cardG_gt1 oR. have [y Ns_y CNy_x]: exists2 y, y \in (N`_\sigma)^# & x \in ('C_N[y])^#. have [y Ry nty] := trivgPn _ ntR; have [Ns_y cxy] := setIP Ry. by exists y; rewrite 2!inE ?nty // inE Nx cent1C ntx. have kN'q: q \notin \kappa(N). rewrite (contra (@kappa_tau13 N q)) // negb_or (contraL (@tau2'1 _ _ _)) //. exact: tau3'2. have [[kNx _] | [t2Nx _ uniqN]] := pi_of_cent_sigma maxN Ns_y CNy_x sN'x. by case/idPn: (pnatPpi kNx pi_x_q). have defNx: 'N[x] = N. apply/set1P; rewrite -uniqN /'N[x] MSx_gt1. by case: pickP => // /(_ N); rewrite uniqN /= set11. rewrite /'R[x] {}defNx -(erefl (gval R)) (pHall_Hall hallR). split=> // _; split=> // [|L MSxL]. rewrite !(maxN, inE) /=; case: (pgroup _ _) => //=; rewrite andbT. apply: contra kN'q => skN_N; have:= pnatPpi (mem_p_elt skN_N Nx) pi_x_q. by case/orP=> //=; rewrite (negPf sN'q). have [u Ru ->{L MSxL}] := atransP2 transR MSxM MSxL; rewrite /= cardJg. have [Ns_u cxu] := setIP Ru; have Nu := subsetP sNsN u Ns_u. rewrite -{1}(conjGid Ru) -(conjGid cxu) -{1 6 7}(conjGid Nu) -!conjIg pHallJ2. split=> // [|p t2Np]. rewrite /= -(setTI 'C[x]) -!(setICA setT) -!morphim_conj. exact: injm_sdprod (subsetT _) (injm_conj _ _) defCx. have [A Ep2A _] := ex_tau2Elem hallMN t2Np. have [[nsAMN _] _ _ _] := tau2_compl_context maxN hallMN t2Np Ep2A. have{} Ep2A: A \in 'E_p^2(M) by move: Ep2A; rewrite pnElemI; case/setIP. have rpM: 'r_p(M) > 1 by apply/p_rank_geP; exists A. have: p \in \pi(M) by rewrite -p_rank_gt0 ltnW. rewrite sigmaJ partition_pi_mmax // !orbA; case/orP=> //. rewrite orbAC -2!andb_orr -(subnKC rpM) andbF /= => t2Mp. case/negP: ntX; rewrite -subG1 (subset_trans sXx) //. have [_ _ <- _ _] := tau2_context maxM t2Mp Ep2A. have [[sAM abelA _] [_ nAMN]] := (pnElemP Ep2A, andP nsAMN). rewrite -coprime_norm_cent ?(subset_trans sAM) ?gFnorm //. by rewrite cycle_subG inE Ms_x (subsetP nAMN). have [[sM'p _] [pA _]] := (andP t2Mp, andP abelA). exact: pnat_coprime (pcore_pgroup _ _) (pi_pgroup pA sM'p). 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)