path: root/mathcomp/odd_order/BGsection10.v

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
(* Distributed under the terms of CeCILL-B.                                  *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
Require Import ssrbool ssrfun eqtype ssrnat seq div path fintype.
From mathcomp
Require Import bigop finset prime fingroup morphism perm automorphism quotient.
From mathcomp
Require Import action gproduct gfunctor pgroup cyclic center commutator.
From mathcomp
Require Import gseries nilpotent sylow abelian maximal hall.
From mathcomp
Require Import BGsection1 BGsection3 BGsection4 BGsection5 BGsection6.
From mathcomp
Require Import BGsection7 BGsection9.

(******************************************************************************)
(*   This file covers B & G, section 10, including with the definitions:      *)
(*   \alpha(M) == the primes p such that M has p-rank at least 3.             *)
(*   \beta(M)  == the primes p in \alpha(M) such that Sylow p-subgroups of M  *)
(*                are not narrow (see BGsection5), i.e., such that M contains *)
(*                no maximal elementary abelian subgroups of rank 2. In a     *)
(*                minimal counter-example G, \beta(M) is the intersection of  *)
(*                \alpha(M) and \beta(G). Note that B & G refers to primes in *)
(*                \beta(G) as ``ideal'' primes, somewhat inconsistently.      *)
(*   \sigma(M) == the primes p such that there exists a p-Sylow subgroup P    *)
(*                of M whose normaliser (in the minimal counter-example) is   *)
(*                contained in M.                                             *)
(*   M`_\alpha == the \alpha(M)-core of M.                                    *)
(*   M`_\beta  == the \beta(M)-core of M.                                     *)
(*   M`_\sigma == the \sigma(M)-core of M.                                    *)
(******************************************************************************)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GroupScope.

Reserved Notation "\alpha ( M )" (at level 2, format "\alpha ( M )").
Reserved Notation "\beta ( M )" (at level 2, format "\beta ( M )").
Reserved Notation "\sigma ( M )" (at level 2, format "\sigma ( M )").

Reserved Notation "M `_ \alpha" (at level 3, format "M `_ \alpha").
Reserved Notation "M `_ \beta" (at level 3, format "M `_ \beta").
Reserved Notation "M `_ \sigma" (at level 3, format "M `_ \sigma").

Section Def.

Variable gT : finGroupType.
Implicit Type p : nat.

Variable M : {set gT}.

Definition alpha := [pred p | 2 < 'r_p(M)].
Definition alpha_core := 'O_alpha(M).
Canonical Structure alpha_core_group := Eval hnf in [group of alpha_core].

Definition beta :=
  [pred p | [forall (P : {group gT} | p.-Sylow(M) P), ~~ p.-narrow P]].
Definition beta_core := 'O_beta(M).
Canonical Structure beta_core_group := Eval hnf in [group of beta_core].

Definition sigma :=
  [pred p | [exists (P : {group gT} | p.-Sylow(M) P), 'N(P) \subset M]].
Definition sigma_core := 'O_sigma(M).
Canonical Structure sigma_core_group := Eval hnf in [group of sigma_core].

End Def.

Notation "\alpha ( M )" := (alpha M) : group_scope.
Notation "M `_ \alpha" := (alpha_core M) : group_scope.
Notation "M `_ \alpha" := (alpha_core_group M) : Group_scope.

Notation "\beta ( M )" := (beta M) : group_scope.
Notation "M `_ \beta" := (beta_core M) : group_scope.
Notation "M `_ \beta" := (beta_core_group M) : Group_scope.

Notation "\sigma ( M )" := (sigma M) : group_scope.
Notation "M `_ \sigma" := (sigma_core M) : group_scope.
Notation "M `_ \sigma" := (sigma_core_group M) : Group_scope.

Section CoreTheory.

Variable gT : minSimpleOddGroupType.
Local Notation G := (TheMinSimpleOddGroup gT).
Implicit Type x : gT.
Implicit Type P : {group gT}.

Section GenericCores.

Variables H K : {group gT}.

Lemma sigmaJ x : \sigma(H :^ x) =i \sigma(H).
Proof.
move=> p; apply/exists_inP/exists_inP=> [] [P sylP sNH]; last first.
  by exists (P :^ x)%G; rewrite ?pHallJ2 // normJ conjSg.
by exists (P :^ x^-1)%G; rewrite ?normJ ?sub_conjgV // -(pHallJ2 _ _ _ x) actKV.
Qed.

Lemma MsigmaJ x : (H :^ x)`_\sigma = H`_\sigma :^ x.
Proof. by rewrite /sigma_core -(eq_pcore H (sigmaJ x)) pcoreJ. Qed.

Lemma alphaJ x : \alpha(H :^ x) =i \alpha(H).
Proof. by move=> p; rewrite !inE /= p_rankJ. Qed.

Lemma MalphaJ x : (H :^ x)`_\alpha = H`_\alpha :^ x.
Proof. by rewrite /alpha_core -(eq_pcore H (alphaJ x)) pcoreJ. Qed.

Lemma betaJ x : \beta(H :^ x) =i \beta(H).
Proof.
move=> p; apply/forall_inP/forall_inP=> nnSylH P sylP.
  by rewrite -(@narrowJ _ _ _ x) nnSylH ?pHallJ2.
by rewrite -(@narrowJ _ _ _ x^-1) nnSylH // -(pHallJ2 _ _ _ x) actKV.
Qed.

Lemma MbetaJ x : (H :^ x)`_\beta = H`_\beta :^ x.
Proof. by rewrite /beta_core -(eq_pcore H (betaJ x)) pcoreJ. Qed.

End GenericCores.

(* This remark appears at the start (p. 70) of B & G, Section 10, just after  *)
(* the definition of ideal, which we do not include, since it is redundant    *)
(* with the notation p \in \beta(G) that is used later.                       *)
Remark not_narrow_ideal p P : p.-Sylow(G) P -> ~~ p.-narrow P -> p \in \beta(G).
Proof.
move=> sylP nnP; apply/forall_inP=> Q sylQ.
by have [x _ ->] := Sylow_trans sylP sylQ; rewrite narrowJ.
Qed.

Section MaxCores.

Variables M : {group gT}.
Hypothesis maxM : M \in 'M.

(* This is the first inclusion in the remark following the preliminary        *)
(* definitions in B & G, p. 70.                                               *)
Remark beta_sub_alpha : {subset \beta(M) <= \alpha(M)}.
Proof.
move=> p; rewrite !inE /= => /forall_inP nnSylM.
have [P sylP] := Sylow_exists p M; have:= nnSylM P sylP.
by rewrite negb_imply (p_rank_Sylow sylP) => /andP[].
Qed.

Remark alpha_sub_sigma : {subset \alpha(M) <= \sigma(M)}.
Proof.
move=> p a_p; have [P sylP] := Sylow_exists p M; have [sPM pP _ ] := and3P sylP.
have{a_p} rP: 2 < 'r(P) by rewrite (rank_Sylow sylP).
apply/exists_inP; exists P; rewrite ?uniq_mmax_norm_sub //.
exact: def_uniq_mmax (rank3_Uniqueness (mFT_pgroup_proper pP) rP) maxM sPM.
Qed.

Remark beta_sub_sigma : {subset \beta(M) <= \sigma(M)}.
Proof. by move=> p; move/beta_sub_alpha; apply: alpha_sub_sigma. Qed.

Remark Mbeta_sub_Malpha : M`_\beta \subset M`_\alpha.
Proof. exact: sub_pcore beta_sub_alpha. Qed.

Remark Malpha_sub_Msigma : M`_\alpha \subset M`_\sigma.
Proof. exact: sub_pcore alpha_sub_sigma. Qed.

Remark Mbeta_sub_Msigma : M`_\beta \subset M`_\sigma.
Proof. exact: sub_pcore beta_sub_sigma. Qed.

(* This is the first part of the remark just above B & G, Theorem 10.1. *)
Remark norm_sigma_Sylow p P :
  p \in \sigma(M) -> p.-Sylow(M) P -> 'N(P) \subset M.
Proof.
case/exists_inP=> Q sylQ sNPM sylP.
by case: (Sylow_trans sylQ sylP) => m mM ->; rewrite normJ conj_subG.
Qed.

(* This is the second part of the remark just above B & G, Theorem 10.1. *)
Remark sigma_Sylow_G p P : p \in \sigma(M) -> p.-Sylow(M) P -> p.-Sylow(G) P.
Proof.
move=> sMp sylP; apply: (mmax_sigma_Sylow maxM) => //.
exact: norm_sigma_Sylow sMp sylP.
Qed.

Lemma sigma_Sylow_neq1 p P : p \in \sigma(M) -> p.-Sylow(M) P -> P :!=: 1.
Proof.
move=> sMp /(norm_sigma_Sylow sMp); apply: contraTneq => ->.
by rewrite norm1 subTset -properT mmax_proper.
Qed.

Lemma sigma_sub_pi : {subset \sigma(M) <= \pi(M)}.
Proof.
move=> p sMp; have [P sylP]:= Sylow_exists p M.
by rewrite -p_rank_gt0 -(rank_Sylow sylP) rank_gt0 (sigma_Sylow_neq1 sMp sylP).
Qed.

Lemma predI_sigma_alpha : [predI \sigma(M) & \alpha(G)] =i \alpha(M).
Proof.
move=> p; rewrite inE /= -(andb_idl (@alpha_sub_sigma p)).
apply: andb_id2l => sMp; have [P sylP] := Sylow_exists p M.
by rewrite !inE -(rank_Sylow sylP) -(rank_Sylow (sigma_Sylow_G sMp sylP)).
Qed.

Lemma predI_sigma_beta : [predI \sigma(M) & \beta(G)] =i \beta(M).
Proof.
move=> p; rewrite inE /= -(andb_idl (@beta_sub_sigma p)).
apply: andb_id2l => sMp; apply/idP/forall_inP=> [bGp P sylP | nnSylM].
  exact: forall_inP bGp P (sigma_Sylow_G sMp sylP).
have [P sylP] := Sylow_exists p M.
exact: not_narrow_ideal (sigma_Sylow_G sMp sylP) (nnSylM P sylP).
Qed.

End MaxCores.

End CoreTheory.

Section Ten.

Variable gT : minSimpleOddGroupType.
Local Notation G := (TheMinSimpleOddGroup gT).

Implicit Type p : nat.
Implicit Type A E H K M N P Q R S V W X Y : {group gT}.

(* This is B & G, Theorem 10.1(d); note that we do not assume M is maximal. *)
Theorem sigma_Sylow_trans M p X g :
  p \in \sigma(M) -> p.-Sylow(M) X -> X :^ g \subset M -> g \in M.
Proof.
move=> sMp sylX sXgM; have pX := pHall_pgroup sylX.
have [|h hM /= sXghX] := Sylow_Jsub sylX sXgM; first by rewrite pgroupJ.
by rewrite -(groupMr _ hM) (subsetP (norm_sigma_Sylow _ sylX)) ?inE ?conjsgM.
Qed.

(* This is B & G, Theorem 10.1 (a, b, c). *)
(* Part (e) of Theorem 10.1 is obviously stated incorrectly, and this is      *)
(* difficult to correct because it is not used in the rest of the proof.      *)
Theorem sigma_group_trans M p X :
     M \in 'M -> p \in \sigma(M) -> p.-group X ->
  [/\ (*a*) forall g, X \subset M -> X :^ g \subset M ->
            exists2 c, c \in 'C(X) & exists2 m, m \in M & g = c * m,
      (*b*) [transitive 'C(X), on [set Mg in M :^: G | X \subset Mg] | 'Js ]
    & (*c*) X \subset M -> 'C(X) * 'N_M(X) = 'N(X)].
Proof.
move=> maxM sMp pX; have defNM := norm_mmax maxM.
pose OM (Y : {set gT}) : {set {set gT}} := [set Mg in M :^: G | Y \subset Mg].
pose trM (Y : {set gT}) := [transitive 'C(Y), on OM Y | 'Js].
have actsOM Y: [acts 'N(Y), on OM Y | 'Js].
  apply/actsP=> z nYz Q; rewrite !inE -{1}(normP nYz) conjSg.
  by rewrite (acts_act (acts_orbit _ _ _)) ?inE.
have OMid Y: (gval M \in OM Y) = (Y \subset M) by rewrite inE orbit_refl.
have ntOM Y: p.-group Y -> exists B, gval B \in OM Y.
  have [S sylS] := Sylow_exists p M; have sSM := pHall_sub sylS.
  have sylS_G := sigma_Sylow_G maxM sMp sylS.
  move=> pY; have [g Gg sXSg] := Sylow_subJ sylS_G (subsetT Y) pY.
  by exists (M :^ g)%G; rewrite inE mem_orbit // (subset_trans sXSg) ?conjSg.
have maxOM Y H: gval H \in OM Y -> H \in 'M.
  by case/setIdP=> /imsetP[g _ /val_inj->]; rewrite mmaxJ.
have part_c Y H: trM Y -> gval H \in OM Y -> 'C(Y) * 'N_H(Y) = 'N(Y).
  move=> trMY O_H; rewrite -(norm_mmax (maxOM Y H O_H)) -(astab1Js H) setIC.
  have [sCN nCN] := andP (cent_normal Y); rewrite -normC 1?subIset ?nCN //.
  by apply/(subgroup_transitiveP O_H); rewrite ?(atrans_supgroup sCN) ?actsOM.
suffices trMX: trM X.
  do [split; rewrite // -OMid] => [g O_M sXgM |]; last exact: part_c.
  have O_Mg': M :^ g^-1 \in OM X by rewrite inE mem_orbit -?sub_conjg ?inE.
  have [c Cc /= Mc] := atransP2 trMX O_M O_Mg'; exists c^-1; rewrite ?groupV //.
  by exists (c * g); rewrite ?mulKg // -defNM inE conjsgM -Mc conjsgKV.
elim: {X}_.+1 {-2}X (ltnSn (#|G| - #|X|)) => // n IHn X geXn in pX *.
have{n IHn geXn} IHX Y: X \proper Y -> p.-group Y -> trM Y.
  move=> ltXY; apply: IHn; rewrite -ltnS (leq_trans _ geXn) // ltnS.
  by rewrite ltn_sub2l ?(leq_trans (proper_card ltXY)) // cardsT max_card.
have [-> | ntX] := eqsVneq X 1.
  rewrite /trM cent1T /OM setIdE (setIidPl _) ?atrans_orbit //.
  by apply/subsetP=> Mg; case/imsetP=> g _ ->; rewrite inE sub1G.
pose L := 'N(X)%G; have ltLG := mFT_norm_proper ntX (mFT_pgroup_proper pX).
have IH_L: {in OM X &, forall B B',
  B != B' -> exists2 X1, X \proper gval X1 & p.-Sylow(B :&: L) X1}.
- move=> _ _ /setIdP[/imsetP[a Ga ->] sXMa] /setIdP[/imsetP[b Gb ->] sXMb].
  move=> neqMab.
  have [S sylS sXS] := Sylow_superset sXMa pX; have [sSMa pS _] := and3P sylS.
  have [defS | ltXS] := eqVproper sXS.
    case/eqP: neqMab; apply: (canRL (actKV _ _)); apply: (act_inj 'Js a).
    rewrite /= -conjsgM [_ :^ _]conjGid ?(sigma_Sylow_trans _ sylS) ?sigmaJ //.
    by rewrite -defS conjsgM conjSg sub_conjgV.
  have pSL: p.-group (S :&: L) := pgroupS (subsetIl _ _) pS.
  have [X1 sylX1 sNX1] := Sylow_superset (setSI L sSMa) pSL; exists X1 => //.
  by rewrite (proper_sub_trans (nilpotent_proper_norm (pgroup_nil pS) _)).
have [M1 O_M1] := ntOM X pX; apply/imsetP; exists (gval M1) => //; apply/eqP.
rewrite eqEsubset andbC acts_sub_orbit ?(subset_trans (cent_sub X)) // O_M1 /=.
apply/subsetP=> M2 O_M2.
have [-> | neqM12] := eqsVneq M1 M2; first exact: orbit_refl.
have [|X2 ltXX2 sylX2] := IH_L _ _ O_M2 O_M1; first by rewrite eq_sym.
have{IH_L neqM12} [X1 ltXX1 sylX1] := IH_L _ _ O_M1 O_M2 neqM12.
have [[sX1L1 pX1 _] [sX2L2 pX2 _]] := (and3P sylX1, and3P sylX2).
have [[sX1M1 sX1L] [sX2M2 sX2L]] := (subsetIP sX1L1, subsetIP sX2L2).
have [P sylP sX1P] := Sylow_superset sX1L pX1; have [sPL pP _] := and3P sylP.
have [M0 O_M0] := ntOM P pP; have [MG_M0 sPM0] := setIdP O_M0.
have [t Lt sX2Pt] := Sylow_subJ sylP sX2L pX2.
have [sX1M0 ltXP] := (subset_trans sX1P sPM0, proper_sub_trans ltXX1 sX1P).
have M0C_M1: gval M1 \in orbit 'Js 'C(X) M0.
  rewrite (subsetP (imsetS _ (centS (proper_sub ltXX1)))) // -orbitE.
  by rewrite (atransP (IHX _ ltXX1 pX1)) inE ?MG_M0 //; case/setIdP: O_M1 => ->.
have M0tC_M2: M2 \in orbit 'Js 'C(X) (M0 :^ t).
  rewrite (subsetP (imsetS _ (centS (proper_sub ltXX2)))) // -orbitE.
  rewrite (atransP (IHX _ ltXX2 pX2)) inE; first by case/setIdP: O_M2 => ->.
  rewrite (acts_act (acts_orbit _ _ _)) ?inE ?MG_M0 //.
  by rewrite (subset_trans sX2Pt) ?conjSg.
rewrite (orbit_eqP M0C_M1) (orbit_transl _ M0tC_M2).
have maxM0 := maxOM _ _ O_M0; have ltMG := mmax_proper maxM0.
have [rPgt2 | rPle2] := ltnP 2 'r(P).
  have uP: P \in 'U by rewrite rank3_Uniqueness ?(mFT_pgroup_proper pP).
  have uP_M0: 'M(P) = [set M0] := def_uniq_mmax uP maxM0 sPM0.
  by rewrite conjGid ?orbit_refl ?(subsetP (sub_uniq_mmax uP_M0 sPL ltLG)).
have pl1L: p.-length_1 L.
  have [oddL]: odd #|L| /\ 'r_p(L) <= 2 by rewrite mFT_odd -(rank_Sylow sylP).
  by case/rank2_der1_complement; rewrite ?mFT_sol ?plength1_pseries2_quo.
have [|u v nLPu Lp'_v ->] := imset2P (_ : t \in 'N_L(P) * 'O_p^'(L)).
  by rewrite normC ?plength1_Frattini // subIset ?gFnorm.
rewrite actM (orbit_transl _ (mem_orbit _ _ _)); last first.
  have coLp'X: coprime #|'O_p^'(L)| #|X| := p'nat_coprime (pcore_pgroup _ _) pX.
  apply: subsetP Lp'_v; have [sLp'L nLp'L] := andP (pcore_normal p^' L).
  rewrite -subsetIidl -coprime_norm_cent ?subsetIidl //.
  exact: subset_trans (normG X) nLp'L.
have [|w x nM0Pw cPx ->] := imset2P (_ : u \in 'N_M0(P) * 'C(P)).
  rewrite normC ?part_c ?IHX //; first by case/setIP: nLPu.
  by rewrite setIC subIset ?cent_norm.
rewrite actM /= conjGid ?mem_orbit //; last by case/setIP: nM0Pw.
by rewrite (subsetP (centS (subset_trans (proper_sub ltXX1) sX1P))).
Qed.

Section OneMaximal.

Variable M : {group gT}.
Hypothesis maxM : M \in 'M.

Let ltMG := mmax_proper maxM.
Let solM := mmax_sol maxM.

Let aMa : \alpha(M).-group (M`_\alpha). Proof. exact: pcore_pgroup. Qed.
Let nsMaM : M`_\alpha <| M. Proof. exact: pcore_normal. Qed.
Let sMaMs : M`_\alpha \subset M`_\sigma. Proof. exact: Malpha_sub_Msigma. Qed.

Let F := 'F(M / M`_\alpha).
Let nsFMa : F <| M / M`_\alpha. Proof. exact: Fitting_normal. Qed.

Let alpha'F : \alpha(M)^'.-group F.
Proof.
rewrite -[F](nilpotent_pcoreC \alpha(M) (Fitting_nil _)) -Fitting_pcore /=.
by rewrite trivg_pcore_quotient (trivgP (Fitting_sub 1)) dprod1g pcore_pgroup.
Qed.

Let Malpha_quo_sub_Fitting : M^`(1) / M`_\alpha \subset F.
Proof.
have [/= K defF sMaK nsKM] := inv_quotientN nsMaM nsFMa; rewrite -/F in defF.
have [sKM _] := andP nsKM; have nsMaK: M`_\alpha <| K := normalS sMaK sKM nsMaM.
have [[_ nMaK] [_ nMaM]] := (andP nsMaK, andP nsMaM).
have hallMa: \alpha(M).-Hall(K) M`_\alpha.
  by rewrite /pHall sMaK pcore_pgroup -card_quotient -?defF.
have [H hallH] := Hall_exists \alpha(M)^' (solvableS sKM solM).
have{hallH} defK := sdprod_normal_p'HallP nsMaK hallH hallMa.
have{defK} [_ sHK defK nMaH tiMaH] := sdprod_context defK.
have{defK} isoHF: H \isog F by rewrite [F]defF -defK quotientMidl quotient_isog.
have{sHK nMaH} sHM := subset_trans sHK sKM.
have{tiMaH isoHF sHM H} rF: 'r(F) <= 2.
  rewrite -(isog_rank isoHF); have [p p_pr -> /=] := rank_witness H.
  have [|a_p] := leqP 'r_p(M) 2; first exact: leq_trans (p_rankS p sHM).
  rewrite 2?leqW // leqNgt p_rank_gt0 /= (card_isog isoHF) /= -/F.
  exact: contraL (pnatPpi alpha'F) a_p.
by rewrite quotient_der // rank2_der1_sub_Fitting ?mFT_quo_odd ?quotient_sol.
Qed.

Let sigma_Hall_sub_der1 H : \sigma(M).-Hall(M) H -> H \subset M^`(1).
Proof.
move=> hallH; have [sHM sH _] := and3P hallH.
rewrite -(Sylow_gen H) gen_subG; apply/bigcupsP=> P /SylowP[p p_pr sylP].
have [-> | ntP] := eqsVneq P 1; first by rewrite sub1G.
have [sPH pP _] := and3P sylP; have{ntP} [_ p_dv_P _] := pgroup_pdiv pP ntP.
have{p_dv_P} s_p: p \in \sigma(M) := pgroupP (pgroupS sPH sH) p p_pr p_dv_P.
have{sylP} sylP: p.-Sylow(M) P := subHall_Sylow hallH s_p sylP.
have [sPM nMP] := (pHall_sub sylP, norm_sigma_Sylow s_p sylP).
have sylP_G := sigma_Sylow_G maxM s_p sylP.
have defG': G^`(1) = G.
  have [_ simpG] := simpleP _ (mFT_simple gT).
  by have [?|//] := simpG _ (der_normal 1 _); case/derG1P: (mFT_nonAbelian gT).
rewrite -subsetIidl -{1}(setIT P) -defG'.
rewrite (focal_subgroup_gen sylP_G) (focal_subgroup_gen sylP) genS //.
apply/subsetP=> _ /imset2P[x g Px /setIdP[Gg Pxg] ->].
pose X := <[x]>; have sXM : X \subset M by rewrite cycle_subG (subsetP sPM).
have sXgM: X :^ g \subset M by rewrite -cycleJ cycle_subG (subsetP sPM).
have [trMX _ _] := sigma_group_trans maxM s_p (mem_p_elt pP Px).
have [c cXc [m Mm def_g]] := trMX _ sXM sXgM; rewrite cent_cycle in cXc.
have def_xg: x ^ g = x ^ m by rewrite def_g conjgM /conjg -(cent1P cXc) mulKg.
by rewrite commgEl def_xg -commgEl mem_imset2 // inE Mm -def_xg.
Qed.

(* This is B & G, Theorem 10.2(a1). *) 
Theorem Malpha_Hall : \alpha(M).-Hall(M) M`_\alpha.
Proof.
have [H hallH] := Hall_exists \sigma(M) solM; have [sHM sH _] := and3P hallH.
rewrite (subHall_Hall hallH (alpha_sub_sigma maxM)) // /pHall pcore_pgroup /=.
rewrite -(card_quotient (subset_trans sHM (normal_norm nsMaM))) -pgroupE.
rewrite (subset_trans sMaMs) ?pcore_sub_Hall ?(pgroupS _ alpha'F) //=.
exact: subset_trans (quotientS _ (sigma_Hall_sub_der1 hallH)) _.
Qed.

(* This is B & G, Theorem 10.2(b1). *) 
Theorem Msigma_Hall : \sigma(M).-Hall(M) M`_\sigma.
Proof.
have [H hallH] := Hall_exists \sigma(M) solM; have [sHM sH _] := and3P hallH.
rewrite /M`_\sigma (normal_Hall_pcore hallH) // -(quotientGK nsMaM).
rewrite -(quotientGK (normalS _ sHM nsMaM)) ?cosetpre_normal //; last first.
  by rewrite (subset_trans sMaMs) ?pcore_sub_Hall.
have hallHa: \sigma(M).-Hall(F) (H / M`_\alpha).
  apply: pHall_subl (subset_trans _ Malpha_quo_sub_Fitting) (Fitting_sub _) _.
    by rewrite quotientS ?sigma_Hall_sub_der1.
  exact: quotient_pHall (subset_trans sHM (normal_norm nsMaM)) hallH.
rewrite (nilpotent_Hall_pcore (Fitting_nil _) hallHa) /=.
exact: char_normal_trans (pcore_char _ _) nsFMa.
Qed.

Lemma pi_Msigma : \pi(M`_\sigma) =i \sigma(M).
Proof.
move=> p; apply/idP/idP=> [|s_p /=]; first exact: pnatPpi (pcore_pgroup _ _).
by rewrite (card_Hall Msigma_Hall) pi_of_part // inE /= sigma_sub_pi.
Qed.

(* This is B & G, Theorem 10.2(b2). *) 
Theorem Msigma_Hall_G : \sigma(M).-Hall(G) M`_\sigma.
Proof.
rewrite pHallE subsetT /= eqn_dvd {1}(card_Hall Msigma_Hall).
rewrite partn_dvd ?cardG_gt0 ?cardSg ?subsetT //=.
apply/dvdn_partP; rewrite ?part_gt0 // => p.
rewrite pi_of_part ?cardG_gt0 // => /andP[_ s_p].
rewrite partn_part => [|q /eqnP-> //].
have [P sylP] := Sylow_exists p M; have [sPM pP _] := and3P sylP.
rewrite -(card_Hall (sigma_Sylow_G _ _ sylP)) ?cardSg //.
by rewrite (sub_Hall_pcore Msigma_Hall) ?(pi_pgroup pP).
Qed.

(* This is B & G, Theorem 10.2(a2). *) 
Theorem Malpha_Hall_G : \alpha(M).-Hall(G) M`_\alpha.
Proof.
apply: subHall_Hall Msigma_Hall_G (alpha_sub_sigma maxM) _.
exact: pHall_subl sMaMs (pcore_sub _ _) Malpha_Hall.
Qed.

(* This is B & G, Theorem 10.2(c). *)
Theorem Msigma_der1 : M`_\sigma \subset M^`(1).
Proof. exact: sigma_Hall_sub_der1 Msigma_Hall. Qed.

(* This is B & G, Theorem 10.2(d1). *)
Theorem Malpha_quo_rank2 : 'r(M / M`_\alpha) <= 2.
Proof.
have [p p_pr ->] := rank_witness (M / M`_\alpha).
have [P sylP] := Sylow_exists p M; have [sPM pP _] := and3P sylP.
have nMaP := subset_trans sPM (normal_norm nsMaM).
rewrite -(rank_Sylow (quotient_pHall nMaP sylP)) /= leqNgt.
have [a_p | a'p] := boolP (p \in \alpha(M)).
  by rewrite quotientS1 ?rank1 ?(sub_Hall_pcore Malpha_Hall) ?(pi_pgroup pP).
rewrite -(isog_rank (quotient_isog _ _)) ?coprime_TIg ?(rank_Sylow sylP) //.
exact: pnat_coprime aMa (pi_pnat pP _).
Qed.

(* This is B & G, Theorem 10.2(d2). *)
Theorem Malpha_quo_nil : nilpotent (M^`(1) / M`_\alpha).
Proof. exact: nilpotentS Malpha_quo_sub_Fitting (Fitting_nil _). Qed.

(* This is B & G, Theorem 10.2(e). *)
Theorem Msigma_neq1 : M`_\sigma :!=: 1.
Proof.
without loss Ma1: / M`_\alpha = 1.
  by case: eqP => // Ms1 -> //; apply/trivgP; rewrite -Ms1 Malpha_sub_Msigma.
have{Ma1} rFM: 'r('F(M)) <= 2.
  rewrite (leq_trans _ Malpha_quo_rank2) // Ma1.
  by rewrite -(isog_rank (quotient1_isog _)) rankS ?Fitting_sub.
pose q := max_pdiv #|M|; pose Q := 'O_q(M)%G.
have sylQ: q.-Sylow(M) Q := rank2_max_pcore_Sylow (mFT_odd M) solM rFM.
have piMq: q \in \pi(M) by rewrite pi_max_pdiv cardG_gt1 mmax_neq1.
have{piMq} ntQ: Q :!=: 1 by rewrite -rank_gt0 (rank_Sylow sylQ) p_rank_gt0.
rewrite (subG1_contra _ ntQ) ?(sub_Hall_pcore Msigma_Hall) ?pcore_sub //.
rewrite (pi_pgroup (pcore_pgroup _ _)) //; apply/exists_inP; exists Q => //.
by rewrite (mmax_normal maxM) ?pcore_normal.
Qed.

(* This is B & G, Lemma 10.3. *)
Theorem cent_alpha'_uniq X :
     X \subset M -> \alpha(M)^'.-group X -> 'r('C_(M`_\alpha)(X)) >= 2 ->
  'C_M(X)%G \in 'U.
Proof.
have ltM_G := sub_proper_trans (subsetIl M _) ltMG.
move=> sXM a'X; have [p p_pr -> rCX] := rank_witness 'C_(M`_\alpha)(X).
have{rCX} [B EpB] := p_rank_geP rCX; have{EpB} [sBCX abelB dimB] := pnElemP EpB.
have [[sBMa cXB] [pB cBB _]] := (subsetIP sBCX, and3P abelB).
have rMa: 1 < 'r_p(M`_\alpha) by rewrite -dimB -p_rank_abelem ?p_rankS.
have{rMa} a_p: p \in \alpha(M) by rewrite (pnatPpi aMa) // -p_rank_gt0 ltnW.
have nBX: X \subset 'N(B) by rewrite cents_norm // centsC.
have coMaX: coprime #|M`_\alpha| #|X| := pnat_coprime aMa a'X.
have [sMaM nMaM] := andP nsMaM; have solMa := solvableS sMaM solM.
have nMaX := subset_trans sXM nMaM.
have [P [sylP nPX sBP]] := coprime_Hall_subset nMaX coMaX solMa sBMa pB nBX.
have [sPMa pP _] := and3P sylP; have sPM := subset_trans sPMa sMaM.
have EpCB: B \in 'E_p^2('C_P(B)) by rewrite !inE subsetI sBP abelB dimB !andbT.
have: 1 < 'r_p('C_P(B)) by apply/p_rank_geP; exists B.
rewrite leq_eqVlt; case: ltngtP => // rCPB _.
  apply: (uniq_mmaxS (subset_trans sBCX (setSI _ sMaM))) => //=.
  have pCPB := pgroupS (subsetIl P 'C(B)) pP; rewrite -rank_pgroup // in rCPB.
  have: 2 < 'r('C(B)) by rewrite (leq_trans rCPB) ?rankS ?subsetIr.
  by apply: cent_rank3_Uniqueness; rewrite -dimB -rank_abelem.
have cPX: P \subset 'C(X).
  have EpPB: B \in 'E_p(P) by apply/pElemP.
  have coPX: coprime #|P| #|X| := coprimeSg sPMa coMaX.
  rewrite centsC (coprime_odd_faithful_cent_abelem EpPB) ?mFT_odd //.
  rewrite -(setIid 'C(B)) setIA (pmaxElem_LdivP p_pr _) 1?centsC //.
  by rewrite (subsetP (p_rankElem_max _ _)) -?rCPB.
have sylP_M := subHall_Sylow Malpha_Hall a_p sylP.
have{sylP_M} rP: 2 < 'r(P) by rewrite (rank_Sylow sylP_M).
by rewrite rank3_Uniqueness ?(leq_trans rP (rankS _)) //= subsetI sPM.
Qed.

Variable p : nat.

(* This is B & G, Lemma 10.4(a). *)
(* We omit the redundant assumption p \in \pi(M). *)
Lemma der1_quo_sigma' : p %| #|M / M^`(1)| -> p \in \sigma(M)^'.
Proof.
apply: contraL => /= s_p; have piMp := sigma_sub_pi maxM s_p.
have p_pr: prime p by move: piMp; rewrite mem_primes; case/andP.
rewrite -p'natE ?(pi'_p'nat _ s_p) // -pgroupE -partG_eq1.
rewrite -(card_Hall (quotient_pHall _ Msigma_Hall)) /=; last first.
  exact/gFsub_trans/gFnorm.
by rewrite quotientS1 ?cards1 // Msigma_der1.
Qed.

Hypothesis s'p : p \in \sigma(M)^'.

(* This is B & G, Lemma 10.4(b). *)
(* We do not need the assumption M`_\alpha != 1; the assumption p \in \pi(M)  *)
(* is restated as P != 1.                                                     *)
Lemma cent1_sigma'_Zgroup P :
    p.-Sylow(M) P -> P :!=: 1 ->
  exists x,
    [/\ x \in 'Ohm_1('Z(P))^#, 'M('C[x]) != [set M] & Zgroup 'C_(M`_\alpha)[x]].
Proof.
move=> sylP ntP; have [sPM pP _] := and3P sylP; have nilP := pgroup_nil pP.
set T := 'Ohm_1('Z(P)); have charT: T \char P by rewrite !gFchar_trans.
suffices [x Tx not_uCx]: exists2 x, x \in T^# & 'M('C[x]) != [set M].
  exists x; split=> //; rewrite odd_rank1_Zgroup ?mFT_odd //= leqNgt.
  apply: contra not_uCx; rewrite -cent_cycle; set X := <[x]> => rCMaX.
  have{Tx} [ntX Tx] := setD1P Tx; rewrite -cycle_eq1 -/X in ntX.
  have sXP: X \subset P by rewrite cycle_subG (subsetP (char_sub charT)).
  rewrite (@def_uniq_mmaxS _ M 'C_M(X)) ?subsetIr ?mFT_cent_proper //.
  apply: def_uniq_mmax; rewrite ?subsetIl //.
  rewrite cent_alpha'_uniq ?(subset_trans sXP) ?(pi_pgroup (pgroupS sXP pP)) //.
  by apply: contra s'p; apply: alpha_sub_sigma.
apply/exists_inP; rewrite -negb_forall_in; apply: contra s'p.
move/forall_inP => uCT; apply/exists_inP; exists P => //.
apply/subsetP=> u nPu; have [y Ty]: exists y, y \in T^#.
  by apply/set0Pn; rewrite setD_eq0 subG1 Ohm1_eq1 center_nil_eq1.
rewrite -(norm_mmax maxM) (sameP normP eqP) (inj_eq (@group_inj gT)) -in_set1.
have Tyu: y ^ u \in T^#.
  by rewrite memJ_norm // normD1 (subsetP (char_norms charT)).
by rewrite -(eqP (uCT _ Tyu)) -conjg_set1 normJ mmax_ofJ (eqP (uCT _ Ty)) set11.
Qed.

(* This is B & G, Lemma 10.4(c), part 1. *)
(* The redundant assumption p \in \pi(M) is omitted. *)
Lemma sigma'_rank2_max : 'r_p(M) = 2 -> 'E_p^2(M) \subset 'E*_p(G).
Proof.
move=> rpM; apply: contraR s'p => /subsetPn[A Ep2A not_maxA].
have{Ep2A} [sAM abelA dimA] := pnElemP Ep2A; have [pA _ _] := and3P abelA.
have [P sylP sAP] := Sylow_superset sAM pA; have [_ pP _] := and3P sylP.
apply/exists_inP; exists P; rewrite ?uniq_mmax_norm_sub //.
apply: def_uniq_mmaxS (mFT_pgroup_proper pP) (def_uniq_mmax _ _ sAM) => //.
by rewrite (@nonmaxElem2_Uniqueness _ p) // !(not_maxA, inE) abelA dimA subsetT.
Qed.

(* This is B & G, Lemma 10.4(c), part 2 *)
(* The redundant assumption p \in \pi(M) is omitted. *)
Lemma sigma'_rank2_beta' : 'r_p(M) = 2 -> p \notin \beta(G).
Proof.
move=> rpM; rewrite -[p \in _]negb_exists_in negbK; apply/exists_inP.
have [A Ep2A]: exists A, A \in 'E_p^2(M) by apply/p_rank_geP; rewrite rpM.
have [_ abelA dimA] := pnElemP Ep2A; have [pA _] := andP abelA.
have [P sylP sAP] := Sylow_superset (subsetT _) pA.
exists P; rewrite ?inE //; apply/implyP=> _; apply/set0Pn.
exists A; rewrite 3!inE abelA dimA sAP (subsetP (pmaxElemS _ (subsetT P))) //.
by rewrite inE (subsetP (sigma'_rank2_max rpM)) // inE.
Qed.

(* This is B & G, Lemma 10.5, part 1; the condition on X has been weakened,   *)
(* because the proof of Lemma 12.2(a) requires the stronger result.           *)
Lemma sigma'_norm_mmax_rank2 X : p.-group X -> 'N(X) \subset M -> 'r_p(M) = 2.
Proof.
move=> pX sNX_M; have sXM: X \subset M := subset_trans (normG X) sNX_M.
have [P sylP sXP] := Sylow_superset sXM pX; have [sPM pP _] := and3P sylP.
apply: contraNeq s'p; case: ltngtP => // rM _; last exact: alpha_sub_sigma.
apply/exists_inP; exists P; rewrite ?(subset_trans _ sNX_M) ?char_norms //.
rewrite sub_cyclic_char // (odd_pgroup_rank1_cyclic pP) ?mFT_odd //.
by rewrite (p_rank_Sylow sylP).
Qed.

(* This is B & G, Lemma 10.5, part 2. We omit the second claim of B & G 10.5  *)
(* as it is an immediate consequence of sigma'_rank2_beta' (i.e., 10.4(c)).   *)
Lemma sigma'1Elem_sub_p2Elem X :
    X \in 'E_p^1(G) -> 'N(X) \subset M -> 
  exists2 A, A \in 'E_p^2(G) & X \subset A.
Proof.
move=> EpX sNXM; have sXM := subset_trans (normG X) sNXM.
have [[_ abelX dimX] p_pr] := (pnElemP EpX, pnElem_prime EpX).
have pX := abelem_pgroup abelX; have rpM2 := sigma'_norm_mmax_rank2 pX sNXM.
have [P sylP sXP] := Sylow_superset sXM pX; have [sPM pP _] := and3P sylP.
pose T := 'Ohm_1('Z(P)); pose A := X <*> T; have nilP := pgroup_nil pP.
have charT: T \char P by apply/gFchar_trans/gFchar.
have neqTX: T != X.
  apply: contraNneq s'p => defX; apply/exists_inP; exists P => //.
  by rewrite (subset_trans _ sNXM) // -defX char_norms.
have rP: 'r(P) = 2 by rewrite (rank_Sylow sylP) rpM2.
have ntT: T != 1 by rewrite Ohm1_eq1 center_nil_eq1 // -rank_gt0 rP.
have sAP: A \subset P by rewrite join_subG sXP char_sub.
have cTX: T \subset 'C(X) := centSS (Ohm_sub 1 _) sXP (subsetIr P _).
have{cTX} defA: X \* T = A by rewrite cprodEY.
have{defA} abelA : p.-abelem A.
  have pZ: p.-group 'Z(P) := pgroupS (center_sub P) pP.
  by rewrite (cprod_abelem _ defA) abelX Ohm1_abelem ?center_abelian.
exists [group of A]; last exact: joing_subl.
rewrite !inE subsetT abelA eqn_leq -{1}rP -{1}(rank_abelem abelA) rankS //=.
rewrite -dimX (properG_ltn_log (pgroupS sAP pP)) // /proper join_subG subxx.
rewrite joing_subl /=; apply: contra ntT => sTX; rewrite eqEsubset sTX in neqTX.
by rewrite -(setIidPr sTX) prime_TIg ?(card_pnElem EpX).
Qed.

End OneMaximal.

(* This is B & G, Theorem 10.6. *)
Theorem mFT_proper_plength1 p H : H \proper G -> p.-length_1 H.
Proof.
case/mmax_exists=> M /setIdP[maxM sHM].
suffices{H sHM}: p.-length_1 M by apply: plength1S.
have [solM oddM] := (mmax_sol maxM, mFT_odd M).
have [rpMle2 | a_p] := leqP 'r_p(M) 2.
  by rewrite plength1_pseries2_quo; case/rank2_der1_complement: rpMle2.
pose Ma := M`_\alpha; have hallMa: \alpha(M).-Hall(M) Ma := Malpha_Hall maxM.
have [[K hallK] [sMaM aMa _]] := (Hall_exists \alpha(M)^' solM, and3P hallMa).
have defM: Ma ><| K = M by apply/sdprod_Hall_pcoreP.
have{aMa} coMaK: coprime #|Ma| #|K| := pnat_coprime aMa (pHall_pgroup hallK).
suffices{a_p hallMa}: p.-length_1 Ma.
  rewrite !p_elt_gen_length1 /p_elt_gen setIdE /= -/Ma -(setIidPl sMaM) -setIA.
  rewrite -(setIdE M) (setIidPr _) //; apply/subsetP=> x; case/setIdP=> Mx p_x.
  by rewrite (mem_Hall_pcore hallMa) /p_elt ?(pi_pnat p_x).
have{sMaM} <-: [~: Ma, K] = Ma.
  have sMaMs: Ma \subset M`_\sigma := Malpha_sub_Msigma maxM.
  have sMaM': Ma \subset M^`(1) := subset_trans sMaMs (Msigma_der1 maxM).
  by have [] := coprime_der1_sdprod defM coMaK (solvableS sMaM solM) sMaM'.
have [q q_pr q_dv_Mq]: {q | prime q & q %| #|M / M^`(1)| }.
  apply: pdivP; rewrite card_quotient ?der_norm // indexg_gt1 proper_subn //.
  by rewrite (sol_der1_proper solM) ?mmax_neq1.
have s'q: q \in \sigma(M)^' by apply: der1_quo_sigma' q_dv_Mq.
have [Q sylQ] := Sylow_exists q K; have [sQK qQ _] := and3P sylQ.
have a'q: q \in \alpha(M)^' by apply: contra s'q; apply: alpha_sub_sigma.
have{a'q sylQ hallK} sylQ: q.-Sylow(M) Q := subHall_Sylow hallK a'q sylQ.
have{q_dv_Mq} ntQ: Q :!=: 1.
  rewrite -rank_gt0 (rank_Sylow sylQ) p_rank_gt0 mem_primes q_pr cardG_gt0.
  exact: dvdn_trans q_dv_Mq (dvdn_quotient _ _).
have{s'q sylQ ntQ} [x [Q1x _ ZgCx]] := cent1_sigma'_Zgroup maxM s'q sylQ ntQ.
have{Q1x} [ntx Q1x] := setD1P Q1x.
have sZQ := center_sub Q; have{sQK} sZK := subset_trans sZQ sQK.
have{sZK} Kx: x \in K by rewrite (subsetP sZK) // (subsetP (Ohm_sub 1 _)).
have{sZQ qQ} abelQ1 := Ohm1_abelem (pgroupS sZQ qQ) (center_abelian Q).
have{q q_pr Q abelQ1 Q1x} ox: prime #[x] by rewrite (abelem_order_p abelQ1).
move: Kx ox ZgCx; rewrite -cycle_subG -cent_cycle.
exact: odd_sdprod_Zgroup_cent_prime_plength1 solM oddM defM coMaK.
Qed.

Section OneSylow.

Variables (p : nat) (P : {group gT}).
Hypothesis sylP_G: p.-Sylow(G) P.
Let pP : p.-group P := pHall_pgroup sylP_G.

(* This is an B & G, Corollary 10.7(a), second part (which does not depend on *)
(* a particular complement).                                                  *)
Corollary mFT_Sylow_der1 : P \subset 'N(P)^`(1).
Proof.
have [-> | ntP] := eqsVneq P 1; first exact: sub1G.
have ltNG: 'N(P) \proper G := mFT_norm_proper ntP (mFT_pgroup_proper pP).
have [M /setIdP[/= maxM sNM]] := mmax_exists ltNG.
have [ltMG solM] := (mmax_proper maxM, mmax_sol maxM).
have [pl1M sPM] := (mFT_proper_plength1 p ltMG, subset_trans (normG P) sNM).
have sylP := pHall_subl sPM (subsetT M) sylP_G.
have sMp: p \in \sigma(M) by apply/exists_inP; exists P.
apply: subset_trans (dergS 1 (subsetIr M 'N(P))) => /=.
apply: plength1_Sylow_sub_der1 sylP pl1M (subset_trans _ (Msigma_der1 maxM)).
by rewrite (sub_Hall_pcore (Msigma_Hall maxM)) ?(pi_pgroup pP).
Qed.

(* This is B & G, Corollary 10.7(a), first part. *)
Corollary mFT_Sylow_sdprod_commg V : P ><| V = 'N(P) -> [~: P, V] = P.
Proof.
move=> defV; have sPN' := mFT_Sylow_der1.
have sylP := pHall_subl (normG P) (subsetT 'N(P)) sylP_G.
have [|//] := coprime_der1_sdprod defV _ (pgroup_sol pP) sPN'.
by rewrite (coprime_sdprod_Hall_l defV) // (pHall_Hall sylP).
Qed.

(* This is B & G, Corollary 10.7(b). *)
Corollary mFT_rank2_Sylow_cprod :
    'r(P) < 3 -> ~~ abelian P ->
  exists2 S, [/\ ~~ abelian (gval S), logn p #|S| = 3 & exponent S %| p]
  & exists2 C, cyclic (gval C) & S \* C = P /\ 'Ohm_1(C) = 'Z(S).
Proof.
move=> rP not_cPP; have sylP := pHall_subl (normG P) (subsetT 'N(P)) sylP_G.
have ntP: P :!=: 1 by apply: contraNneq not_cPP => ->; apply: abelian1.
have ltNG: 'N(P) \proper G := mFT_norm_proper ntP (mFT_pgroup_proper pP).
have [V hallV] := Hall_exists p^' (mFT_sol ltNG); have [_ p'V _] := and3P hallV.
have defNP: P ><| V = 'N(P) := sdprod_normal_p'HallP (normalG P) hallV sylP.
have defP: [~: P, V] = P := mFT_Sylow_sdprod_commg defNP.
have [_] := rank2_coprime_comm_cprod pP (mFT_odd _) ntP rP defP p'V (mFT_odd _).
case=> [/idPn// | [S esS [C [mulSC cycC defC1]]]].
exists S => //; exists C => //; split=> //; rewrite defC1.
have sSP: S \subset P by case/cprodP: mulSC => _ /mulG_sub[].
have [[not_cSS dimS _] pS] := (esS, pgroupS sSP pP).
by have [||[]] := p3group_extraspecial pS; rewrite ?dimS.
Qed.

(* This is B & G, Corollary 10.7(c). *)
Corollary mFT_sub_Sylow_trans : forall Q x,
  Q \subset P -> Q :^ x \subset P -> exists2 y, y \in 'N(P) & Q :^ x = Q :^ y.
Proof.
move=> Q x; have [-> /trivgP-> /trivgP-> | ntP sQP sQxP] := eqsVneq P 1.
  by exists 1; rewrite ?group1 ?conjs1g.
have ltNG: 'N(P) \proper G := mFT_norm_proper ntP (mFT_pgroup_proper pP).
have [M /=] := mmax_exists ltNG; case/setIdP=> maxM sNM.
have [ltMG solM] := (mmax_proper maxM, mmax_sol maxM).
have [pl1M sPM] := (mFT_proper_plength1 p ltMG, subset_trans (normG P) sNM).
have sylP := pHall_subl sPM (subsetT M) sylP_G.
have sMp: p \in \sigma(M) by apply/exists_inP; exists P.
have [transCQ _ _] := sigma_group_trans maxM sMp (pgroupS sQP pP).
have [||q cQq [u Mu defx]] := transCQ x; try exact: subset_trans _ sPM.
have nQC := normP (subsetP (cent_sub Q) _ _).
have [|q' cMQq' [y nMPy defu]] := plength1_Sylow_trans sylP pl1M solM sQP Mu.
  by rewrite defx conjsgM nQC in sQxP.
have [[_ nPy] [_ cQq']] := (setIP nMPy, setIP cMQq').
by exists y; rewrite // defx defu !conjsgM 2?nQC.
Qed.

(* This is B & G, Corollary 10.7(d). *)
Corollary mFT_subnorm_Sylow Q : Q \subset P -> p.-Sylow('N(Q)) 'N_P(Q).
Proof.
move=> sQP; have pQ := pgroupS sQP pP.
have [S /= sylS] := Sylow_exists p 'N(Q); have [sNS pS _] := and3P sylS.
have sQS: Q \subset S := normal_sub_max_pgroup (Hall_max sylS) pQ (normalG Q).
have [x _ sSxP] := Sylow_Jsub sylP_G (subsetT S) pS.
have sQxP: Q :^ x \subset P by rewrite (subset_trans _ sSxP) ?conjSg.
have [y nPy defQy] := mFT_sub_Sylow_trans sQP sQxP.
have nQxy: x * y^-1 \in 'N(Q) by rewrite inE conjsgM defQy actK.
have sSxyP: S :^ (x * y^-1) \subset P by rewrite conjsgM sub_conjgV (normP nPy).
have sylSxy: p.-Sylow('N(Q)) (S :^ (x * y^-1)) by rewrite pHallJ.
have pNPQ: p.-group 'N_P(Q) := pgroupS (subsetIl P 'N(Q)) pP.
by rewrite (sub_pHall sylSxy pNPQ) ?subsetIr // subsetI sSxyP (@pHall_sub _ p).
Qed.

(* This is B & G, Corollary 10.7(e). *)
Corollary mFT_Sylow_normalS Q R :
  p.-group R -> Q \subset P :&: R -> Q <| 'N(P) -> Q <| 'N(R).
Proof.
move=> pR /subsetIP[sQP sQR] /andP[nQP nQ_NP].
have [x _ sRxP] := Sylow_Jsub sylP_G (subsetT R) pR.
rewrite /normal normsG //; apply/subsetP=> y nRy.
have sQxP: Q :^ x \subset P by rewrite (subset_trans _ sRxP) ?conjSg.
have sQyxP: Q :^ (y * x) \subset P.
  by rewrite actM (subset_trans _ sRxP) // -(normP nRy) !conjSg.
have [t tNP defQx] := mFT_sub_Sylow_trans sQP sQxP.
have [z zNP defQxy] := mFT_sub_Sylow_trans sQP sQyxP.
by rewrite inE -(conjSg _ _ x) -actM /= defQx defQxy !(normsP nQ_NP).
Qed.

End OneSylow.

Section AnotherMaximal.

Variable M : {group gT}.
Hypothesis maxM : M \in 'M.

Let solM : solvable M := mmax_sol maxM.
Let ltMG : M \proper G := mmax_proper maxM.

Let sMbMs : M`_\beta \subset M`_\sigma := Mbeta_sub_Msigma maxM.
Let nsMbM : M`_\beta <| M := pcore_normal _ _.

Let hallMs : \sigma(M).-Hall(M) M`_\sigma := Msigma_Hall maxM.
Let nsMsM : M`_\sigma <| M := pcore_normal _ M.
Let sMsM' : M`_\sigma \subset M^`(1) := Msigma_der1 maxM.

Lemma Mbeta_der1 : M`_\beta \subset M^`(1).
Proof. exact: subset_trans sMbMs sMsM'. Qed.

Let sM'M : M^`(1) \subset M := der_sub 1 M.
Let nsMsM' : M`_\sigma <| M^`(1) := normalS sMsM' sM'M nsMsM.
Let nsMbM' : M`_\beta <| M^`(1) := normalS Mbeta_der1 sM'M nsMbM.
Let nMbM' := normal_norm nsMbM'.

(* This is B & G, Lemma 10.8(c). *)
Lemma beta_max_pdiv p :
    p \notin \beta(M) ->
  [/\ p^'.-Hall(M^`(1)) 'O_p^'(M^`(1)),
      p^'.-Hall(M`_\sigma) 'O_p^'(M`_\sigma)
    & forall q, q \in \pi(M / 'O_p^'(M)) -> q <= p].
Proof.
rewrite !inE -negb_exists_in negbK => /exists_inP[P sylP nnP].
have [|ncM' p_max] := narrow_der1_complement_max_pdiv (mFT_odd M) solM sylP nnP.
  by rewrite mFT_proper_plength1 ?implybT.
by rewrite -(pcore_setI_normal _ nsMsM') (Hall_setI_normal nsMsM').
Qed.

(* This is B & G, Lemma 10.8(a), first part. *)
Lemma Mbeta_Hall : \beta(M).-Hall(M) M`_\beta.
Proof.
have [H hallH] := Hall_exists \beta(M) solM; have [sHM bH _]:= and3P hallH.
rewrite [M`_\beta](sub_pHall hallH) ?pcore_pgroup ?pcore_sub //=.
rewrite -(setIidPl sMbMs) pcore_setI_normal ?pcore_normal //.
have sH: \sigma(M).-group H := sub_pgroup (beta_sub_sigma maxM) bH.
have sHMs: H \subset M`_\sigma by rewrite (sub_Hall_pcore hallMs).
rewrite -pcoreNK -bigcap_p'core subsetI sHMs.
apply/bigcapsP=> p b'p; have [_ hallKp' _] := beta_max_pdiv b'p.
by rewrite (sub_Hall_pcore hallKp') ?(pi_p'group bH).
Qed.

(* This is B & G, Lemma 10.8(a), second part. *)
Lemma Mbeta_Hall_G : \beta(M).-Hall(G) M`_\beta.
Proof.
apply: (subHall_Hall (Msigma_Hall_G maxM) (beta_sub_sigma maxM)).
exact: pHall_subl sMbMs (pcore_sub _ _) Mbeta_Hall.
Qed.

(* This is an equivalent form of B & G, Lemma 10.8(b), which is used directly *)
(* later in the proof (e.g., Corollary 10.9a below, and Lemma 12.11), and is  *)
(* proved as an intermediate step of the proof of of 12.8(b).                 *)
Lemma Mbeta_quo_nil : nilpotent (M^`(1) / M`_\beta).
Proof.
have /and3P[_ bMb b'M'Mb] := pHall_subl Mbeta_der1 sM'M Mbeta_Hall.
apply: nilpotentS (Fitting_nil (M^`(1) / M`_\beta)) => /=.
rewrite -{1}[_ / _]Sylow_gen gen_subG.
apply/bigcupsP=> Q /SylowP[q _ /and3P[sQM' qQ _]].
apply: subset_trans (pcore_sub q _).
rewrite p_core_Fitting -pcoreNK -bigcap_p'core subsetI sQM' /=.
apply/bigcapsP=> [[p /= _] q'p]; have [b_p | b'p] := boolP (p \in \beta(M)).
  by rewrite pcore_pgroup_id ?(pi'_p'group _ b_p) // /pgroup card_quotient.
have p'Mb: p^'.-group M`_\beta := pi_p'group bMb b'p.
rewrite sub_Hall_pcore ?(pi_p'group qQ) {Q qQ sQM'}//.
rewrite pquotient_pcore ?quotient_pHall 1?gFsub_trans //.
by have [-> _ _] := beta_max_pdiv b'p.
Qed.

(* This is B & G, Lemma 10.8(b), generalized to arbitrary beta'-subgroups of  *)
(* M^`(1) (which includes Hall beta'-subgroups of M^`(1) and M`_\beta).       *)
Lemma beta'_der1_nil H : \beta(M)^'.-group H -> H \subset M^`(1) -> nilpotent H.
Proof.
move=> b'H sHM'; have [_ bMb _] := and3P Mbeta_Hall.
have{b'H} tiMbH: M`_\beta :&: H = 1 := coprime_TIg (pnat_coprime bMb b'H).
rewrite {tiMbH}(isog_nil (quotient_isog (subset_trans sHM' nMbM') tiMbH)).
exact: nilpotentS (quotientS _ sHM') Mbeta_quo_nil.
Qed.

(* This is B & G, Corollary 10.9(a). *)
Corollary beta'_cent_Sylow p q X :
     p \notin \beta(M) -> q \notin \beta(M) -> q.-group X ->
     (p != q) && (X \subset M^`(1)) || (p < q) && (X \subset M) ->
  [/\ (*a1*) exists2 P, p.-Sylow(M`_\sigma) (gval P) & X \subset 'C(P),
      (*a2*) p \in \alpha(M) -> 'C_M(X)%G \in 'U
    & (*a3*) q.-Sylow(M^`(1)) X -> 
          exists2 P, p.-Sylow(M^`(1)) (gval P) & P \subset 'N_M(X)^`(1)].
Proof.
move=> b'p b'q qX q'p_sXM'; pose pq : nat_pred := pred2 p q.
have [q'p sXM]: p \in q^' /\ X \subset M.
  case/orP: q'p_sXM' => /andP[q'p /subset_trans-> //].
  by rewrite !inE neq_ltn q'p.
have sXM'M: X <*> M^`(1) \subset M by rewrite join_subG sXM.
have solXM': solvable (X <*> M^`(1)) := solvableS sXM'M solM.
have pqX: pq.-group X by rewrite (pi_pgroup qX) ?inE ?eqxx ?orbT.
have{solXM' pqX} [W /= hallW sXW] := Hall_superset solXM' (joing_subl _ _) pqX.
have [sWXM' pqW _] := and3P hallW; have sWM := subset_trans sWXM' sXM'M.
have{b'q} b'W: \beta(M)^'.-group W. (* GG -- Coq diverges on b'p <> b'q *)
  by apply: sub_pgroup pqW => r /pred2P[]->; [apply: b'p | apply: b'q].
have nilM'W: nilpotent (M^`(1) :&: W).
  by rewrite beta'_der1_nil ?subsetIl ?(pgroupS (subsetIr _ _)).
have{nilM'W} nilW: nilpotent W.
  do [case/orP: q'p_sXM'=> /andP[]] => [_ sXM' | lt_pq _].
    by rewrite -(setIidPr sWXM') (joing_idPr sXM').
  pose Wq := 'O_p^'(M) :&: W; pose Wp := 'O_p(M^`(1) :&: W).
  have nMp'M := char_norm (pcore_char p^' M).
  have nMp'W := subset_trans sWM nMp'M.
  have sylWq: q.-Sylow(W) Wq.
    have [sWqMp' sWp'W] := subsetIP (subxx Wq).
    have [Q sylQ] := Sylow_exists q W; have [sQW qQ _] := and3P sylQ.
    rewrite [Wq](sub_pHall sylQ _ _ (subsetIr _ W)) //= -/Wq.
      apply/pgroupP=> r r_pr r_dv_Wp'.
      have:= pgroupP (pgroupS sWqMp' (pcore_pgroup _ _)) r r_pr r_dv_Wp'.
      by apply/implyP; rewrite implyNb; apply: (pgroupP (pgroupS sWp'W pqW)).
    have [[_ _ max_p] sQM] := (beta_max_pdiv b'p, subset_trans sQW sWM).
    rewrite subsetI sQW -quotient_sub1 ?(subset_trans sQM nMp'M) //.
    apply: contraLR lt_pq; rewrite -leqNgt andbT subG1 -rank_gt0.
    rewrite (rank_pgroup (quotient_pgroup _ qQ)) p_rank_gt0 => piQb_q.
    exact: max_p (piSg (quotientS _ sQM) piQb_q).
  have nM'W: W \subset 'N(M^`(1)) by rewrite (subset_trans sWM) ?der_norm.
  have qWWM': q.-group (W / (M^`(1) :&: W)).
    rewrite (isog_pgroup _ (second_isog _)) ?(pgroupS (quotientS _ sWXM')) //=.
    by rewrite (quotientYidr (subset_trans sXW nM'W)) quotient_pgroup.
  have{qWWM'} sylWp: p.-Sylow(W) Wp.
    rewrite /pHall pcore_pgroup gFsub_trans ?subsetIr //=.
    rewrite -(Lagrange_index (subsetIr _ _) (pcore_sub _ _)) pnat_mul //.
    rewrite -(divgS (pcore_sub _ _)) -card_quotient ?normsI ?normG //= -pgroupE.
    rewrite (pi_p'group qWWM') //= -(dprod_card (nilpotent_pcoreC p nilM'W)).
    by rewrite mulKn ?cardG_gt0 // -pgroupE pcore_pgroup.
  have [[sWqW qWq _] [sWpW pWp _]] := (and3P sylWq, and3P sylWp).
  have <-: Wp * Wq = W.
    apply/eqP; rewrite eqEcard mul_subG //= -(partnC q (cardG_gt0 W)).
    rewrite (coprime_cardMg (p'nat_coprime (pi_pnat pWp _) qWq)) //.
    rewrite (card_Hall sylWp) (card_Hall sylWq) -{2}(part_pnat_id pqW) -partnI.
    rewrite mulnC (@eq_partn _ p) // => r.
    by rewrite !inE andb_orl andbN orbF; apply: andb_idr; move/eqP->.
  apply: nilpotentS (mul_subG _ _) (Fitting_nil W).
    rewrite Fitting_max ?(pgroup_nil pWp) //.
    by rewrite gFnormal_trans //= setIC norm_normalI.
  by rewrite Fitting_max ?(pgroup_nil qWq) //= setIC norm_normalI.
have part1: exists2 P : {group gT}, p.-Sylow(M`_\sigma) P & X \subset 'C(P).
  have sMsXM' := subset_trans sMsM' (joing_subr X _).
  have nsMsXM': M`_\sigma <| X <*> M^`(1) := normalS sMsXM' sXM'M nsMsM.
  have sylWp: p.-Hall(M`_\sigma) ('O_p(W) :&: M`_\sigma).
    rewrite setIC (Sylow_setI_normal nsMsXM') //.
    exact: subHall_Sylow hallW (predU1l _ _) (nilpotent_pcore_Hall p nilW).
  have [_ _ cWpWp' _] := dprodP (nilpotent_pcoreC p nilW).
  exists ('O_p(W) :&: M`_\sigma)%G; rewrite ?(centSS _ _ cWpWp') ?subsetIl //.
  by rewrite (sub_Hall_pcore (nilpotent_pcore_Hall _ _)) ?(pi_p'group qX).
split=> // [a_p | {part1}sylX].
  have ltCMX_G := sub_proper_trans (subsetIl M 'C(X)) ltMG.
  have [P sylP cPX] := part1; have s_p := alpha_sub_sigma maxM a_p.
  have{sylP} sylP := subHall_Sylow hallMs s_p sylP.
  apply: rank3_Uniqueness ltCMX_G (leq_trans a_p _).
  by rewrite -(rank_Sylow sylP) rankS //= subsetI (pHall_sub sylP) // centsC.
do [move: sWXM'; rewrite (joing_idPr (pHall_sub sylX)) => sWM'] in hallW.
have nMbX: X \subset 'N(M`_\beta) := subset_trans sXM (normal_norm nsMbM).
have nsMbXM : M`_\beta <*> X <| M.
  rewrite -{2}(quotientGK nsMbM) -quotientYK ?cosetpre_normal //=.
  rewrite (eq_Hall_pcore _ (quotient_pHall nMbX sylX)); last first.
    exact: nilpotent_pcore_Hall Mbeta_quo_nil.
  by rewrite gFnormal_trans ?quotient_normal ?gFnormal.
pose U := 'N_M(X); have defM: M`_\beta * U = M.
  have sXU : X \subset U by rewrite subsetI sXM normG.
  rewrite -[U](mulSGid sXU) /= -/U mulgA -norm_joinEr //.
  apply: Frattini_arg nsMbXM (pHall_subl (joing_subr _ X) _ sylX).
  by rewrite join_subG Mbeta_der1 (pHall_sub sylX).
have sWpU: 'O_p(W) \subset U.
  rewrite gFsub_trans // subsetI sWM normal_norm //=.
  have sylX_W: q.-Sylow(W) X := pHall_subl sXW sWM' sylX.
  by rewrite (eq_Hall_pcore (nilpotent_pcore_Hall q nilW) sylX_W) pcore_normal.
have sylWp: p.-Sylow(M^`(1)) 'O_p(W).
  exact: subHall_Sylow hallW (predU1l _ _) (nilpotent_pcore_Hall p nilW).
exists 'O_p(W)%G; rewrite //= -(setIidPl (pHall_sub sylWp)).
rewrite (pprod_focal_coprime defM) ?pcore_normal ?subsetIr //.
exact: pnat_coprime (pcore_pgroup _ _) (pi_pnat (pcore_pgroup _ _) _).
Qed.

(* This is B & G, Corollary 10.9(b). *)
Corollary nonuniq_norm_Sylow_pprod p H S :
    H \in 'M -> H :!=: M -> p.-Sylow(G) S -> 'N(S) \subset H :&: M -> 
  M`_\beta * (H :&: M) = M /\ \alpha(M) =i \beta(M).
Proof.
move=> maxH neqHM sylS_G sN_HM; have [sNH sNM] := subsetIP sN_HM.
have [sSM sSH] := (subset_trans (normG S) sNM, subset_trans (normG S) sNH).
have [sylS pS] := (pHall_subl sSM (subsetT M) sylS_G, pHall_pgroup sylS_G).
have sMp: p \in \sigma(M) by apply/exists_inP; exists S.
have aM'p: p \in \alpha(M)^'.
  apply: contra neqHM; rewrite !inE -(rank_Sylow sylS) => rS.
  have uniqS: S \in 'U := rank3_Uniqueness (mFT_pgroup_proper pS) rS.
  by rewrite (eq_uniq_mmax (def_uniq_mmax uniqS maxM sSM) maxH sSH).
have sSM': S \subset M^`(1).
  by rewrite (subset_trans _ sMsM') ?(sub_Hall_pcore hallMs) ?(pi_pgroup pS).
have nMbS := subset_trans sSM (normal_norm nsMbM).
have nMbSM: M`_\beta <*> S <| M.
  rewrite -{2}(quotientGK nsMbM) -quotientYK ?cosetpre_normal //=.
  have sylS_M' := pHall_subl sSM' sM'M sylS.
  rewrite (eq_Hall_pcore _ (quotient_pHall nMbS sylS_M')); last first.
    exact: nilpotent_pcore_Hall Mbeta_quo_nil.
  by rewrite gFnormal_trans ?quotient_normal ?gFnormal.
have defM: M`_\beta * 'N_M(S) = M.
  have sSNM: S \subset 'N_M(S) by rewrite subsetI sSM normG.
  rewrite -(mulSGid sSNM) /= mulgA -norm_joinEr //.
  by rewrite (Frattini_arg _ (pHall_subl _ _ sylS_G)) ?joing_subr ?subsetT.
split=> [|q].
  apply/eqP; rewrite setIC eqEsubset mulG_subG subsetIl pcore_sub /=.
  by rewrite -{1}defM mulgS ?setIS.
apply/idP/idP=> [aMq|]; last exact: beta_sub_alpha.
apply: contraR neqHM => bM'q; have bM'p := contra (@beta_sub_alpha _ M p) aM'p.
have [|_ uniqNM _] := beta'_cent_Sylow bM'q bM'p pS.
  by apply: contraR aM'p; rewrite sSM'; case: eqP => //= <- _.
rewrite (eq_uniq_mmax (def_uniq_mmax (uniqNM aMq) maxM (subsetIl _ _)) maxH) //.
by rewrite subIset ?(subset_trans (cent_sub _)) ?orbT.
Qed.

(* This is B & G, Proposition 10.10. *)
Proposition max_normed_2Elem_signaliser p q (A Q : {group gT}) :
    p != q -> A \in 'E_p^2(G) :&: 'E*_p(G) -> Q \in |/|*(A; q) ->
    q %| #|'C(A)| ->
  exists2 P : {group gT}, p.-Sylow(G) P /\ A \subset P
          & [/\ (*a*) 'O_p^'('C(P)) * ('N(P) :&: 'N(Q)) = 'N(P),
                (*b*) P \subset 'N(Q)^`(1)
              & (*c*) q.-narrow Q -> P \subset 'C(Q)].
Proof.
move=> neq_pq /setIP[Ep2A EpmA] maxQ piCAq.
have [_ abelA dimA] := pnElemP Ep2A; have [pA cAA _] := and3P abelA.
have [p_pr oA] := (pnElem_prime Ep2A, card_pnElem Ep2A).
have{dimA} rA2: 'r(A) = 2 by rewrite (rank_abelem abelA).
have{EpmA} ncA: normed_constrained A.
  have ntA: A :!=: 1 by rewrite -rank_gt0 rA2.
  exact: plength_1_normed_constrained ntA EpmA (mFT_proper_plength1 _).
pose pi := \pi(A); pose K := 'O_pi^'('C(A)).
have def_pi : pi =i (p : nat_pred).
  by move=> r; rewrite !inE /= oA primes_exp ?primes_prime ?inE.
have pi'q : q \notin pi by rewrite def_pi !inE eq_sym.
have transKA: [transitive K, on |/|*(A; q) | 'JG].
  by rewrite normed_constrained_rank2_trans // (center_idP cAA) rA2.
have [P0 sylP0 sAP0] := Sylow_superset (subsetT _) pA.
have pP0: p.-group P0 := pHall_pgroup sylP0.
have piP0: pi.-group P0 by rewrite (eq_pgroup _ def_pi).
have{pP0} snAP0: A <|<| P0 := nilpotent_subnormal (pgroup_nil pP0) sAP0.
have{pi'q snAP0 ncA piP0} [//|] := normed_trans_superset ncA pi'q snAP0 piP0.
rewrite /= -/pi -/K => -> transKP submaxPA maxPfactoring.
have{transKP} [Q0 maxQ0 _] := imsetP transKP.
have{transKA} [k Kk defQ] := atransP2 transKA (subsetP submaxPA _ maxQ0) maxQ.
set P := P0 :^ k; have{sylP0} sylP: p.-Sylow(G) P by rewrite pHallJ ?in_setT.
have nAK: K \subset 'N(A) by rewrite cents_norm ?pcore_sub.
have{sAP0 nAK K Kk} sAP: A \subset P by rewrite -(normsP nAK k Kk) conjSg.
exists [group of P] => //.
have{maxPfactoring} [sPNQ' defNP] := maxPfactoring _ maxQ0.
move/(congr1 ('Js%act^~ k)): defNP sPNQ'; rewrite -(conjSg _ _ k) /=.
rewrite conjsMg !conjIg !conjsRg -!derg1 -!normJ -pcoreJ -centJ -/P.
rewrite -(congr_group defQ) (eq_pcore _ (eq_negn def_pi)) => defNP sPNQ'.
have{sPNQ'} sPNQ': P \subset 'N(Q)^`(1).
  by rewrite (setIidPl (mFT_Sylow_der1 sylP)) in sPNQ'.
split=> // narrowQ; have [-> | ntQ] := eqsVneq Q 1; first exact: cents1.
pose AutQ := conj_aut Q @* 'N(Q).
have qQ: q.-group Q by case/mem_max_normed: maxQ.
have ltNG: 'N(Q) \proper G by rewrite mFT_norm_proper // (mFT_pgroup_proper qQ).
have{ltNG} qAutQ': q.-group AutQ^`(1).
  have qAutQq: q.-group 'O_q(AutQ) := pcore_pgroup _ _.
  rewrite (pgroupS _ qAutQq) // der1_min ?gFnorm //.
  have solAutQ: solvable AutQ by rewrite morphim_sol -?mFT_sol_proper.
  have [oddQ oddAutQ]: odd #|Q| /\ odd #|AutQ| by rewrite morphim_odd mFT_odd.
  by have /(Aut_narrow qQ)[] := Aut_conj_aut Q 'N(Q).
have nQP: P \subset 'N(Q) := subset_trans sPNQ' (der_sub 1 _).
rewrite (sameP setIidPl eqP) eqEsubset subsetIl /=.
rewrite -quotient_sub1 ?normsI ?normG ?norms_cent //= -ker_conj_aut subG1.
rewrite trivg_card1 (card_isog (first_isog_loc _ _)) //= -trivg_card1 -subG1.
have q'AutP: q^'.-group (conj_aut Q @* P).
  by rewrite morphim_pgroup //; apply: pi_pnat (pHall_pgroup sylP) _.
rewrite -(coprime_TIg (pnat_coprime qAutQ' q'AutP)) subsetI subxx.
by rewrite /= -morphim_der // morphimS.
Qed.

(* Notation for Proposition 11, which is the last to appear in this segment. *)
Local Notation sigma' := \sigma(gval M)^'.

(* This is B & G, Proposition 10.11(a). *)
Proposition sigma'_not_uniq K : K \subset M -> sigma'.-group K -> K \notin 'U.
Proof.
move=> sKM sg'K; have [E hallE sKE] := Hall_superset solM sKM sg'K.
have [sEM sg'E _] := and3P hallE.
have rEle2: 'r(E) <= 2.
  have [q _ ->] := rank_witness E; rewrite leqNgt; apply/negP=> rEgt2.
  have: q \in sigma' by rewrite (pnatPpi sg'E) // -p_rank_gt0 -(subnKC rEgt2).
  by rewrite inE /= alpha_sub_sigma //; apply: leq_trans (p_rankS q sEM).
have [E1 | ntE]:= eqsVneq E 1.
  by apply: contraL (@uniq_mmax_neq1 _ K) _; rewrite -subG1 -E1.
pose p := max_pdiv #|E|; pose P := 'O_p(E).
have piEp: p \in \pi(E) by rewrite pi_max_pdiv cardG_gt1.
have sg'p: p \in sigma' by rewrite (pnatPpi sg'E).
have sylP: p.-Sylow(E) P.
  rewrite rank2_max_pcore_Sylow ?mFT_odd ?(solvableS sEM solM) //.
  exact: leq_trans (rankS (Fitting_sub E)) rEle2.
apply: contra (sg'p) => uniqK; apply/existsP; exists [group of P].
have defMK := def_uniq_mmax uniqK maxM (subset_trans sKE sEM).
rewrite (subHall_Sylow hallE) // (sub_uniq_mmax defMK) //; last first.
  rewrite mFT_norm_proper ?(mFT_pgroup_proper (pcore_pgroup _ _)) //.
  by rewrite -cardG_gt1 (card_Hall sylP) p_part_gt1.
by rewrite (subset_trans sKE) // gFnorm.
Qed.

(* This is B & G, Proposition 10.11(b). *)
Proposition sub'cent_sigma_rank1 K :
  K \subset M -> sigma'.-group K -> 'r('C_K(M`_\sigma)) <= 1.
Proof.
move=> sKM sg'K; rewrite leqNgt; apply/rank_geP=> [[A /nElemP[p Ep2A]]].
have p_pr := pnElem_prime Ep2A.
have [sACKMs abelA dimA] := pnElemP Ep2A; rewrite subsetI centsC in sACKMs.
have{sACKMs} [sAK cAMs]: A \subset K /\ M`_\sigma \subset 'C(A) := andP sACKMs.
have sg'p: p \in sigma'.
  by rewrite (pgroupP (pgroupS sAK sg'K)) // (card_pnElem Ep2A) dvdn_mull.
have [Ms1 | [q q_pr q_dvd_Ms]] := trivgVpdiv M`_\sigma.
  by case/eqP: (Msigma_neq1 maxM).
have sg_q: q \in \sigma(M) := pgroupP (pcore_pgroup _ _) _ q_pr q_dvd_Ms.
have neq_pq: p != q by apply: contraNneq sg'p => ->.
have [Q sylQ] := Sylow_exists q M`_\sigma; have [sQMs qQ _] := and3P sylQ.
have cAQ: Q \subset 'C(A) := subset_trans sQMs cAMs.
have{q_dvd_Ms} q_dv_CA: q %| #|'C(A)|.
  rewrite (dvdn_trans _ (cardSg cAQ)) // -(part_pnat_id (pnat_id q_pr)).
  by rewrite (card_Hall sylQ) partn_dvd.
have{cAQ} maxQ: Q \in |/|*(A; q).
  rewrite inE; apply/maxgroupP; rewrite qQ cents_norm 1?centsC //.
  split=> // Y /andP[qY _] sQY; apply: sub_pHall qY sQY (subsetT Y).
  by rewrite (subHall_Sylow (Msigma_Hall_G maxM)).
have sNQM: 'N(Q) \subset M.
  by rewrite (norm_sigma_Sylow sg_q) // (subHall_Sylow hallMs).
have rCAle2: 'r('C(A)) <= 2.
  apply: contraR (sigma'_not_uniq sKM sg'K); rewrite -ltnNge => rCAgt2.
  apply: uniq_mmaxS sAK (sub_mmax_proper maxM sKM) _.
  by apply: cent_rank3_Uniqueness rCAgt2; rewrite (rank_abelem abelA) dimA.
have max2A: A \in 'E_p^2(G) :&: 'E*_p(G).
  rewrite 3!inE subsetT abelA dimA; apply/pmaxElemP; rewrite inE subsetT.
  split=> // Y /pElemP[_ abelY /eqVproper[]//ltAY].
  have [pY cYY _] := and3P abelY.
  suffices: 'r_p('C(A)) > 2 by rewrite ltnNge (leq_trans (p_rank_le_rank p _)).
  rewrite -dimA (leq_trans (properG_ltn_log pY ltAY)) //.
  by rewrite logn_le_p_rank // inE centsC (subset_trans (proper_sub ltAY)).
have{rCAle2 cAMs} Ma1: M`_\alpha = 1.
  apply: contraTeq rCAle2; rewrite -rank_gt0 -ltnNge.
  have [r _ ->] := rank_witness M`_\alpha; rewrite p_rank_gt0.
  move/(pnatPpi (pcore_pgroup _ _))=> a_r; apply: (leq_trans a_r).
  have [R sylR] := Sylow_exists r M`_\sigma.
  have sylR_M: r.-Sylow(M) R.
    by rewrite (subHall_Sylow (Msigma_Hall maxM)) ?alpha_sub_sigma.
  rewrite -(p_rank_Sylow sylR_M) (p_rank_Sylow sylR).
  by rewrite (leq_trans (p_rank_le_rank r _)) // rankS // centsC.
have{Ma1} nilM': nilpotent M^`(1).
  by rewrite (isog_nil (quotient1_isog _)) -Ma1 Malpha_quo_nil.
have{max2A maxQ neq_pq q_dv_CA} [P [sylP sAP] sPNQ']:
  exists2 P : {group gT}, p.-Sylow(G) P /\ A \subset P & P \subset 'N(Q)^`(1).
- by case/(max_normed_2Elem_signaliser neq_pq): maxQ => // P ? []; exists P.
have{sNQM} defP: 'O_p(M^`(1)) = P.
  rewrite (nilpotent_Hall_pcore nilM' (pHall_subl _ _ sylP)) ?subsetT //.
  by rewrite (subset_trans sPNQ') ?dergS.
have nsPM: P <| M by rewrite -defP !gFnormal_trans.
have sPM := normal_sub nsPM.
case/exists_inP: sg'p; exists P; first exact: pHall_subl (subsetT M) sylP.
by rewrite (mmax_normal maxM) // -rank_gt0 ltnW // -dimA -rank_abelem ?rankS.
Qed.

(* This is B & G, Proposition 10.11(c). *)
Proposition sub'cent_sigma_cyclic K (Y := 'C_K(M`_\sigma) :&: M^`(1)) :
  K \subset M -> sigma'.-group K -> cyclic Y /\ Y <| M.
Proof.
move=> sKM sg'K; pose Z := 'O_sigma'('F(M)).
have nsZM: Z <| M by rewrite !gFnormal_trans.
have [sZM nZM] := andP nsZM; have Fnil := Fitting_nil M.
have rZle1: 'r(Z) <= 1.
  apply: leq_trans (rankS _) (sub'cent_sigma_rank1 sZM (pcore_pgroup _ _)).
  rewrite subsetI subxx (sameP commG1P trivgP) /=.
  rewrite -(TI_pcoreC \sigma(M) M 'F(M)) subsetI commg_subl commg_subr.
  by rewrite (subset_trans sZM) ?gFnorm ?gFsub_trans.
have{rZle1} cycZ: cyclic Z.
  have nilZ: nilpotent Z := nilpotentS (gFsub _ _) Fnil.
  by rewrite nil_Zgroup_cyclic // odd_rank1_Zgroup // mFT_odd.
have cZM': M^`(1) \subset 'C_M(Z).
  rewrite der1_min ?normsI ?normG ?norms_cent //= -ker_conj_aut.
  rewrite (isog_abelian (first_isog_loc _ _)) //.
  by rewrite (abelianS (Aut_conj_aut _ _)) // Aut_cyclic_abelian.
have sYF: Y \subset 'F(M).
  apply: subset_trans (cent_sub_Fitting (mmax_sol maxM)).
  have [_ /= <- _ _] := dprodP (nilpotent_pcoreC \sigma(M) Fnil).
  by rewrite centM setICA setISS // setIC subIset ?centS // pcore_Fitting.
have{sYF} sYZ: Y \subset Z.
  rewrite (sub_Hall_pcore (nilpotent_pcore_Hall _ Fnil)) //=.
  by rewrite -setIA (pgroupS (subsetIl K _)).
by rewrite (cyclicS sYZ cycZ) (char_normal_trans _ nsZM) // sub_cyclic_char.
Qed.

(* This is B & G, Proposition 10.11(d). *)
Proposition commG_sigma'_1Elem_cyclic p K P (K0 := [~: K, P]) :
    K \subset M -> sigma'.-group K -> p \in sigma' -> P \in 'E_p^1('N_M(K)) ->
    'C_(M`_\sigma)(P) = 1 -> p^'.-group K -> abelian K ->
  [/\ K0 \subset 'C(M`_\sigma), cyclic K0 & K0 <| M].
Proof.
move=> sKM sg'K sg'p EpP regP p'K cKK.
have nK0P: P \subset 'N(K0) := commg_normr P K.
have p_pr := pnElem_prime EpP; have [sPMN _ oP] := pnElemPcard EpP.
have [sPM nKP]: P \subset M /\ P \subset 'N(K) by apply/subsetIP.
have /andP[sMsM nMsM]: M`_\sigma <| M := pcore_normal _ _.
have sK0K: K0 \subset K by rewrite commg_subl.
have [sK0M sg'K0]:= (subset_trans sK0K sKM, pgroupS sK0K sg'K).
have [nMsK0 nMsP] := (subset_trans sK0M nMsM, subset_trans sPM nMsM).
have coKP: coprime #|K| #|P| by rewrite oP coprime_sym prime_coprime -?p'natE.
have coK0Ms: coprime #|K0| #|M`_\sigma|.
  by rewrite coprime_sym (pnat_coprime (pcore_pgroup _ _)).
have nilK0Ms: nilpotent (K0 <*> M`_\sigma).
  have mulK0MsP: K0 <*> M`_\sigma ><| P = K0 <*> M`_\sigma <*> P.
    rewrite sdprodEY ?normsY // coprime_TIg //= norm_joinEl //.
    rewrite coprime_cardMg // coprime_mull (coprimeSg sK0K) //.
    by rewrite oP (pnat_coprime (pcore_pgroup _ _)) ?pnatE.
  apply: (prime_Frobenius_sol_kernel_nil mulK0MsP); rewrite ?oP //=.
    by rewrite (solvableS _ solM) // !join_subG sK0M pcore_sub.
  rewrite norm_joinEl // -subcent_TImulg ?subsetI ?nK0P //.
    by rewrite coprime_abel_cent_TI ?mul1g.
  exact: coprime_TIg.
have cMsK0: K0 \subset 'C(M`_\sigma).
  rewrite (sub_nilpotent_cent2 nilK0Ms) ?joing_subl ?joing_subr //.
  exact: pnat_coprime (pcore_pgroup _ _) sg'K0.
have [cycY nsYM] := sub'cent_sigma_cyclic sK0M sg'K0.
set Y := _ :&: _ in cycY nsYM.
have sK0Y: K0 \subset Y by rewrite !subsetI subxx cMsK0 commgSS.
split=> //; first exact: cyclicS sK0Y cycY.
by apply: char_normal_trans nsYM; rewrite sub_cyclic_char.
Qed.

End AnotherMaximal.

(* This is B & G, Lemma 10.12. *)
Lemma sigma_disjoint M H :
    M \in 'M -> H \in 'M -> gval H \notin M :^: G ->
  [/\ (*a*) M`_\alpha :&: H`_\sigma = 1,
            [predI \alpha(M) & \sigma(H)] =i pred0
    & (*b*) nilpotent M`_\sigma ->
            M`_\sigma :&: H`_\sigma = 1
         /\ [predI \sigma(M) & \sigma(H)] =i pred0].
Proof.
move=> maxM maxH notjMH.
suffices sigmaMHnil p: p \in [predI \sigma(M) & \sigma(H)] ->
  p \notin \alpha(M) /\ ~~ nilpotent M`_\sigma.
- have a2: [predI \alpha(M) & \sigma(H)] =i pred0.
    move=> p; apply/andP=> [[/= aMp sHp]].
    by case: (sigmaMHnil p); rewrite /= ?aMp // inE /= alpha_sub_sigma.
  split=> // [|nilMs].
    rewrite coprime_TIg // (pnat_coprime (pcore_pgroup _ _)) //.
    apply: sub_in_pnat (pcore_pgroup _ _) => p _ sHp.
    by apply: contraFN (a2 p) => aMp; rewrite inE /= sHp andbT.
  have b2: [predI \sigma(M) & \sigma(H)] =i pred0.
    by move=> p; apply/negP; case/sigmaMHnil => _; rewrite nilMs.
  rewrite coprime_TIg // (pnat_coprime (pcore_pgroup _ _)) //.
  apply: sub_in_pnat (pcore_pgroup _ _) => p _ sHp.
  by apply: contraFN (b2 p) => bMp; rewrite inE /= sHp andbT.
case/andP=> sMp sHp; have [S sylS]:= Sylow_exists p M.
have [sSM pS _] := and3P sylS.
have sylS_G: p.-Sylow(G) S := sigma_Sylow_G maxM sMp sylS.
have [g sSHg]: exists g, S \subset H :^ g.
  have [Sg' sylSg']:= Sylow_exists p H.
  have [g _ ->] := Sylow_trans (sigma_Sylow_G maxH sHp sylSg') sylS_G.
  by exists g; rewrite conjSg (pHall_sub sylSg').
have{notjMH} neqHgM: H :^ g != M.
  by apply: contraNneq notjMH => <-; rewrite orbit_sym mem_orbit ?in_setT.
do [split; apply: contra neqHgM] => [|nilMs].
  rewrite !inE -(p_rank_Sylow sylS) -rank_pgroup //= => rS_gt3.
  have uniqS: S \in 'U := rank3_Uniqueness (mFT_pgroup_proper pS) rS_gt3.
  have defUS: 'M(S) = [set M] := def_uniq_mmax uniqS maxM sSM.
  by rewrite (eq_uniq_mmax defUS _ sSHg) ?mmaxJ.
have nsSM: S <| M.
  have nsMsM: M`_\sigma <| M by apply: pcore_normal.
  have{sylS} sylS: p.-Sylow(M`_\sigma) S.
    apply: pHall_subl (pcore_sub _ _) sylS => //.
    by rewrite (sub_Hall_pcore (Msigma_Hall maxM)) ?(pi_pgroup pS).
  by rewrite (nilpotent_Hall_pcore nilMs sylS) gFnormal_trans.
have sNS_Hg: 'N(S) \subset H :^ g.
  rewrite -sub_conjgV -normJ (norm_sigma_Sylow sHp) //.
  by rewrite (pHall_subl _ (subsetT _)) ?sub_conjgV // pHallJ ?in_setT.
have ltHg: H :^ g \proper G by rewrite mmax_proper ?mmaxJ //.
rewrite (mmax_max maxM ltHg) // -(mmax_normal maxM nsSM) //.
by apply: contraTneq sNS_Hg => ->; rewrite norm1 proper_subn.
Qed.

(* This is B & G, Lemma 10.13. *)
Lemma basic_p2maxElem_structure p A P :
    A \in 'E_p^2(G) :&: 'E*_p(G) -> p.-group P -> A \subset P -> ~~ abelian P ->
  let Z0 := ('Ohm_1('Z(P)))%G in
  [/\ (*a*) Z0 \in 'E_p^1(A),
      (*b*) exists Y : {group gT},
            [/\ cyclic Y, Z0 \subset Y
              & forall A0, A0 \in 'E_p^1(A) :\ Z0 -> A0 \x Y = 'C_P(A)]
    & (*c*) [transitive 'N_P(A), on 'E_p^1(A) :\ Z0| 'JG]].
Proof.
case/setIP=> Ep2A maxA pP sAP not_cPP Z0; set E1A := 'E_p^1(A).
have p_pr: prime p := pnElem_prime Ep2A; have [_ abelA dimA] := pnElemP Ep2A.
have [oA [pA cAA _]] := (card_pnElem Ep2A, and3P abelA).
have [p_gt0 p_gt1] := (prime_gt0 p_pr, prime_gt1 p_pr).
have{maxA} maxA S:
  p.-group S -> A \subset S -> A \in 'E*_p(S) /\ 'Ohm_1('C_S(A)) = A.
- move=> pS sAS; suff maxAS: A \in 'E*_p(S) by rewrite (Ohm1_cent_max maxAS).
  by rewrite (subsetP (pmaxElemS p (subsetT S))) // inE maxA inE.
have [S sylS sPS] := Sylow_superset (subsetT P) pP.
pose Z1 := 'Ohm_1('Z(S))%G; have sZ1Z: Z1 \subset 'Z(S) := Ohm_sub 1 _.
have [pS sAS] := (pHall_pgroup sylS, subset_trans sAP sPS).
have [maxAS defC1] := maxA S pS sAS; set C := 'C_S(A) in defC1.
have sZ0A: Z0 \subset A by rewrite -defC1 OhmS // setISS // centS.
have sZ1A: Z1 \subset A by rewrite -defC1 OhmS // setIS // centS.
have [pZ0 pZ1]: p.-group Z0 /\ p.-group Z1 by split; apply: pgroupS pA.
have sZ10: Z1 \subset Z0.
  rewrite -[gval Z1]Ohm_id OhmS // subsetI (subset_trans sZ1A) //=.
  by rewrite (subset_trans sZ1Z) // subIset // centS ?orbT.
have ntZ1: Z1 :!=: 1.
  have: A :!=: 1 by rewrite -cardG_gt1 oA (ltn_exp2l 0).
  apply: contraNneq; rewrite -subG1 -(setIidPr sZ1Z) => /TI_Ohm1.
  by rewrite setIid => /(trivg_center_pgroup pS) <-.
have EpZ01: abelian C -> Z1 = Z0 /\ Z0 \in E1A.
  move=> cCC; have [eqZ0A | ltZ0A] := eqVproper sZ0A.
    rewrite (abelianS _ cCC) // in not_cPP.
    by rewrite subsetI sPS centsC -eqZ0A gFsub_trans ?subsetIr.
  have leZ0p: #|Z0| <= p ^ 1.
    by rewrite (card_pgroup pZ0) leq_exp2l // -ltnS -dimA properG_ltn_log.
  have [_ _ [e oZ1]] := pgroup_pdiv pZ1 ntZ1.
  have{e oZ1}: #|Z1| >= p by rewrite oZ1 (leq_exp2l 1).
  rewrite (geq_leqif (leqif_trans (subset_leqif_card sZ10) (leqif_eq leZ0p))).
  rewrite [E1A]p1ElemE // !inE sZ0A; case/andP=> sZ01 ->.
  by split=> //; apply/eqP; rewrite -val_eqE eqEsubset sZ10.
have [A1 neqA1Z EpA1]: exists2 A1, A1 != Z1 & #|Z1| = p -> A1 \in E1A.
  have [oZ1 |] := #|Z1| =P p; last by exists 1%G; rewrite // eq_sym.
  have [A1 defA]:= abelem_split_dprod abelA sZ1A.
  have{defA} [_ defA _ tiA1Z1] := dprodP defA.
  have EpZ1: Z1 \in E1A by rewrite [E1A]p1ElemE // !inE sZ1A /= oZ1.
  suffices: A1 \in E1A by exists A1; rewrite // eq_sym; apply/(TIp1ElemP EpZ1).
  rewrite [E1A]p1ElemE // !inE -defA mulG_subr /=.
  by rewrite -(mulKn #|A1| p_gt0) -{1}oZ1 -TI_cardMg // defA oA mulKn.
pose cplA1C Y := [/\ cyclic Y, Z0 \subset Y, A1 \x Y = C & abelian C].
have [Y [{cplA1C} cycY sZ0Y defC cCC]]: exists Y, cplA1C Y.
  have [rSgt2 | rSle2] := ltnP 2 'r(S).
    rewrite (rank_pgroup pS) in rSgt2; have oddS := mFT_odd S.
    have max2AS: A \in 'E_p^2(S) :&: 'E*_p(S) by rewrite 3!inE sAS abelA dimA.
    have oZ1: #|Z1| = p by case/Ohm1_ucn_p2maxElem: max2AS => // _ [].
    have{EpA1} EpA1 := EpA1 oZ1; have [sA1A abelA1 oA1] := pnElemPcard EpA1.
    have EpZ1: Z1 \in E1A by rewrite [E1A]p1ElemE // !inE sZ1A /= oZ1.
    have [_ defA cA1Z tiA1Z] := dprodP (p2Elem_dprodP Ep2A EpA1 EpZ1 neqA1Z).
    have defC: 'C_S(A1) = C.
      rewrite /C -defA centM setICA setIC ['C_S(Z1)](setIidPl _) // centsC.
      by rewrite (subset_trans sZ1Z) ?subsetIr.
    have rCSA1: 'r_p('C_S(A1)) <= 2.
      by rewrite defC -p_rank_Ohm1 defC1 (p_rank_abelem abelA) dimA.
    have sA1S := subset_trans sA1A sAS.
    have nnS: p.-narrow S by apply/implyP=> _; apply/set0Pn; exists A.
    have [] := narrow_cent_dprod pS oddS rSgt2 nnS oA1 sA1S rCSA1.
    set Y := _ :&: _; rewrite {}defC => cycY _ _ defC; exists [group of Y].
    have cCC: abelian C; last split=> //.
      apply/center_idP; rewrite -(center_dprod defC).
      rewrite (center_idP (abelem_abelian abelA1)).
      by rewrite (center_idP (cyclic_abelian cycY)).
    have{EpZ01} [<- _] := EpZ01 cCC; rewrite subsetI (subset_trans sZ1Z) //.
    by rewrite setIS ?centS ?gFsub_trans.
  have not_cSS := contra (abelianS sPS) not_cPP.
  have:= mFT_rank2_Sylow_cprod sylS rSle2 not_cSS.
  case=> E [_ dimE3 eE] [Y cycY [defS defY1]].
  have [[_ mulEY cEY] cYY] := (cprodP defS, cyclic_abelian cycY).
  have defY: 'Z(S) = Y.
    case/cprodP: (center_cprod defS) => _ <- _.
    by rewrite (center_idP cYY) -defY1 mulSGid ?Ohm_sub.
  have pY: p.-group Y by rewrite -defY (pgroupS (center_sub S)).
  have sES: E \subset S by rewrite -mulEY mulG_subl.
  have pE := pgroupS sES pS.
  have defS1: 'Ohm_1(S) = E.
    apply/eqP; rewrite (OhmE 1 pS) eqEsubset gen_subG andbC.
    rewrite sub_gen; last by rewrite subsetI sES sub_LdivT.
    apply/subsetP=> ey /LdivP[]; rewrite -mulEY.
    case/imset2P=> e y Ee Yy -> eyp; rewrite groupM //.
    rewrite (subsetP (center_sub E)) // -defY1 (OhmE 1 pY) mem_gen //.
    rewrite expgMn in eyp; last by red; rewrite -(centsP cEY).
    by rewrite (exponentP eE) // mul1g in eyp; rewrite !inE Yy eyp eqxx.
  have sAE: A \subset E by rewrite -defS1 -(Ohm1_id abelA) OhmS.
  have defC: A * Y = C.
    rewrite /C -mulEY setIC -group_modr; last first.
      by rewrite -defY subIset // orbC centS.
    congr (_ * _); apply/eqP; rewrite /= setIC eqEcard subsetI sAE.
    have pCEA: p.-group 'C_E(A) := pgroupS (subsetIl E _) pE.
    rewrite -abelianE cAA (card_pgroup pCEA) oA leq_exp2l //= leqNgt.
    apply: contraL cycY => dimCEA3.
    have sAZE: A \subset 'Z(E).
      rewrite subsetI sAE // centsC (sameP setIidPl eqP) eqEcard subsetIl /=.
      by rewrite (card_pgroup pE) (card_pgroup pCEA) dimE3 leq_exp2l.
    rewrite abelian_rank1_cyclic // -ltnNge (rank_pgroup pY).
    by rewrite (p_rank_abelian p cYY) defY1 -dimA lognSg.
  have cAY: Y \subset 'C(A) by apply: centSS cEY.
  have cCC: abelian C by rewrite -defC abelianM cAA cYY.
  have{EpZ01} [eqZ10 EpZ1] := EpZ01 cCC; rewrite -eqZ10 in EpZ1.
  have sZ0Y: Z0 \subset Y by rewrite -eqZ10 -defY Ohm_sub.
  have{EpA1} EpA1 := EpA1 (card_pnElem EpZ1).
  have [sA1A _ oA1] := pnElemPcard EpA1.
  have [_ defA _ tiA1Z] := dprodP (p2Elem_dprodP Ep2A EpA1 EpZ1 neqA1Z).
  exists Y; split; rewrite // dprodE ?(centSS _ sA1A cAY) ?prime_TIg ?oA1 //.
    by rewrite -(mulSGid sZ0Y) -eqZ10 mulgA defA.
  apply: contraL cycY => sA1Y; rewrite abelian_rank1_cyclic // -ltnNge.
  by rewrite -dimA -rank_abelem ?rankS // -defA eqZ10 mul_subG.
have{EpZ01} [eqZ10 EpZ0] := EpZ01 cCC; have oZ0 := card_pnElem EpZ0.
have{EpA1} EpA1: A1 \in E1A by rewrite EpA1 ?eqZ10.
have [sA1A _ oA1] := pnElemPcard EpA1; rewrite {}eqZ10 in neqA1Z.
have [_ defA _ tiA1Z] := dprodP (p2Elem_dprodP Ep2A EpA1 EpZ0 neqA1Z).
split=> //; first exists (P :&: Y)%G.
  have sPY_Y := subsetIr P Y; rewrite (cyclicS sPY_Y) //.
  rewrite subsetI (subset_trans sZ0A) //= sZ0Y.
  split=> // A0 /setD1P[neqA0Z EpA0]; have [sA0A _ _] := pnElemP EpA0.
  have [_ mulA0Z _ tiA0Z] := dprodP (p2Elem_dprodP Ep2A EpA0 EpZ0 neqA0Z).
  have{defC} [_ defC cA1Y tiA1Y] := dprodP defC.
  rewrite setIC -{2}(setIidPr sPS) setIAC.
  apply: dprod_modl (subset_trans sA0A sAP); rewrite -defC dprodE /=.
  - by rewrite -(mulSGid sZ0Y) !mulgA mulA0Z defA.
  - rewrite (centSS (subxx Y) sA0A) // -defA centM subsetI cA1Y /=.
    by rewrite sub_abelian_cent ?cyclic_abelian.
  rewrite setIC -(setIidPr sA0A) setIA -defA -group_modr //.
  by rewrite (setIC Y) tiA1Y mul1g setIC.
apply/imsetP; exists A1; first by rewrite 2!inE neqA1Z.
apply/eqP; rewrite eq_sym eqEcard; apply/andP; split.
  apply/subsetP=> _ /imsetP[x /setIP[Px nAx] ->].
  rewrite 2!inE /E1A -(normP nAx) pnElemJ EpA1 andbT -val_eqE /=.
  have nZ0P: P \subset 'N(Z0) by rewrite !gFnorm_trans.
  by rewrite -(normsP nZ0P x Px) (inj_eq (@conjsg_inj _ x)).
have pN: p.-group 'N_P(_) := pgroupS (subsetIl P _) pP.
have defCPA: 'N_('N_P(A))(A1) = 'C_P(A).
  apply/eqP; rewrite eqEsubset andbC subsetI setIS ?cent_sub //.
  rewrite subIset /=; last by rewrite orbC cents_norm ?centS.
  rewrite setIAC (subset_trans (subsetIl _ _)) //= subsetI subsetIl /=.
  rewrite -defA centM subsetI andbC subIset /=; last first.
    by rewrite centsC gFsub_trans ?subsetIr.
  have nC_NP: 'N_P(A1) \subset 'N('C(A1)) by rewrite norms_cent ?subsetIr.
  rewrite -quotient_sub1 // subG1 trivg_card1.
  rewrite (pnat_1 (quotient_pgroup _ (pN _))) //.
  rewrite -(card_isog (second_isog nC_NP)) /= (setIC 'C(A1)).
  by apply: p'group_quotient_cent_prime; rewrite ?subsetIr ?oA1.
have sCN: 'C_P(A) \subset 'N_P(A) by rewrite setIS ?cent_sub.
have nA_NCPA: 'N_P('C_P(A)) \subset 'N_P(A).
  have [_ defCPA1] := maxA P pP sAP.
  by rewrite -[in 'N(A)]defCPA1 setIS // gFnorm_trans.
rewrite card_orbit astab1JG /= {}defCPA.
rewrite -(leq_add2l (Z0 \in E1A)) -cardsD1 EpZ0 (card_p1Elem_p2Elem Ep2A) ltnS.
rewrite dvdn_leq ?(pfactor_dvdn 1) ?indexg_gt0 // -divgS // logn_div ?cardSg //.
rewrite subn_gt0  properG_ltn_log ?pN //= (proper_sub_trans _ nA_NCPA) //.
rewrite (nilpotent_proper_norm (pgroup_nil pP)) // properEneq subsetIl andbT.
by apply: contraNneq not_cPP => <-; rewrite (abelianS (setSI _ sPS)).
Qed.

(* This is B & G, Proposition 10.14(a). *)
Proposition beta_not_narrow p : p \in \beta(G) ->
      [disjoint 'E_p^2(G) & 'E*_p(G)]
  /\ (forall P, p.-Sylow(G) P -> [disjoint 'E_p^2(P) & 'E*_p(P)]).
Proof.
move/forall_inP=> nnG.
have nnSyl P: p.-Sylow(G) P -> [disjoint 'E_p^2(P) & 'E*_p(P)].
  by move/nnG; rewrite negb_imply negbK setI_eq0 => /andP[].
split=> //; apply/pred0Pn=> [[E /andP[/= Ep2E EpmE]]].
have [_ abelE dimE]:= pnElemP Ep2E; have pE := abelem_pgroup abelE.
have [P sylP sEP] := Sylow_superset (subsetT E) pE.
case/pred0Pn: (nnSyl P sylP); exists E; rewrite /= 2!inE sEP abelE dimE /=.
by rewrite (subsetP (pmaxElemS p (subsetT P))) // inE EpmE inE.
Qed.

(* This is B & G, Proposition 10.14(b). *)
Proposition beta_noncyclic_uniq p R :
  p \in \beta(G) -> p.-group R -> 'r(R) > 1 -> R \in 'U.
Proof.
move=> b_p pR rRgt1; have [P sylP sRP] := Sylow_superset (subsetT R) pR.
rewrite (rank_pgroup pR) in rRgt1; have [A Ep2A] := p_rank_geP rRgt1.
have [sAR abelA dimA] := pnElemP Ep2A; have p_pr := pnElem_prime Ep2A.
case: (pickP [pred F in 'E_p(P) | A \proper F]) => [F | maxA]; last first.
  have [_ nnSyl] := beta_not_narrow b_p; case/pred0Pn: (nnSyl P sylP).
  exists A; rewrite /= (subsetP (pnElemS p 2 sRP)) //.
  apply/pmaxElemP; split=> [|F EpF]; first by rewrite inE (subset_trans sAR).
  by case/eqVproper=> [// | ltAF]; case/andP: (maxA F).
case/andP=> /pElemP[_ abelF] ltAF; have [pF cFF _] := and3P abelF.
apply: uniq_mmaxS sAR (mFT_pgroup_proper pR) _.
have rCAgt2: 'r('C(A)) > 2.
  rewrite -dimA (leq_trans (properG_ltn_log pF ltAF)) // -(rank_abelem abelF).
  by rewrite rankS // centsC (subset_trans (proper_sub ltAF)).
by apply: cent_rank3_Uniqueness rCAgt2; rewrite (rank_abelem abelA) dimA.
Qed.

(* This is B & G, Proposition 10.14(c). *)
Proposition beta_subnorm_uniq p P X :
  p \in \beta(G) -> p.-Sylow(G) P -> X \subset P -> 'N_P(X)%G \in 'U.
Proof.
move=> b_p sylP sXP; set Q := 'N_P(X)%G.
have pP := pHall_pgroup sylP; have pQ: p.-group Q := pgroupS (subsetIl _ _) pP.
have [| rQle1] := ltnP 1 'r(Q); first exact: beta_noncyclic_uniq pQ.
have cycQ: cyclic Q.
  by rewrite (odd_pgroup_rank1_cyclic pQ) ?mFT_odd -?rank_pgroup.
have defQ: P :=: Q.
  apply: (nilpotent_sub_norm (pgroup_nil pP) (subsetIl _ _)).
  by rewrite setIS // char_norms // sub_cyclic_char // subsetI sXP normG.
have:= forall_inP b_p P; rewrite inE negb_imply ltnNge; move/(_ sylP).
by rewrite defQ -(rank_pgroup pQ) (leq_trans rQle1).
Qed.

(* This is B & G, Proposition 10.14(d). *)
Proposition beta_norm_sub_mmax M Y :
  M \in 'M -> \beta(M).-subgroup(M) Y -> Y :!=: 1 -> 'N(Y) \subset M.
Proof.
move=> maxM /andP[sYM bY] ntY.
have [F1 | [q q_pr q_dv_FY]] := trivgVpdiv 'F(Y).
  by rewrite -(trivg_Fitting (solvableS sYM (mmax_sol maxM))) F1 eqxx in ntY.
pose X := 'O_q(Y); have qX: q.-group X := pcore_pgroup q _.
have ntX: X != 1.
  apply: contraTneq q_dv_FY => X1; rewrite -p'natE // -partn_eq1 //.
  rewrite -(card_Hall (nilpotent_pcore_Hall q (Fitting_nil Y))).
  by rewrite /= p_core_Fitting -/X X1 cards1.
have bMq: q \in \beta(M) by apply: (pgroupP (pgroupS (Fitting_sub Y) bY)).
have b_q: q \in \beta(G) by move: bMq; rewrite -predI_sigma_beta //; case/andP.
have sXM: X \subset M := gFsub_trans _ sYM.
have [P sylP sXP] := Sylow_superset sXM qX; have [sPM qP _] := and3P sylP.
have sylPG: q.-Sylow(G) P by rewrite (sigma_Sylow_G maxM) ?beta_sub_sigma.
have uniqNX: 'M('N_P(X)) = [set M].
  apply: def_uniq_mmax => //; last by rewrite subIset ?sPM.
  exact: (beta_subnorm_uniq b_q).
rewrite (subset_trans (char_norms (pcore_char q Y))) //.
rewrite (sub_uniq_mmax uniqNX) ?subsetIr // mFT_norm_proper //.
by rewrite (sub_mmax_proper maxM).
Qed.

End Ten.