proposition: Theorem BGsummaryII M (X : {set gT}) : M \in 'M -> X \in pred2 'A(M) 'A0(M) -> let D := [set x in X | ~~ ('C[x] \subset M)] in [/\ D \subset 'A1(M), {in X, forall x a, x ^ a \in X -> exists2 y, y \in M & x ^ a = x ^ y} & {in D, forall x (L := 'N[x]), [/\ 'M('C[x]) = [set L], FTtype L \in pred2 1%N 2, [/\ L`_\F ><| (M :&: L) = L, {in X, forall y, coprime #|L`_\F| #|'C_M[y]| }, x \in 'A(L) :\: 'A1(L) & 'C_(L`_\F)[x] ><| 'C_M[x] = 'C[x]] & FTtype L == 2 -> exists2 E, [Frobenius M = M`_\F ><| gval E] & cyclic E]}].
proof: Proof. move=> maxM defX. have sA0M: 'A0(M) \subset M := subset_trans (FTsupp0_sub M) (subsetDl M 1). have sAA0: 'A(M) \subset 'A0(M) := FTsupp_sub0 M. have sAM: 'A(M) \subset M := subset_trans sAA0 sA0M. without loss {defX} ->: X / X = 'A0(M). case/pred2P: defX => ->; move/(_ _ (erefl _))=> //. set D0 := finset _ => [[sD0A1 tameA0 signD0]] D. have sDD0: D \subset D0 by rewrite /D /D0 !setIdE setSI. split=> [|x Ax a Axa|x Dx]; first exact: subset_trans sDD0 sD0A1. by apply: tameA0; apply: (subsetP sAA0). have [/= -> -> [-> coA0L -> -> frobL]] := signD0 x (subsetP sDD0 x Dx). by do 2![split=> //] => y Ay; rewrite coA0L // (subsetP sAA0). move=> {X} D; pose Ms := M`_\sigma. have tiA0A x a: x \in 'A0(M) :\: 'A(M) -> x ^ a \notin 'A(M). rewrite 3!inE; case: (x \in _) => //= /and3P[_ notM'x _]. apply: contra notM'x => /bigcupP[y _ /setD1P[_ /setIP[Mx _]]]. by rewrite -(p_eltJ _ _ a) (mem_p_elt (pgroup_pi _)). have tiA0 x a: x \in 'A0(M) :\: 'A1(M) -> x ^ a \in 'A0(M) -> a \in M. case/setDP=> A0x notA1x A0xa. have [Mx Mxa] := (subsetP sA0M x A0x, subsetP sA0M _ A0xa). have [[U K] /= complU] := kappa_witness maxM. have [Ax | notAx] := boolP (x \in 'A(M)). have [_ _ _ [_]] := BGsummaryB maxM complU; set B := _ :\: _ => tiB. have Bx: x \in B by apply/setDP. have /tiB/normedTI_memJ_P: 'A(M) != 'A1(M) by apply: contraTneq Ax => ->. case=> _ _ /(_ x) <- //; rewrite 3?inE // conjg_eq1; apply/andP; split. apply: contra notA1x; rewrite !inE def_FTcore // => /andP[->]. by rewrite !(mem_Hall_pcore (Msigma_Hall maxM)) // p_eltJ. by apply: contraLR Ax => notAxa; rewrite -(conjgK a x) tiA0A // inE notAxa. have ntK: K :!=: 1. rewrite -(trivgFmax maxM complU) FTtype_Fmax //. by apply: contra notAx => /FTsupp0_type1 <-. have [_ _ [_ [_ /normedTI_memJ_P[_ _ tiB]] _ _]]:= BGsummaryC maxM complU ntK. by rewrite -(tiB x) inE ?tiA0A ?notAx // inE notAx. have sDA1: D \subset 'A1(M). apply/subsetPn=> [[x /setIdP[A0x not_sCxM] notA1x]]. case/subsetP: not_sCxM => a cxa. by apply: (tiA0 x); [apply/setDP | rewrite /conjg -(cent1P cxa) mulKg]. have sDMs1: D \subset Ms^# by rewrite /Ms -def_FTcore. have [tameMs _ signM PsignM] := BGsummaryD maxM. split=> // [x A0x a A0xa|x Dx]. have [A1x | notA1x] := boolP (x \in 'A1(M)); last first. by exists a; rewrite // (tiA0 x) // inE notA1x. case/setD1P: A1x => _; rewrite def_FTcore // => Ms_x. apply/imsetP; rewrite tameMs ?imset_f ?inE //. rewrite (mem_Hall_pcore (Msigma_Hall maxM)) ?(subsetP sA0M) //. by rewrite p_eltJ (mem_p_elt (pcore_pgroup _ _) Ms_x). have [Ms1x [_ not_sCxM]] := (subsetP sDMs1 x Dx, setIdP Dx). have [[uniqN defNF] [ANx typeN hallMN] type2] := PsignM x Ms1x not_sCxM. have [maxN _] := mem_uniq_mmax uniqN. split=> //; last 1 first. - rewrite -FTtype_P2max // => /type2[FmaxM]. by rewrite (Fcore_eq_Msigma maxM _) // notP1type_Msigma_nil ?FmaxM. - by rewrite !inE -FTtype_Fmax // -FTtype_P2max // -in_setU. split=> // [|y A0y|]; rewrite defNF ?sdprod_sigma //=; last by case/signM: Ms1x. rewrite coprime_pi' ?cardG_gt0 // -pgroupE. rewrite (eq_p'group _ (pi_Msigma maxN)); apply: wlog_neg => not_sNx'CMy. have ell1x := Msigma_ell1 maxM Ms1x. have SMxM: M \in 'M_\sigma[x] by rewrite inE maxM cycle_subG; case/setD1P: Ms1x. have MSx_gt1: #|'M_\sigma[x]| > 1. rewrite ltn_neqAle lt0n {2}(cardD1 M) SMxM andbT eq_sym. by apply: contra not_sCxM; move/cent1_sub_uniq_sigma_mmax->. have [FmaxM t2'M]: M \in 'M_'F /\ \tau2(M)^'.-group M. apply: (non_disjoint_signalizer_Frobenius ell1x MSx_gt1 SMxM). by apply: contra not_sNx'CMy; apply: pgroupS (subsetIl _ _). have defA0: 'A0(M) = Ms^#. rewrite FTsupp0_type1; last by rewrite -FTtype_Fmax. rewrite /'A(M) /'A1(M) -FTtype_Fmax // FmaxM def_FTcore //= -/Ms. apply/setP => z; apply/bigcupP/idP=> [[t Ms1t] | Ms1z]; last first. have [ntz Ms_z] := setD1P Ms1z. by exists z; rewrite // 3!inE ntz cent1id (subsetP (pcore_sub _ _) z Ms_z). case/setD1P=> ntz; case/setIP=> Mz ctz. rewrite 2!inE ntz (mem_Hall_pcore (Msigma_Hall maxM)) //. apply: sub_in_pnat (pnat_pi (order_gt0 z)) => p _ pi_z_p. have szM: <[z]> \subset M by rewrite cycle_subG. have [piMp [_ k'M]] := (piSg szM pi_z_p, setIdP FmaxM). apply: contraR (pnatPpi k'M piMp) => s'p /=. rewrite unlock; apply/andP; split. have:= piMp; rewrite (partition_pi_mmax maxM) (negPf s'p) orbF. by rewrite orbCA [p \in _](negPf (pnatPpi t2'M piMp)). move: pi_z_p; rewrite -p_rank_gt0 /= -(setIidPr szM). case/p_rank_geP=> P; rewrite pnElemI -setIdE => /setIdP[EpP sPz]. apply/exists_inP; exists P => //; apply/trivgPn. have [ntt Ms_t] := setD1P Ms1t; exists t => //. by rewrite inE Ms_t (subsetP (centS sPz)) // cent_cycle cent1C. move: A0y; rewrite defA0 => /setD1P[nty Ms_y]. have sCyMs: 'C_M[y] \subset Ms. rewrite -[Ms](setD1K (group1 _)) -subDset /= -defA0 subsetU //. rewrite (bigcup_max y) //; first by rewrite 2!inE nty def_FTcore. by rewrite -FTtype_Fmax ?FmaxM. have notMGN: gval 'N[x] \notin M :^: G. have [_ [//|_ _ t2Nx _ _]] := FT_signalizer_context ell1x. have [ntx Ms_x] := setD1P Ms1x; have sMx := mem_p_elt (pcore_pgroup _ _) Ms_x. apply: contra ntx => /imsetP[a _ defN]. rewrite -order_eq1 (pnat_1 sMx (sub_p_elt _ t2Nx)) // => p. by rewrite defN tau2J // => /andP[]. apply: sub_pgroup (pgroupS sCyMs (pcore_pgroup _ _)) => p sMp. by apply: contraFN (sigma_partition maxM maxN notMGN p) => sNp; apply/andP. 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 BGsection2 BGsection3 BGsection4 BGsection5) odd_order(BGsection6 BGsection7 BGsection9 BGsection10 BGsection12) odd_order(BGsection13 BGsection14 BGsection15)