proposition: Theorem BGsummaryD M : M \in 'M -> [/\ {in M`_\sigma &, forall x y, y \in x ^: G -> y \in x ^: M}, forall g (Ms := M`_\sigma), g \notin M -> Ms:&: M :^ g = Ms :&: Ms :^ g /\ cyclic (Ms :&: M :^ g), {in M`_\sigma^#, forall x, [/\ Hall 'C[x] 'C_M[x], 'R[x] ><| 'C_M[x] = 'C[x] & let MGx := [set Mg in M :^: G | x \in Mg] in [transitive 'R[x], on MGx | 'Js] /\ #|'R[x]| = #|MGx| ]} & {in M`_\sigma^#, forall x (N := 'N[x]), ~~ ('C[x] \subset M) -> [/\ 'M('C[x]) = [set N] /\ N`_\F = N`_\sigma, x \in 'A(N) :\: 'A1(N) /\ N \in 'M_'F :|: 'M_'P2, \sigma(N)^'.-Hall(N) (M :&: N) & N \in 'M_'P2 -> [/\ M \in 'M_'F, exists2 E, [Frobenius M = M`_\sigma ><| gval E] & cyclic E & ~~ normedTI (M`_\F)^# G M]]}].
proof: Proof. move=> maxM; have [[U K] /= complU] := kappa_witness maxM. have defSM: {in M`_\sigma^#, forall x, [set Mg in M :^: G | x \in Mg] = val @: 'M_\sigma[x]}. - move=> x /setD1P[ntx Ms_x]. have SMxM: M \in 'M_\sigma[x] by rewrite inE maxM cycle_subG. apply/setP=> /= Mg; apply/setIdP/imsetP=> [[] | [H]]. case/imsetP=> g _ -> Mg_x; exists (M :^ g)%G => //=. rewrite inE cycle_subG (mem_Hall_pcore (Msigma_Hall _)) ?mmaxJ // maxM. by rewrite (eq_p_elt _ (sigmaJ _ _)) (mem_p_elt (pcore_pgroup _ M)). case/setIdP=> maxH; rewrite cycle_subG => Hs_x ->. split; last exact: subsetP (pcore_sub _ _) x Hs_x. pose p := pdiv #[x]; have pixp: p \in \pi(#[x]) by rewrite pi_pdiv order_gt1. apply/idPn=> /(sigma_partition maxM maxH)/(_ p). rewrite inE /= (pnatPpi (mem_p_elt (pcore_pgroup _ _) Ms_x)) //. by rewrite (pnatPpi (mem_p_elt (pcore_pgroup _ _) Hs_x)). split. - have hallMs := pHall_subl (subxx _) (subsetT _) (Msigma_Hall_G maxM). move=> x y Ms_x Ms_y /=/imsetP[a _ def_y]; rewrite def_y in Ms_y *. have [b /setIP[Mb _ ->]] := sigma_Hall_tame maxM hallMs Ms_x Ms_y. exact: imset_f. - move=> g notMg; split. apply/eqP; rewrite eqEsubset andbC setIS ?conjSg ?pcore_sub //=. rewrite subsetI subsetIl -MsigmaJ. rewrite (sub_Hall_pcore (Msigma_Hall _)) ?mmaxJ ?subsetIr //. rewrite (eq_pgroup _ (sigmaJ _ _)). exact: pgroupS (subsetIl _ _) (pcore_pgroup _ _). have [E hallE] := ex_sigma_compl maxM. by have [_ _] := sigma_compl_embedding maxM hallE; case/(_ g). - move=> x Ms1x /=. have [[ntx Ms_x] ell1x] := (setD1P Ms1x, Msigma_ell1 maxM Ms1x). have [[trR oR nsRC hallR] defC] := FT_signalizer_context ell1x. have SMxM: M \in 'M_\sigma[x] by rewrite inE maxM cycle_subG. suffices defCx: 'R[x] ><| 'C_M[x] = 'C[x]. split=> //; first by rewrite -(sdprod_Hall defCx). rewrite defSM //; split; last by rewrite (card_imset _ val_inj). apply/imsetP; exists (gval M); first exact: imset_f. by rewrite -(atransP trR _ SMxM) -imset_comp. have [| SMgt1] := leqP #|'M_\sigma[x]| 1. rewrite leq_eqVlt {2}(cardD1 M) SMxM orbF => eqSMxM. have ->: 'R[x] = 1 by apply/eqP; rewrite trivg_card1 oR. by rewrite sdprod1g (setIidPr _) ?cent1_sub_uniq_sigma_mmax. have [uniqN _ _ _ defCx] := defC SMgt1. have{defCx} [[defCx _ _ _] [_ sCxN]] := (defCx M SMxM, mem_uniq_mmax uniqN). by rewrite -setIA (setIidPr sCxN) in defCx. move=> x Ms1x /= not_sCM. have [[ntx Ms_x] ell1x] := (setD1P Ms1x, Msigma_ell1 maxM Ms1x). have SMxM: M \in 'M_\sigma[x] by rewrite inE maxM cycle_subG. have SMgt1: #|'M_\sigma[x]| > 1. apply: contraR not_sCM; rewrite -leqNgt leq_eqVlt {2}(cardD1 M) SMxM orbF. by move/cent1_sub_uniq_sigma_mmax->. have [_ [//|uniqN ntR t2Nx notP1maxN]] := FT_signalizer_context ell1x. have [maxN sCxN] := mem_uniq_mmax uniqN. case/(_ M SMxM)=> _ st2NsM _ ->; split=> //. - by rewrite (Fcore_eq_Msigma maxN (notP1type_Msigma_nil _)) // -in_setU. - split=> //; apply/setDP; split. have [y Ry nty] := trivgPn _ ntR; have [Nsy cxy] := setIP Ry. apply/bigcupP; exists y; first by rewrite 2!inE def_FTcore ?nty. rewrite 3!inE ntx cent1C cxy -FTtype_Pmax //= andbT. have Nx: x \in 'N[x] by rewrite (subsetP sCxN) ?cent1id. case PmaxN: ('N[x] \in 'M_'P) => //. have [KN hallKN] := Hall_exists \kappa('N[x]) (mmax_sol maxN). have [_ _ [_ _ _ _ [_ _ _ defN]]] := Ptype_embedding PmaxN hallKN. have hallN': \kappa('N[x])^'.-Hall('N[x]) 'N[x]^`(1). exact/(sdprod_normal_pHallP (der_normal 1 _) hallKN). rewrite (mem_normal_Hall hallN') ?der_normal // (sub_p_elt _ t2Nx) // => p. by case/andP=> _; apply: contraL => /rank_kappa->. rewrite 2!inE ntx def_FTcore //=; apply: contra ntx => Ns_x. rewrite -(constt_p_elt (mem_p_elt (pcore_pgroup _ _) Ns_x)). by rewrite (constt1P (sub_p_elt _ t2Nx)) // => p; case/andP. move=> P2maxN; have [PmaxN _] := setDP P2maxN; have [_ notFmaxN] := setDP PmaxN. have [FmaxM _ [E _]] := nonFtype_signalizer_base maxM Ms1x not_sCM notFmaxN. case=> cycE frobM; split=> //; first by exists E. move: SMgt1; rewrite (cardsD1 M) SMxM ltnS lt0n => /pred0Pn[My /setD1P[neqMyM]]. move/(imset_f val); rewrite -defSM //= => /setIdP[/imsetP[y _ defMy] My_x]. rewrite (Fcore_eq_Msigma maxM (notP1type_Msigma_nil _)) ?FmaxM //. apply/normedTI_P=> [[_ _ /(_ y (in_setT y))/contraR/implyP/idPn[]]]. rewrite -{1}(norm_mmax maxM) (sameP normP eqP) -defMy neqMyM. apply/pred0Pn; exists x; rewrite /= conjD1g !inE ntx Ms_x /= -MsigmaJ. rewrite (mem_Hall_pcore (Msigma_Hall _)) ?mmaxJ /= -?defMy //. by rewrite defMy (eq_p_elt _ (sigmaJ _ _)) (mem_p_elt (pcore_pgroup _ _) Ms_x). 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)