path: root/mathcomp/odd_order/BGsection7.v

(* (c) Copyright 2006-2015 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 fintype bigop.
From mathcomp
Require Import finset prime fingroup morphism automorphism action quotient.
From mathcomp
Require Import gfunctor cyclic pgroup center commutator gseries nilpotent.
From mathcomp
Require Import sylow abelian maximal hall.
From mathcomp
Require Import BGsection1 BGsection6.

(******************************************************************************)
(*   This file covers B & G, section 7, i.e., the proof of the Thompson       *)
(* Transitivity Theorem, as well as some generalisations used later in the    *)
(* proof.                                                                     *)
(*   This is the first section of the proof that applies to a (hypothetical)  *)
(* minimally simple odd group, so we also introduce at this point some        *)
(* infrastructure to carry over this assumption into the rest of the proof.   *)
(*   minSimpleOddGroupType == a finGroupType that ranges exactly over the     *)
(*                            elements of a minimal counter-example to the    *)
(*                            Odd Order Theorem.                              *)
(*                       G == the group of all the elements in a              *)
(*                            minSimpleOddGroupType (this is a local notation *)
(*                            that must be reestablished for each such Type). *)
(*                      'M == the set of all (proper) maximal subgroups of G  *)
(*                   'M(H) == the set of all elements of 'M that contain H    *)
(*                      'U == the set of all H such that 'M(H) contains a     *)
(*                            single (unique) maximal subgroup of G.          *)
(*               'SCN_n[p] == the set of all SCN subgroups of rank at least n *)
(*                            of all the Sylow p-subgroups of G.              *)
(*            |/|_H(A, pi) == the set of all pi-subgroups of H that are       *)
(*                            normalised by A.                                *)
(*             |/|*(A, pi) == the set of pi-subgroups of G, normalised by A,  *)
(*                            and maximal subject to this condition.          *)
(*    normed_constrained A == A is a nontrivial proper subgroup of G, such    *)
(*                            that for any proper subgroup X containing A,    *)
(*                            all Y in |/|_X(A, pi') lie in the pi'-core of X *)
(*                            (here pi is the set of prime divisors of #|A|). *)
(*                            This is Hypothesis 7.1 in B & G.                *)
(******************************************************************************)

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

Import GroupScope.

Reserved Notation "''M'" (at level 8, format "''M'").
Reserved Notation "''M' ( H )" (at level 8, format "''M' ( H )").
Reserved Notation "''U'" (at level 8).
Reserved Notation "''SCN_' n [ p ]"
  (at level 8, n at level 2, format "''SCN_' n [ p ]").
Reserved Notation "|/|_ X ( A ; pi )"
  (at level 8, X at level 2, format "|/|_ X ( A ;  pi )").
Reserved Notation "|/|* ( A ; pi )"
  (at level 8, format "|/|* ( A ;  pi )").

(* The generic setup for the whole Odd Order Theorem proof. *)
Section InitialReduction.

Implicit Type gT : finGroupType.

Record minSimpleOddGroupMixin gT : Prop := MinSimpleOddGroupMixin {
  _ : odd #|[set: gT]|;
  _ : simple [set: gT];
  _ : ~~ solvable [set: gT];
  _ : forall M : {group gT}, M \proper [set: gT] -> solvable M
}.

Structure minSimpleOddGroupType := MinSimpleOddGroupType {
  minSimpleOddGroupType_base :> finGroupType;
  _ : minSimpleOddGroupMixin minSimpleOddGroupType_base
}.

Hypothesis IH_FT : minSimpleOddGroupType -> False.

Lemma minSimpleOdd_ind gT (G : {group gT}) : odd #|G| -> solvable G.
Proof.
move: {2}_.+1 (ltnSn #|G|) => n.
elim: n => // n IHn in gT G *; rewrite ltnS => leGn oddG.
have oG: #|[subg G]| = #|G| by rewrite (card_isog (isog_subg G)).
apply/idPn=> nsolG; case: IH_FT; exists [finGroupType of subg_of G].
do [split; rewrite ?oG //=] => [||M].
- rewrite -(isog_simple (isog_subg _)); apply/simpleP; split=> [|H nsHG].
    by apply: contra nsolG; move/eqP->; rewrite abelian_sol ?abelian1.
  have [sHG _]:= andP nsHG; apply/pred2P; apply: contraR nsolG; case/norP=> ntH.
  rewrite eqEcard sHG -ltnNge (series_sol nsHG) => ltHG.
  by rewrite !IHn ?(oddSg sHG) ?quotient_odd ?(leq_trans _ leGn) ?ltn_quotient.
- by apply: contra nsolG => solG; rewrite -(im_sgval G) morphim_sol.
rewrite properEcard oG; case/andP=> sMG ltMG.
by apply: IHn (leq_trans ltMG leGn) (oddSg sMG _); rewrite oG.
Qed.

Lemma minSimpleOdd_prime gT (G : {group gT}) :
  odd #|G| -> simple G -> prime #|G|.
Proof. by move/minSimpleOdd_ind; apply: simple_sol_prime. Qed.

End InitialReduction.

Notation TheMinSimpleOddGroup gT :=
    [set: FinGroup.arg_sort (FinGroup.base (minSimpleOddGroupType_base gT))]
  (only parsing).

(* Elementary properties of the minimal counter example. *)
Section MinSimpleOdd.

Variable gT : minSimpleOddGroupType.
Notation G := (TheMinSimpleOddGroup gT).
Implicit Types H K D M P U V X : {group gT}.
Local Notation sT := {set gT}.
Implicit Type p : nat.

Lemma mFT_odd H : odd #|H|.
Proof. by apply: (oddSg (subsetT H)); case: gT => ? []. Qed.

Lemma mFT_simple : simple G.
Proof. by case: gT => ? []. Qed.

Lemma mFT_nonSolvable : ~~ solvable G.
Proof. by case: gT => ? []. Qed.

Lemma mFT_sol M : M \proper G -> solvable M.
Proof. by case: gT M => ? []. Qed.

Lemma mFT_nonAbelian : ~~ abelian G.
Proof. by apply: contra mFT_nonSolvable; apply: abelian_sol. Qed.

Lemma mFT_neq1 : G != 1.
Proof. by apply: contraNneq mFT_nonAbelian => ->; apply: abelian1. Qed.

Lemma mFT_gt1 : [1] \proper G. Proof. by rewrite proper1G mFT_neq1. Qed.

Lemma mFT_quo_odd M H : odd #|M / H|.
Proof. by rewrite quotient_odd ?mFT_odd. Qed.

Lemma mFT_sol_proper M : (M \proper G) = solvable M.
Proof.
apply/idP/idP; first exact: mFT_sol.
by rewrite properT; apply: contraL; move/eqP->; apply: mFT_nonSolvable.
Qed.

Lemma mFT_pgroup_proper p P : p.-group P -> P \proper G.
Proof. by move/pgroup_sol; rewrite mFT_sol_proper. Qed.

Lemma mFT_norm_proper H : H :!=: 1 -> H \proper G -> 'N(H) \proper G.
Proof.
move=> ntH; rewrite !properT; apply: contra; move/eqP=> nHG; apply/eqP.
move/eqP: ntH; case/simpleP: mFT_simple => _; case/(_ H) => //=.
by rewrite -nHG normalG.
Qed.

Lemma cent_mFT_trivial : 'C(G) = 1.
Proof.
apply/eqP; apply: contraR mFT_nonAbelian => ntC.
rewrite /abelian subTset /= eqEproper subsetT /=; apply/negP=> prC.
have:= mFT_norm_proper ntC prC.
by rewrite /proper subsetT norms_cent ?normG.
Qed.

Lemma mFT_cent_proper H : H :!=: 1 -> 'C(H) \proper G.
Proof.
case: (eqsVneq H G) => [-> | ].
  by rewrite cent_mFT_trivial properT eq_sym.
rewrite -properT => prH ntH; apply: sub_proper_trans (cent_sub H) _.
exact: mFT_norm_proper.
Qed.

Lemma mFT_cent1_proper x : x != 1 -> 'C[x] \proper G.
Proof. by rewrite -cycle_eq1 -cent_cycle; apply: mFT_cent_proper. Qed.

Lemma mFT_quo_sol M H : H :!=: 1 -> solvable (M / H).
Proof.
move=> ntH; case: (eqsVneq H G) => [-> |].
  rewrite [_ / _](trivgP _) ?abelian_sol ?abelian1 //.
  by rewrite quotient_sub1 ?normsG ?subsetT.
rewrite -properT => prH; rewrite -quotientInorm morphim_sol //.
by apply: solvableS (subsetIr _ _) (mFT_sol _); rewrite mFT_norm_proper.
Qed.

(* Maximal groups of the minimal FT counterexample, as defined at the start   *)
(* of B & G, section 7.                                                       *)
Definition minSimple_max_groups := [set M : {group gT} | maximal M G].
Local Notation "'M" := minSimple_max_groups : group_scope.

Definition minSimple_max_groups_of (H : sT) := [set M in 'M | H \subset M].
Local Notation "''M' ( H )" := (minSimple_max_groups_of H) : group_scope.

Definition minSimple_uniq_max_groups := [set U : {group gT} | #|'M(U)| == 1%N].
Local Notation "'U" := minSimple_uniq_max_groups : group_scope.

Definition minSimple_SCN_at n p := \bigcup_(P in 'Syl_p(G)) 'SCN_n(P).

Lemma mmax_exists H : H \proper G -> {M | M \in 'M(H)}.
Proof.
case/(@maxgroup_exists _ (fun M => M \proper G)) => M maxM sHM.
by exists M; rewrite !inE sHM andbT.
Qed.

Lemma any_mmax : {M : {group gT} | M \in 'M}.
Proof. by have [M] := mmax_exists mFT_gt1; case/setIdP; exists M. Qed.

Lemma mmax_proper M : M \in 'M -> M \proper G.
Proof. by rewrite inE; apply: maxgroupp. Qed.

Lemma mmax_sol M : M \in 'M -> solvable M.
Proof. by move/mmax_proper/mFT_sol. Qed.

Lemma mmax_max M H : M \in 'M -> H \proper G -> M \subset H -> H :=: M.
Proof. by rewrite inE; case/maxgroupP=> _; apply. Qed.

Lemma eq_mmax : {in 'M &, forall M H, M \subset H -> M :=: H}.
Proof. by move=> M H Mmax; move/mmax_proper=> prH; move/mmax_max->. Qed.

Lemma sub_mmax_proper M H : M \in 'M -> H \subset M -> H \proper G.
Proof. by move=> maxM sHM; apply: sub_proper_trans (mmax_proper maxM). Qed.

Lemma mmax_norm X M :
  M \in 'M -> X :!=: 1 -> X \proper G -> M \subset 'N(X) -> 'N(X) = M.
Proof. by move=> maxM ntX prX; apply: mmax_max (mFT_norm_proper _ _). Qed.

Lemma mmax_normal_subset A M :
  M \in 'M -> A <| M -> ~~ (A \subset [1]) -> 'N(A) = M.
Proof.
rewrite -gen_subG subG1 => maxM /andP[sAM nAM] ntGA.
rewrite (mmax_max maxM) // (sub_proper_trans (norm_gen _)) ?mFT_norm_proper //.
by rewrite (sub_mmax_proper maxM) // gen_subG.
Qed.

Lemma mmax_normal M H : M \in 'M -> H <| M -> H :!=: 1 -> 'N(H) = M.
Proof. by rewrite -subG1; apply: mmax_normal_subset. Qed.

Lemma mmax_sigma_Sylow p P M :
  M \in 'M -> p.-Sylow(M) P -> 'N(P) \subset M -> p.-Sylow(G) P.
Proof.
by move=> maxM sylP sNM; rewrite -Sylow_subnorm setTI (pHall_subl _ sNM) ?normG.
Qed.

Lemma mmax_neq1 M : M \in 'M -> M :!=: 1.
Proof.
move=> maxM; apply: contra mFT_nonAbelian; move/eqP=> M1.
case: (eqVneq G 1) => [-> | ]; first exact: abelian1.
case/trivgPn=> x; rewrite -cycle_subG -cycle_eq1 subEproper /=.
case/predU1P=> [<- | ]; first by rewrite cycle_abelian.
by move/(mmax_max maxM)=> ->; rewrite M1 ?sub1G ?eqxx.
Qed.

Lemma norm_mmax M : M \in 'M -> 'N(M) = M.
Proof.
move=> maxM; apply: mmax_max (normG M) => //.
exact: (mFT_norm_proper (mmax_neq1 maxM) (mmax_proper maxM)).
Qed.

Lemma mmaxJ M x : (M :^ x \in 'M)%G = (M \in 'M).
Proof. by rewrite !inE /= -{1}[G](@conjGid _ _ x) ?maximalJ ?inE. Qed.

Lemma mmax_ofS H K : H \subset K -> 'M(K) \subset 'M(H).
Proof.
move=> sHK; apply/subsetP=> M; rewrite !inE => /andP[->].
exact: subset_trans.
Qed.

Lemma mmax_ofJ K x M : ((M :^ x)%G \in 'M(K :^ x)) = (M \in 'M(K)).
Proof. by rewrite inE mmaxJ conjSg !inE. Qed.

Lemma uniq_mmaxP U : reflect (exists M, 'M(U) = [set M]) (U \in 'U).
Proof. by rewrite inE; apply: cards1P. Qed.
Implicit Arguments uniq_mmaxP [U].

Lemma mem_uniq_mmax U M : 'M(U) = [set M] -> M \in 'M /\ U \subset M.
Proof. by move/setP/(_ M); rewrite set11 => /setIdP. Qed.

Lemma eq_uniq_mmax U M H :
  'M(U) = [set M] -> H \in 'M -> U \subset H -> H :=: M.
Proof.
by move=> uU_M maxH sUH; apply/congr_group/set1P; rewrite -uU_M inE maxH.
Qed.

Lemma def_uniq_mmax U M :
  U \in 'U -> M \in 'M -> U \subset M -> 'M(U) = [set M].
Proof.
case/uniq_mmaxP=> D uU_D maxM sUM.
by rewrite (group_inj (eq_uniq_mmax uU_D maxM sUM)).
Qed.

Lemma uniq_mmax_subset1 U M :
  M \in 'M -> U \subset M -> (U \in 'U) = ('M(U) \subset [set M]).
Proof.
move=> maxM sUM; apply/idP/idP=> uU; first by rewrite -(def_uniq_mmax uU).
by apply/uniq_mmaxP; exists M; apply/eqP; rewrite eqEsubset uU sub1set inE maxM.
Qed.

Lemma sub_uniq_mmax U M H :
  'M(U) = [set M] -> U \subset H -> H \proper G -> H \subset M.
Proof.
move=> uU_M sUH; case/mmax_exists=> D; case/setIdP=> maxD sHD.
by rewrite -(eq_uniq_mmax uU_M maxD) ?(subset_trans sUH).
Qed.

Lemma mmax_sup_id M : M \in 'M -> 'M(M) = [set M].
Proof.
move=> maxM; apply/eqP; rewrite eqEsubset sub1set inE maxM subxx !andbT.
apply/subsetP=> H; case/setIdP=> maxH; rewrite inE -val_eqE /=.
by move/eq_mmax=> ->.
Qed.

Lemma mmax_uniq_id : {subset 'M <= 'U}.
Proof. by move=> M maxM; apply/uniq_mmaxP; exists M; apply: mmax_sup_id. Qed.

Lemma def_uniq_mmaxJ M K x : 'M(K) = [set M] -> 'M(K :^ x) = [set M :^ x]%G.
Proof.
move=> uK_M; apply/setP=> L; rewrite -(actKV 'JG x L) mmax_ofJ uK_M.
by rewrite !inE (inj_eq (act_inj 'JG x)).
Qed.

Lemma uniq_mmaxJ K x :((K :^ x)%G \in 'U) = (K \in 'U).
Proof.
apply/uniq_mmaxP/uniq_mmaxP=> [] [M uK_M].
  by exists (M :^ x^-1)%G; rewrite -(conjsgK x K); apply: def_uniq_mmaxJ.
by exists (M :^ x)%G; apply: def_uniq_mmaxJ.
Qed.

Lemma uniq_mmax_norm_sub (M U : {group gT}) :
  'M(U) = [set M] -> 'N(U) \subset M.
Proof.
move=> uU_M; have [maxM _] := mem_uniq_mmax uU_M.
apply/subsetP=> x nUx; rewrite -(norm_mmax maxM) inE.
have:= set11 M; rewrite -uU_M -(mmax_ofJ _ x) (normP nUx) uU_M.
by move/set1P/congr_group->.
Qed.

Lemma uniq_mmax_neq1 (U : {group gT}) : U \in 'U -> U :!=: 1.
Proof.
case/uniq_mmaxP=> M uU_M; have [maxM _] := mem_uniq_mmax uU_M.
apply: contraL (uniq_mmax_norm_sub uU_M); move/eqP->.
by rewrite norm1 subTset -properT mmax_proper.
Qed.

Lemma def_uniq_mmaxS M U V :
  U \subset V -> V \proper G -> 'M(U) = [set M] -> 'M(V) = [set M].
Proof.
move=> sUV prV uU_M; apply/eqP; rewrite eqEsubset sub1set -uU_M.
rewrite mmax_ofS //= inE (sub_uniq_mmax uU_M) //.
by case/mem_uniq_mmax: uU_M => ->.
Qed.

Lemma uniq_mmaxS U V : U \subset V -> V \proper G -> U \in 'U -> V \in 'U.
Proof.
move=> sUV prV /uniq_mmaxP[M uU_M]; apply/uniq_mmaxP; exists M.
exact: def_uniq_mmaxS uU_M.
Qed.

End MinSimpleOdd.

Implicit Arguments uniq_mmaxP [gT U].
Prenex Implicits uniq_mmaxP.

Notation "''M'" := (minSimple_max_groups _) : group_scope.
Notation "''M' ( H )" := (minSimple_max_groups_of H) : group_scope.
Notation "''U'" := (minSimple_uniq_max_groups _) : group_scope.
Notation "''SCN_' n [ p ]" := (minSimple_SCN_at _ n p) : group_scope.

Section Hypothesis7_1.

Variable gT : finGroupType.
Implicit Types X Y A P Q : {group gT}.
Local Notation G := [set: gT].

Definition normed_pgroups (X A : {set gT}) pi :=
  [set Y : {group gT} | pi.-subgroup(X) Y & A \subset 'N(Y)].
Local Notation "|/|_ X ( A ; pi )" := (normed_pgroups X A pi) : group_scope.

Definition max_normed_pgroups (A : {set gT}) pi :=
  [set Y : {group gT} | [max Y | pi.-group Y & A \subset 'N(Y)]].
Local Notation "|/|* ( A ; pi )" := (max_normed_pgroups A pi) : group_scope.

(* This is the statement for B & G, Hypothesis 7.1. *)
Inductive normed_constrained (A : {set gT}) :=
  NormedConstrained (pi := \pi(A)) of A != 1 & A \proper G
  & forall X Y : {group gT},
    A \subset X -> X \proper G -> Y \in |/|_X(A; pi^') -> Y \subset 'O_pi^'(X).

Variable pi : nat_pred.

Lemma max_normed_exists A X :
  pi.-group X -> A \subset 'N(X) -> {Y | Y \in |/|*(A; pi) & X \subset Y}.
Proof.
move=> piX nXA; pose piAn Y := pi.-group(Y) && (A \subset 'N(Y)).
have [|Y] := @maxgroup_exists _ piAn X; first by rewrite /piAn piX.
by exists Y; rewrite // inE.
Qed.

Lemma mem_max_normed A X : X \in |/|*(A; pi) -> pi.-group X /\ A \subset 'N(X).
Proof. by rewrite inE; move/maxgroupp; move/andP. Qed.

Lemma norm_acts_max_norm P : [acts 'N(P), on |/|*(P; pi) | 'JG].
Proof.
apply/subsetP=> z Nz; rewrite !inE; apply/subsetP=> Q; rewrite !inE.
case/maxgroupP=> qQ maxQ; apply/maxgroupP; rewrite pgroupJ norm_conj_norm //.
split=> // Y; rewrite sub_conjg /= => qY; move/maxQ=> <-; rewrite ?conjsgKV //.
by rewrite pgroupJ norm_conj_norm ?groupV.
Qed.

Lemma trivg_max_norm P : 1%G \in |/|*(P; pi) -> |/|*(P; pi) = [set 1%G].
Proof.
move=> max1; apply/eqP; rewrite eqEsubset sub1set max1 andbT.
apply/subsetP=> Q; rewrite !inE -val_eqE /= in max1 *.
by case/maxgroupP: max1 => _ max1; move/maxgroupp; move/max1->; rewrite ?sub1G.
Qed.

Lemma max_normed_uniq A P Q :
    |/|*(A; pi) = [set Q] -> A \subset P -> P \subset 'N(Q) ->
  |/|*(P; pi) = [set Q].
Proof.
move=> defAmax sAP nQP; have: Q \in |/|*(A; pi) by rewrite defAmax set11.
rewrite inE; case/maxgroupP; case/andP=> piQ _ maxQ.
apply/setP=> X; rewrite !inE -val_eqE /=; apply/maxgroupP/eqP=> [[]|->{X}].
  case/andP=> piX nXP maxX; have nXA := subset_trans sAP nXP.
  have [Y] := max_normed_exists piX nXA.
  by rewrite defAmax; move/set1P->; move/maxX=> -> //; rewrite piQ.
rewrite piQ; split=> // X; case/andP=> piX nXP sQX.
by rewrite (maxQ X) // piX (subset_trans sAP).
Qed.

End Hypothesis7_1.

Notation "|/|_ X ( A ; pi )" := (normed_pgroups X A pi) : group_scope.
Notation "|/|* ( A ; pi )" := (max_normed_pgroups A pi) : group_scope.

Section Seven.

Variable gT : minSimpleOddGroupType.
Local Notation G := (TheMinSimpleOddGroup gT).
Local Notation grT := {group gT}.
Implicit Types H P Q R K M A B : grT.
Implicit Type p q : nat.

Section NormedConstrained.

Variables (q : nat) (A : grT).
Let pi := Eval simpl in \pi(A).
Let K := 'O_pi^'('C(A)).
Let nsKC : K <| 'C(A) := pcore_normal _ _.

Lemma cent_core_acts_max_norm : [acts K, on |/|*(A; q) | 'JG].
Proof.
by rewrite (subset_trans _ (norm_acts_max_norm _ _)) ?cents_norm ?pcore_sub.
Qed.
Let actsKmax := actsP cent_core_acts_max_norm.

Hypotheses (cstrA : normed_constrained A) (pi'q : q \notin pi).

Let hyp71 H R :
  A \subset H -> H \proper G -> R \in |/|_H(A; pi^') -> R \subset 'O_pi^'(H).
Proof. by case: cstrA H R. Qed.

(* This is the observation between B & G, Hypothesis 7.1 and Lemma 7.1. *)
Remark normed_constrained_Hall : pi^'.-Hall('C(A)) K.
Proof.
have [_ ntA prA _] := cstrA; rewrite -[setT]/G in prA.
rewrite /pHall pcore_pgroup pcore_sub pnatNK /=.
rewrite -card_quotient ?gFnorm //= -/K.
apply/pgroupP=> p p_pr; case/Cauchy=> // Kx; case/morphimP=> x Nx Cx ->{Kx}.
rewrite /order -quotient_cycle //= -/K => def_p; apply/idPn=> pi'p.
have [P sylP] := Sylow_exists p <[x]>; have [sPx pP _]:= and3P sylP.
suffices: P \subset K.
  have nKP: P \subset 'N(K) by rewrite (subset_trans sPx) ?cycle_subG.
  rewrite -quotient_sub1 //= -/K (sameP trivgP eqP) trivg_card1.
  rewrite (card_Hall (morphim_pHall _ nKP sylP)) def_p part_pnat_id ?pnat_id //.
  by case: eqP p_pr => // ->.
suffices sP_pAC: P \subset 'O_pi^'(A <*> 'C(A)).
  rewrite (subset_trans sP_pAC) ?pcore_max ?pcore_pgroup //.
  rewrite /normal gFnorm_trans ?normsG ?joing_subr // andbT.
  rewrite -quotient_sub1; last first.
    by rewrite gFsub_trans // join_subG !(normG, norms_cent).
  rewrite /= -(setIidPr (pcore_sub _ _)) quotientGI ?joing_subr //=.
  rewrite {1}cent_joinEr // quotientMidr coprime_TIg // coprime_morph //.
  by rewrite coprime_pi' ?cardG_gt0 //= -/pi [pnat _ _]pcore_pgroup.
apply: hyp71; first exact: joing_subl.
  apply: sub_proper_trans (mFT_norm_proper ntA prA).
  by rewrite join_subG normG cent_sub.
have sPC: P \subset 'C(A) by rewrite (subset_trans sPx) ?cycle_subG.
rewrite inE /psubgroup cents_norm 1?centsC // andbT.
rewrite (subset_trans sPC) ?joing_subr //=.
by apply: sub_in_pnat pP => p' _; move/eqnP->.
Qed.
Let hallK := normed_constrained_Hall.

(* This is B & G, Lemma 7.1. *)
Lemma normed_constrained_meet_trans Q1 Q2 H :
    A \subset H -> H \proper G -> Q1 \in |/|*(A; q) -> Q2 \in |/|*(A; q) ->
    Q1 :&: H != 1 -> Q2 :&: H != 1 ->
  exists2 k, k \in K & Q2 :=: Q1 :^ k.
Proof.
move: {2}_.+1 (ltnSn (#|G| - #|Q1 :&: Q2|)) => m.
elim: m => // m IHm in H Q1 Q2 * => geQ12m sAH prHG maxQ1 maxQ2 ntHQ1 ntHQ2.
have:= maxQ1; rewrite inE => /maxgroupP[/andP[qQ1 nQ1A] maxQ1P].
have:= maxQ2; rewrite inE => /maxgroupP[/andP[qQ2 nQ2A] maxQ2P].
have prQ12: Q1 :&: Q2 \proper G.
  rewrite properT; apply: contraNneq (mFT_nonSolvable gT) => <-.
  by apply: pgroup_sol (pgroupS _ qQ1); rewrite subsetIl.
wlog defH: H prHG sAH ntHQ1 ntHQ2 / Q1 :&: Q2 != 1 -> H :=: 'N(Q1 :&: Q2).
  case: (eqVneq (Q1 :&: Q2) 1) => [-> | ntQ12] IH.
    by apply: (IH H) => //; case/eqP.
  apply: (IH 'N(Q1 :&: Q2)%G); rewrite ?normsI ?mFT_norm_proper //;
    apply: contra ntQ12; rewrite -!subG1; apply: subset_trans;
    by rewrite subsetI normG (subsetIl, subsetIr).
pose L := 'O_pi^'(H); have sLH: L \subset H := pcore_sub _ _.
have [nLA coLA solL]: [/\ A \subset 'N(L), coprime #|L| #|A| & solvable L].
  rewrite gFnorm_trans ?normsG // coprime_sym coprime_pi' ?cardG_gt0 //.
  by rewrite -pgroupE pcore_pgroup (solvableS sLH) ?mFT_sol.
have Qsyl Q: Q \in |/|*(A; q) -> Q :&: H != 1 ->
  exists R : {group _}, [/\ q.-Sylow(L) R, A \subset 'N(R) & Q :&: H \subset R].
- case/mem_max_normed=> qQ nQA ntQH.
  have qQH: q.-group (Q :&: H) by rewrite (pgroupS _ qQ) ?subsetIl.
  have nQHA: A \subset 'N(Q :&: H) by rewrite normsI // normsG.
  apply: coprime_Hall_subset => //; apply: (hyp71) => //.
  rewrite inE nQHA /psubgroup subsetIr andbT.
  by apply: sub_in_pnat qQH => p _; move/eqnP->.
have [R1 [sylR1 nR1A sQR1]] := Qsyl _ maxQ1 ntHQ1.
have [R2 [sylR2 nR2A sQR2]] := Qsyl _ maxQ2 ntHQ2.
have [h Ch defR2] := coprime_Hall_trans nLA coLA solL sylR2 nR2A sylR1 nR1A.
have{Ch} [Hh Kh]: h \in H /\ h \in K.
  case/setIP: Ch => Lh Ch; rewrite (subsetP sLH) //.
  rewrite (mem_normal_Hall hallK (pcore_normal _ _)) //.
  by rewrite (mem_p_elt _ Lh) ?pcore_pgroup.
have [Q3 maxQ3 sR2Q3] := max_normed_exists (pHall_pgroup sylR2) nR2A.
have maxQ1h: (Q1 :^ h)%G \in |/|*(A; q) by rewrite actsKmax.
case: (eqsVneq Q1 Q2) => [| neQ12]; first by exists 1; rewrite ?group1 ?conjsg1.
have ntHQ3: Q3 :&: H != 1.
  by apply: subG1_contra ntHQ2; rewrite subsetI subsetIr (subset_trans sQR2).
have ntHQ1h: (Q1 :^ h) :&: H != 1.
  by move: ntHQ1; rewrite !trivg_card1 -(cardJg _ h) conjIg (conjGid Hh).
suff [prI1 prI2]: Q1 :&: Q2 \proper Q1 :&: R1 /\ Q1 :&: Q2 \proper Q2 :&: R2.
  have: #|G| - #|(Q1 :^ h) :&: Q3| < m.
    rewrite ltnS in geQ12m; apply: leq_trans geQ12m.
    rewrite ltn_sub2l ?(proper_card prQ12) // -(cardJg _ h) proper_card //.
    by rewrite (proper_sub_trans _ (setIS _ sR2Q3)) // defR2 -conjIg properJ.
  have: #|G| - #|Q3 :&: Q2| < m.
    rewrite ltnS in geQ12m; apply: leq_trans geQ12m.
    rewrite ltn_sub2l ?proper_card // (proper_sub_trans prI2) //.
    by rewrite setIC setISS.
  case/(IHm H) => // k2 Kk2 defQ2; case/(IHm H) => // k3 Kk3 defQ3.
  by exists (h * k3 * k2); rewrite ?groupM ?conjsgM // -defQ3.
case: (eqVneq (Q1 :&: Q2) 1) => [-> | ntQ12].
  by rewrite !proper1G; split; [move: ntHQ1 | move: ntHQ2];
     apply: subG1_contra; rewrite subsetI subsetIl.
rewrite -(setIidPr (subset_trans (pHall_sub sylR1) sLH)) setIA.
rewrite -(setIidPr (subset_trans (pHall_sub sylR2) sLH)) setIA.
rewrite (setIidPl sQR1) (setIidPl sQR2) {}defH //.
have nilQ1 := pgroup_nil qQ1; have nilQ2 := pgroup_nil qQ2.
rewrite !nilpotent_proper_norm /proper ?subsetIl ?subsetIr ?subsetI ?subxx //=.
  by rewrite andbT; apply: contra neQ12 => sQ21; rewrite (maxQ2P Q1) ?qQ1.
by apply: contra neQ12 => sQ12; rewrite (maxQ1P Q2) ?qQ2.
Qed.

(* This is B & G, Theorem 7.2. *)
Theorem normed_constrained_rank3_trans :
  'r('Z(A)) >= 3 -> [transitive K, on |/|*(A; q) | 'JG].
Proof.
case/rank_geP=> B /nElemP[p]; rewrite !inE subsetI -2!andbA.
case/and4P=> sBA cAB abelB mB3; have [_ cBB _] := and3P abelB.
have q'B: forall Q, q.-group Q -> coprime #|Q| #|B|.
  move=> Q qQ; rewrite coprime_sym (coprimeSg sBA) ?coprime_pi' //.
  exact: pi_pnat qQ _.
have [Q1 maxQ1 _] := max_normed_exists (pgroup1 _ q) (norms1 A).
apply/imsetP; exists Q1 => //; apply/setP=> Q2.
apply/idP/imsetP=> [maxQ2|[k Kk] ->]; last by rewrite actsKmax.
have [qQ1 nQ1A]:= mem_max_normed maxQ1; have [qQ2 nQ2A]:= mem_max_normed maxQ2.
case: (eqVneq Q1 1%G) => [trQ1 | ntQ1].
  exists 1; rewrite ?group1 // act1; apply/eqP.
  by rewrite trivg_max_norm -trQ1 // inE in maxQ2.
case: (eqVneq Q2 1%G) => [trQ2 | ntQ2].
  by case/negP: ntQ1; rewrite trivg_max_norm -trQ2 // inE in maxQ1 *.
have: [exists (C : grT | 'C_Q1(C) != 1), cyclic (B / C) && (C <| B)].
  apply: contraR ntQ1 => trQ1; have: B \subset 'N(Q1) := subset_trans sBA nQ1A.
  rewrite -val_eqE -subG1 /=; move/coprime_abelian_gen_cent <-; rewrite ?q'B //.
  rewrite gen_subG; apply/bigcupsP=> C cocyC; rewrite subG1.
  by apply: contraR trQ1 => ntCC; apply/existsP; exists C; rewrite ntCC.
case/existsP=> C /and3P[ntCQ1 cycBC nsCB]; have [sCB nCB]:= andP nsCB.
have{mB3} ncycC: ~~ cyclic C.
  rewrite (abelem_cyclic (quotient_abelem _ abelB)) ?card_quotient // in cycBC.
  rewrite -divgS // logn_div ?cardSg // leq_subLR addn1 (eqP mB3) in cycBC.
  by rewrite (abelem_cyclic (abelemS sCB abelB)) -ltnNge.
have: [exists (z | 'C_Q2[z] != 1), z \in C^#].
  apply: contraR ntQ2 => trQ2; have:= subset_trans sCB (subset_trans sBA nQ2A).
  rewrite -[_ == _]subG1 /=.
  move/coprime_abelian_gen_cent1 <-; rewrite ?(abelianS sCB) //; last first.
    by rewrite (coprimegS sCB) ?q'B.
  rewrite gen_subG; apply/bigcupsP=> z Cz.
  by apply: contraR trQ2 => ntCz; apply/existsP; exists z; rewrite -subG1 ntCz.
case/existsP=> z; rewrite !inE => /and3P[ntzQ2 ntz Cz].
have prCz: 'C[z] \proper G by rewrite -cent_cycle mFT_cent_proper ?cycle_eq1.
have sACz: A \subset 'C[z] by rewrite sub_cent1 (subsetP cAB) ?(subsetP sCB).
have [|//|k Kk defQ2]:= normed_constrained_meet_trans sACz prCz maxQ1 maxQ2.
  by apply: subG1_contra ntCQ1; rewrite setIS //= -cent_cycle centS ?cycle_subG.
by exists k => //; apply: val_inj.
Qed.

(* This is B & G, Theorem 7.3. *)
Theorem normed_constrained_rank2_trans :
  q %| #|'C(A)| -> 'r('Z(A)) >= 2 -> [transitive K, on |/|*(A; q) | 'JG].
Proof.
move=> qC /rank_geP[B /nElemP[p /setIdP[/setIdP[/subsetIP[sBA cAB] abelB] oB]]].
have [_ cBB _] := and3P abelB.
have{abelB oB} ncycB: ~~ cyclic B by rewrite (abelem_cyclic abelB) (eqP oB).
have [R0 sylR0] := Sylow_exists q 'C(A); have [cAR0 qR0 _] := and3P sylR0.
have nR0A: A \subset 'N(R0) by rewrite cents_norm // centsC.
have{nR0A} [R maxR sR0R] := max_normed_exists qR0 nR0A.
apply/imsetP; exists R => //; apply/setP=> Q.
apply/idP/imsetP=> [maxQ|[k Kk] ->]; last by rewrite actsKmax.
have [qR nRA]:= mem_max_normed maxR; have [qQ nQA]:= mem_max_normed maxQ.
have [R1 | ntR] := eqVneq R 1%G.
  rewrite trivg_max_norm -R1 // in maxQ.
  by exists 1; rewrite ?group1 ?act1 ?(set1P maxQ).
have ntQ: Q != 1%G.
  by apply: contra ntR => Q1; rewrite trivg_max_norm -(eqP Q1) // inE in maxR *.
have ntRC: 'C_R(A) != 1.
  have sR0CR: R0 \subset 'C_R(A) by rewrite subsetI sR0R.
  suffices: R0 :!=: 1 by apply: subG1_contra.
  move: ntR; rewrite -!cardG_gt1 -(part_pnat_id qR) (card_Hall sylR0).
  by rewrite !p_part_gt1 !mem_primes !cardG_gt0 qC => /and3P[->].
have: [exists (z | 'C_Q[z] != 1), z \in B^#].
  apply: contraR ntQ => trQ; have:= subset_trans sBA nQA.
  rewrite -[_ == _]subG1=> /coprime_abelian_gen_cent1 <- //; last first.
    by rewrite coprime_sym (coprimeSg sBA) ?coprime_pi' /pgroup ?(pi_pnat qQ).
  rewrite gen_subG; apply/bigcupsP=> z Cz; rewrite subG1.
  by apply: contraR trQ => ntCz; apply/existsP; exists z; rewrite ntCz.
case/existsP=> z; rewrite 2!inE => /and3P[ntzQ ntz Bz].
have prCz: 'C[z] \proper G by rewrite -cent_cycle mFT_cent_proper ?cycle_eq1.
have sACz: A \subset 'C[z] by rewrite sub_cent1 (subsetP cAB).
have [|//|k Kk defQ2]:= normed_constrained_meet_trans sACz prCz maxR maxQ.
  apply: subG1_contra ntRC; rewrite setIS //=.
  by rewrite -cent_cycle centS // cycle_subG (subsetP sBA).
by exists k => //; apply: val_inj.
Qed.

(* This is B & G, Theorem 7.4. *)
Theorem normed_trans_superset P :
    A <|<| P -> pi.-group P -> [transitive K, on |/|*(A; q) | 'JG] ->
 [/\ 'C_K(P) = 'O_pi^'('C(P)),
     [transitive 'O_pi^'('C(P)), on |/|*(P; q) | 'JG],
     |/|*(P; q) \subset |/|*(A; q)
   & {in |/|*(P; q), forall Q, P :&: 'N(P)^`(1) \subset 'N(Q)^`(1)
                            /\ 'N(P) = 'C_K(P) * 'N_('N(P))(Q)}].
Proof.
move=> snAP piP trnK; set KP := 'O_pi^'('C(P)).
have defK B: A \subset B -> 'C_K(B) = 'O_pi^'('C(B)).
  move=> sAB; apply/eqP; rewrite eqEsubset {1}setIC pcoreS ?centS // subsetI.
  by rewrite gFsub (sub_Hall_pcore hallK) ?pcore_pgroup // gFsub_trans ?centS.
suffices: [transitive KP, on |/|*(P; q) | 'JG] /\ |/|*(P; q) \subset |/|*(A; q).
  have nsKPN: KP <| 'N(P) := gFnormal_trans _ (cent_normal _).
  case=> trKP smnPA; rewrite (defK _ (subnormal_sub snAP)); split=> // Q maxQ.
  have defNP: KP * 'N_('N(P))(Q) = 'N(P).
    rewrite -(astab1JG Q) -normC; last by rewrite subIset 1?normal_norm.
    apply/(subgroup_transitiveP maxQ); rewrite ?normal_sub //=.
    by rewrite (atrans_supgroup _ trKP) ?norm_acts_max_norm ?normal_sub.
  split=> //; move/pprod_focal_coprime: defNP => -> //.
  - by rewrite subIset // orbC commgSS ?subsetIr.
  - by rewrite subsetI normG; case/mem_max_normed: maxQ.
  by rewrite (p'nat_coprime (pcore_pgroup _ _)).
elim: {P}_.+1 {-2}P (ltnSn #|P|) => // m IHm P lePm in KP piP snAP *.
wlog{snAP} [B maxnB snAB]: / {B : grT | maxnormal B P P & A <|<| B}.
  case/subnormalEr: snAP => [|[D [snAD nDP prDP]]]; first by rewrite /KP => <-.
  have [B maxnB sDB]: {B : grT | maxnormal B P P & D \subset B}.
    by apply: maxgroup_exists; rewrite prDP normal_norm.
  apply; exists B => //; apply: subnormal_trans snAD (normal_subnormal _).
  by apply: normalS sDB _ nDP; case/andP: (maxgroupp maxnB); case/andP.
have [prBP nBP] := andP (maxgroupp maxnB); have sBP := proper_sub prBP.
have{lePm}: #|B| < m by apply: leq_trans (proper_card prBP) _.
case/IHm=> {IHm}// [|trnB smnBA]; first by rewrite (pgroupS sBP).
have{maxnB} abelPB: is_abelem (P / B).
  apply: charsimple_solvable (maxnormal_charsimple _ maxnB) _ => //.
  have [_ ntA _ _] := cstrA; have sAB := subnormal_sub snAB.
  by apply: mFT_quo_sol; apply: contraL sAB; move/eqP->; rewrite subG1.
have{abelPB} [p p_pr pPB]: exists2 p, prime p & p.-group (P / B).
  by case/is_abelemP: abelPB => p p_pr; case/andP; exists p.
have{prBP} pi_p: p \in pi.
  case/pgroup_pdiv: pPB => [|_ pPB _].
    by rewrite -subG1 quotient_sub1 // proper_subn.
  by apply: pgroupP p_pr pPB; apply: quotient_pgroup.
pose S := |/|*(B; q); have p'S: #|S| %% p != 0.
  have pi'S: pi^'.-nat #|S| := pnat_dvd (atrans_dvd trnB) (pcore_pgroup _ _).
  by rewrite -prime_coprime // (pnat_coprime _ pi'S) ?pnatE.
have{p'S} [Q S_Q nQP]: exists2 Q, Q \in S & P \subset 'N(Q).
  have sTSB: setT \subset G / B by rewrite -im_quotient quotientS ?subsetT.
  have modBE: {in P & S, forall x Q, ('JG %% B) Q (coset B x) = 'JG Q x}%act.
    move=> x Q Px; rewrite inE; move/maxgroupp; case/andP=> _ nQB.
    by rewrite /= modactE ?(subsetP nBP) ?afixJG ?setTI ?inE.
  have actsPB: [acts P / B, on S | 'JG %% B \ sTSB].
    apply/subsetP=> _ /morphimP[x Nx Px ->].
    rewrite !inE; apply/subsetP=> Q S_Q; rewrite inE /= modBE //.
    by rewrite (actsP (norm_acts_max_norm q B)).
  move: p'S; rewrite (pgroup_fix_mod pPB actsPB); set nQ := #|_|.
  case: (posnP nQ) => [->|]; first by rewrite mod0n.
  rewrite lt0n; case/existsP=> Q /setIP[Q_S fixQ]; exists Q => //.
  apply/normsP=> x Px; apply: congr_group; have Nx := subsetP nBP x Px.
  by have:= afixP fixQ (coset B x); rewrite /= modBE ?mem_morphim //= => ->.
have [qQ _]:= mem_max_normed S_Q.
have{qQ nQP} [Q0 maxQ0 sQQ0] := max_normed_exists qQ nQP.
have [_ nQ0P]:= mem_max_normed maxQ0.
have actsKmnP: [acts 'O_pi^'('C(P)), on |/|*(P; q) | 'JG].
  by rewrite (subset_trans _ (norm_acts_max_norm q P)) // cents_norm ?pcore_sub.
case nt_mnP: (1%G \in |/|*(P; q)) => [|{Q S_Q sQQ0}].
  rewrite atrans_acts_card actsKmnP trivg_max_norm // imset_set1 in maxQ0 *.
  have <-: Q = 1%G by apply/trivGP; rewrite -(congr_group (set1P maxQ0)).
  by rewrite cards1 sub1set (subsetP smnBA).
have sAB := subnormal_sub snAB; have sAP := subset_trans sAB sBP.
have smnP_S: |/|*(P; q) \subset S.
  apply/subsetP=> Q1 maxQ1; have [qQ1 nQ1P] := mem_max_normed maxQ1.
  have ntQ1: Q1 != 1%G by case: eqP nt_mnP maxQ1 => // -> ->.
  have prNQ1: 'N(Q1) \proper G := mFT_norm_proper ntQ1 (mFT_pgroup_proper qQ1).
  have nQ1A: A \subset 'N(Q1) := subset_trans sAP nQ1P.
  have [Q2 maxQ2 sQ12] := max_normed_exists qQ1 (subset_trans sBP nQ1P).
  have [qQ2 nQ2B] := mem_max_normed maxQ2; apply: etrans maxQ2; congr in_mem.
  apply: val_inj; suffices: q.-Sylow(Q2) Q1 by move/pHall_id=> /= ->.
  have qNQ2: q.-group 'N_Q2(Q1) by rewrite (pgroupS _ qQ2) ?subsetIl.
  pose KN := 'O_pi^'('N(Q1)); have sNQ2_KN: 'N_Q2(Q1) \subset KN.
    rewrite hyp71 // inE normsI ?norms_norm ?(subset_trans sAB nQ2B) //=.
    by rewrite /psubgroup subsetIr andbT; apply: pi_pnat qNQ2 _.
  rewrite -Sylow_subnorm (pHall_subl _ sNQ2_KN) ?subsetI ?sQ12 ?normG //= -/KN.
  suff: exists Q3 : grT, [/\ q.-Sylow(KN) Q3, P \subset 'N(Q3) & Q1 \subset Q3].
    move: maxQ1; rewrite inE; case/maxgroupP=> _ maxQ1 [Q3 [sylQ3 nQ3P sQ13]].
    by rewrite -(maxQ1 Q3) // (pHall_pgroup sylQ3).
  apply: coprime_Hall_subset; rewrite //= -/KN.
  - by rewrite gFnorm_trans ?norms_norm.
  - by rewrite coprime_sym (pnat_coprime piP (pcore_pgroup _ _)).
  - by rewrite (solvableS (pcore_sub _ _)) ?mFT_sol.
  by rewrite pcore_max ?normalG // /pgroup (pi_pnat qQ1).
split; last exact: subset_trans smnP_S smnBA.
apply/imsetP; exists Q0 => //; apply/setP=> Q2.
apply/idP/imsetP=> [maxQ2 | [k Pk ->]]; last by rewrite (actsP actsKmnP).
have [S_Q0 S_Q2]: Q0 \in S /\ Q2 \in S by rewrite !(subsetP smnP_S).
pose KB := 'O_pi^'('C(B)); pose KBP := KB <*> P.
have pi'KB: pi^'.-group KB by apply: pcore_pgroup.
have nKB_P: P \subset 'N(KB) by rewrite gFnorm_trans ?norms_cent.
have [k KBk defQ2]:= atransP2 trnB S_Q0 S_Q2.
have [qQ2 nQ2P] := mem_max_normed maxQ2.
have hallP: pi.-Hall('N_KBP(Q2)) P.
  have sPN: P \subset 'N_KBP(Q2) by rewrite subsetI joing_subr.
  rewrite pHallE eqn_leq -{1}(part_pnat_id piP) dvdn_leq ?partn_dvd ?cardSg //.
  have ->: #|P| = #|KBP|`_pi.
    rewrite /KBP joingC norm_joinEl // coprime_cardMg ?(pnat_coprime piP) //.
    by rewrite partnM // part_pnat_id // part_p'nat // muln1.
  by rewrite sPN dvdn_leq ?partn_dvd ?cardSg ?cardG_gt0 ?subsetIl.
have hallPk: pi.-Hall('N_KBP(Q2)) (P :^ k).
  rewrite pHallE -(card_Hall hallP) cardJg eqxx andbT subsetI /=.
  by rewrite defQ2 normJ conjSg conj_subG ?joing_subr // mem_gen // inE KBk.
have [gz]: exists2 gz, gz \in 'N_KBP(Q2) & P :=: (P :^ k) :^ gz.
  apply: Hall_trans (solvableS (subsetIr _ _) _) hallP hallPk.
  have ntQ2: Q2 != 1%G by case: eqP nt_mnP maxQ2 => // -> ->.
  exact: mFT_sol (mFT_norm_proper ntQ2 (mFT_pgroup_proper qQ2)).
rewrite [KBP]norm_joinEr //= setIC -group_modr //= setIC -/KB.
case/imset2P=> g z; case/setIP=> KBg nQ2g Pz ->{gz} defP.
exists (k * g); last first.
  by apply: val_inj; rewrite /= conjsgM -(normP nQ2g) defQ2.
rewrite /KP -defK // (subsetP (subsetIl _ 'C(B))) //= setIAC defK // -/KB.
rewrite -coprime_norm_cent 1?coprime_sym ?(pnat_coprime piP) //= -/KB.
rewrite inE groupM //; apply/normP.
by rewrite -{2}(conjsgK z P) (conjGid Pz) {2}defP /= !conjsgM conjsgK.
Qed.

End NormedConstrained.

(* This is B & G, Proposition 7.5(a). As this is only used in Proposition    *)
(* 10.10, under the assumption A \in E*_p(G), we avoid the in_pmaxElemE      *)
(* detour A = [set x in 'C_G(A) | x ^+ p == 1], and just use A \in E*_p(G).  *)
Proposition plength_1_normed_constrained p A :
    A :!=: 1 -> A \in 'E*_p(G) -> (forall M, M \proper G -> p.-length_1 M) ->
  normed_constrained A.
Proof. 
move=> ntA EpA pl1subG.
case/pmaxElemP: (EpA); case/pElemP=> sAG; case/and3P=> pA cAA _ _. 
have prA: A \proper G := sub_proper_trans cAA (mFT_cent_proper ntA).
split=> // X Y sAX prX; case/setIdP; case/andP=> sYX p'Y nYA.
have pl1X := pl1subG _ prX; have solX := mFT_sol prX.
have [p_pr _ [r oApr]] := pgroup_pdiv pA ntA.
have oddp: odd p by move: (mFT_odd A); rewrite oApr odd_exp.
have def_pi: \pi(A)^' =i p^'.
  by move=> q; rewrite inE /= oApr pi_of_exp // pi_of_prime.
have{p'Y} p'Y : p^'.-group Y by rewrite -(eq_pgroup _ def_pi).
rewrite (eq_pcore _ def_pi) (@plength1_norm_pmaxElem _ p X A) //.
by rewrite (subsetP (pmaxElemS p (subsetT _))) // setIC 2!inE sAX.
Qed.

(* This is B & G, Proposition 7.5(b). *)
Proposition SCN_normed_constrained p P A :
  p.-Sylow(G) P -> A \in 'SCN_2(P) -> normed_constrained A.
Proof.
move=> sylP; rewrite 2!inE -andbA => /and3P[nsAP /eqP defCA lt1mA].
have [sAP nAP]:= andP nsAP.
have pP := pHall_pgroup sylP; have pA := pgroupS sAP pP.
have abA: abelian A by rewrite /abelian -{1}defCA subsetIr.
have prP: P \proper G := mFT_pgroup_proper pP.
have ntA: A :!=: 1 by rewrite -rank_gt0 ltnW.
pose pi := \pi(A); simpl in pi.
have [p_pr pdvA [r oApr]] := pgroup_pdiv pA ntA.
have{r oApr} def_pi: pi =i (p : nat_pred).
  by move=> p'; rewrite !inE oApr primes_exp // primes_prime ?inE.
have def_pi' := eq_negn def_pi; have defK := eq_pcore _ def_pi'.
pose Z := 'Ohm_1('Z(P)); have sZ_ZP: Z \subset 'Z(P) by apply: Ohm_sub.
have sZP_A: 'Z(P) \subset A by rewrite -defCA setIS ?centS.
have sZA := subset_trans sZ_ZP sZP_A.
have nsA1: 'Ohm_1(A) <| P by apply: gFnormal_trans.
pose inZor1 B := B \subset Z \/ #|Z| = p /\ Z \subset B.
have [B [E2_B nsBP sBZ]]: exists B, [/\ B \in 'E_p^2(A), B <| P & inZor1 B].
  have pZP: p.-group 'Z(P) by apply: pgroupS (center_sub _) pP.
  have pZ: p.-group Z by apply: pgroupS sZ_ZP pZP.
  have abelZ: p.-abelem Z by rewrite Ohm1_abelem ?center_abelian.
  have nsZP: Z <| P := sub_center_normal sZ_ZP; have [sZP nZP] := andP nsZP.
  case: (eqVneq Z 1).
    rewrite -(setIidPr sZ_ZP); move/TI_Ohm1; rewrite setIid.
    by move/(trivg_center_pgroup pP)=> P1; rewrite -subG1 -P1 sAP in ntA.
  case/(pgroup_pdiv pZ)=> _ _ [[|k] /=]; rewrite -/Z => oZ; last first.
    have: 2 <= 'r_p(Z) by rewrite p_rank_abelem // oZ pfactorK.
    case/p_rank_geP=> B; rewrite /= -/Z => Ep2Z_B; exists B.
    rewrite (subsetP (pnElemS _ _ sZA)) //.
    case/setIdP: Ep2Z_B; case/setIdP=> sBZ _ _; split=> //; last by left.
    by rewrite sub_center_normal ?(subset_trans sBZ).
  pose BZ := ('Ohm_1(A) / Z) :&: 'Z(P / Z).
  have ntBz: BZ != 1.
    rewrite meet_center_nil ?quotient_nil ?(pgroup_nil pP) ?quotient_normal //.
    rewrite -subG1 quotient_sub1 ?(subset_trans (normal_sub nsA1) nZP) //= -/Z.
    apply: contraL lt1mA => sA1Z; rewrite -(pfactorK 1 p_pr) -oZ -rank_Ohm1.
    by rewrite -(rank_abelem abelZ) -leqNgt rankS.
  have lt1A1: 1 < logn p #|'Ohm_1(A)| by rewrite -p_rank_abelian -?rank_pgroup.
  have [B [sBA1 nsBP oB]] := normal_pgroup pP nsA1 lt1A1.
  exists B; split=> //; last do [right; split=> //].
    rewrite 2!inE (subset_trans sBA1) ?Ohm_sub // oB pfactorK //.
    by rewrite (abelemS sBA1) ?Ohm1_abelem.
  apply/idPn=> s'BZ; have: B :&: Z = 1 by rewrite setIC prime_TIg ?oZ.
  move/TI_Ohm1; apply/eqP; rewrite meet_center_nil ?(pgroup_nil pP) //.
  by rewrite -cardG_gt1 oB (ltn_exp2l 0 _ (prime_gt1 p_pr)).
split; rewrite ?(sub_proper_trans sAP) // => X Y sAX prX.
rewrite inE defK -andbA (eq_pgroup _ def_pi'); case/and3P=> sYX p'Y nYA.
move: E2_B; rewrite 2!inE -andbA; case/and3P=> sBA abelB dimB2.
have [pB cBB _] := and3P abelB.
have ntB: B :!=: 1 by case: (eqsVneq B 1) dimB2 => // ->; rewrite cards1 logn1.
have cBA b: b \in B -> A \subset 'C[b].
  by move=> Bb; rewrite -cent_set1 centsC sub1set (subsetP abA) ?(subsetP sBA).
have solCB (b : gT): b != 1 -> solvable 'C[b].
  by move=> ntb; rewrite mFT_sol ?mFT_cent1_proper.
wlog{sAX prX} [b B'b defX]: X Y p'Y nYA sYX / exists2 b, b \in B^# & 'C[b] = X.
  move=> IH; have nYB := subset_trans sBA nYA.
  rewrite -(coprime_abelian_gen_cent1 cBB _ nYB); last first.
  - by rewrite coprime_sym (pnat_coprime pB).
  - apply: contraL dimB2 => /cyclicP[x defB].
    have Bx: x \in B by rewrite defB cycle_id.
    rewrite defB -orderE (abelem_order_p abelB Bx) ?(pfactorK 1) //.
    by rewrite -cycle_eq1 -defB.
  rewrite gen_subG; apply/bigcupsP=> b B'b.
  have [ntb Bb]:= setD1P B'b; have sYbY: 'C_Y[b] \subset Y := subsetIl _ _.
  have{IH} sYbKb: 'C_Y[b] \subset 'O_p^'('C[b]).
    rewrite IH ?(pgroupS sYbY) ?subsetIr //; last by exists b.
    by rewrite normsI // ?normsG ?cBA.
  have{sYbKb} sYbKXb: 'C_Y[b] \subset 'O_p^'('C_X(<[b]>)).
    apply: subset_trans (pcoreS _ (subsetIr _ _)).
    by rewrite /= cent_gen cent_set1 subsetI setSI.
  rewrite (subset_trans sYbKXb) // p'core_cent_pgroup ?mFT_sol //.
  rewrite /psubgroup ?(pgroupS _ pB) cycle_subG //.
  by rewrite (subsetP sAX) ?(subsetP sBA).
wlog Zb: b X Y defX B'b p'Y nYA sYX / b \in Z.
  move=> IH; case Zb: (b \in Z); first exact: IH Zb.
  case/setD1P: B'b => ntb Bb; have solX := solCB b ntb; rewrite defX in solX.
  case: sBZ => [sBZ | [oZ sZB]]; first by rewrite (subsetP sBZ) in Zb.
  have defB: Z * <[b]> = B.
    apply/eqP; rewrite eqEcard mulG_subG sZB cycle_subG Bb.
    have obp := abelem_order_p abelB Bb ntb.
    rewrite (card_pgroup pB) /= (eqP dimB2) TI_cardMg -/#[_] ?oZ ?obp //.
    rewrite -obp in p_pr; case: (prime_subgroupVti [group of Z] p_pr) => //.
    by rewrite cycle_subG Zb.
  pose P1 := P :&: X; have sP1P: P1 \subset P := subsetIl _ _.
  have pP1 := pgroupS sP1P pP.
  have [P2 sylP2 sP12] := Sylow_superset (subsetIr _ _) pP1.
  have defP1: P1 = 'C_P(B).
    rewrite -defB centM /= -/Z setIA /cycle cent_gen cent_set1 defX.
    by rewrite [P :&: _](setIidPl _) // centsC (subset_trans sZ_ZP) ?subsetIr.
  have dimPP1: logn p #|P : P1| <= 1.
    by rewrite defP1 logn_quotient_cent_abelem ?normal_norm ?(eqP dimB2).
  have{dimPP1} nsP12: P1 <| P2.
    have pP2 := pHall_pgroup sylP2.
    have: logn p #|P2 : P1| <= 1.
      apply: leq_trans dimPP1; rewrite dvdn_leq_log //.
      rewrite -(dvdn_pmul2l (cardG_gt0 [group of P1])) !Lagrange ?subsetIl //.
      rewrite -(part_pnat_id pP2) (card_Hall sylP).
      by rewrite partn_dvd ?cardSg ?subsetT.
    rewrite -(pfactorK 1 p_pr) -pfactor_dvdn ?prime_gt0 // -p_part.
    rewrite part_pnat_id ?(pnat_dvd (dvdn_indexg _ _)) //=.
    case: (primeP p_pr) => _ dv_p; move/dv_p=> {dv_p}.
    case/pred2P=> oP21; first by rewrite -(index1g sP12 oP21) normal_refl.
    by rewrite (p_maximal_normal pP2) ?p_index_maximal ?oP21.
  have nsZP1_2: 'Z(P1) <| P2 by rewrite gFnormal_trans.
  have sZKp: Z \subset 'O_{p^', p}(X).
    suff: 'Z(P1) \subset 'O_{p^', p}(X).
      apply: subset_trans; rewrite subsetI {1}defP1 (subset_trans sZB).
        by rewrite (subset_trans sZ_ZP) ?subIset // orbC centS.
      by rewrite subsetI normal_sub.
    apply: odd_p_abelian_constrained sylP2 (center_abelian _) nsZP1_2 => //.
    exact: mFT_odd.
  have coYZ: coprime #|Y| #|Z|.
    by rewrite oZ coprime_sym (pnat_coprime _ p'Y) ?pnatE ?inE.
  have nYZ := subset_trans sZA nYA.
  have <-: [~: Y, Z] * 'C_Y(Z) = Y.
    exact: coprime_cent_prod (solvableS sYX solX).
  set K := 'O_p^'(X); have [nKY nKZ]: Y \subset 'N(K) /\ Z \subset 'N(K).
    by rewrite !gFnorm_trans ?(subset_trans sZA) ?normsG // -defX cBA.
  rewrite mul_subG //.
    have coYZK: coprime #|Y / K| #|'O_p(X / K)|.
      by rewrite coprime_sym coprime_morphr ?(pnat_coprime (pcore_pgroup _ _)).
    rewrite -quotient_sub1 ?comm_subG // -(coprime_TIg coYZK) subsetI.
    rewrite /= -quotient_pseries2 !quotientS ?commg_subl //.
    by rewrite (subset_trans (commgSS sYX sZKp)) ?commg_subr //= gFnorm.
  have: 'O_p^'('C_X(Z)) \subset K.
    rewrite p'core_cent_pgroup // /psubgroup /pgroup oZ pnat_id //.
    by rewrite -defX (subset_trans sZA) ?cBA.
  apply: subset_trans; apply: subset_trans (pcoreS _ (subsetIr _ _)).
  have: cyclic Z by rewrite prime_cyclic ?oZ.
  case/cyclicP=> z defZ; have Zz: z \in Z by rewrite defZ cycle_id.
  rewrite subsetI setSI //= (IH z) ?subsetIr ?(pgroupS (subsetIl _ _)) //.
  - by rewrite defZ /= cent_gen cent_set1.
  - rewrite !inE -cycle_eq1 -defZ trivg_card_le1 oZ -ltnNge prime_gt1 //=.
    by rewrite (subsetP sZB).
  by rewrite normsI // norms_cent // cents_norm // centsC (subset_trans sZA).
set K := 'O_p^'(X); have nsKX: K <| X by apply: pcore_normal.
case/setD1P: B'b => ntb Bb.
have [sAX solX]: A \subset X /\ solvable X by rewrite -defX cBA ?solCB.
have sPX: P \subset X.
  by rewrite -defX -cent_set1 centsC sub1set; case/setIP: (subsetP sZ_ZP b Zb).
have [nKA nKY nKP]: [/\ A \subset 'N(K), Y \subset 'N(K) & P \subset 'N(K)].
  by rewrite !(subset_trans _ (normal_norm nsKX)).
have sylPX: p.-Sylow(X) P by apply: pHall_subl (subsetT _) sylP.
have sAKb: A \subset 'O_{p^', p}(X).
  exact: (odd_p_abelian_constrained (mFT_odd _)) abA nsAP.
have coYZK: coprime #|Y / K| #|'O_p(X / K)|.
  by rewrite coprime_sym coprime_morphr ?(pnat_coprime (pcore_pgroup _ _)).
have cYAq: A / K \subset 'C_('O_p(X / K))(Y / K).
  rewrite subsetI -quotient_pseries2 quotientS //= (sameP commG1P trivgP).
  rewrite /= -quotientR // -(coprime_TIg coYZK) subsetI /= -quotient_pseries2.
  rewrite !quotientS ?commg_subr // (subset_trans (commgSS sAKb sYX)) //.
  by rewrite commg_subl /= gFnorm.
have cYKq: Y / K \subset 'C('O_p(X / K)).
  apply: coprime_nil_faithful_cent_stab => /=.
  - by rewrite gFnorm_trans ?normsG ?quotientS.
  - by rewrite coprime_sym.
  - exact: pgroup_nil (pcore_pgroup _ _).
  apply: subset_trans (cYAq); rewrite -defCA -['C_P(A) / K](morphim_restrm nKP).
  rewrite injm_cent ?ker_restrm ?ker_coset ?morphim_restrm -?quotientE //.
    rewrite setIid (setIidPr sAP) setISS ?centS //.
    by rewrite pcore_sub_Hall ?morphim_pHall.
  by rewrite coprime_TIg ?(pnat_coprime _ (pcore_pgroup _ _)).
rewrite -quotient_sub1 //= -/K -(coprime_TIg coYZK) subsetI subxx /=.
rewrite -Fitting_eq_pcore ?trivg_pcore_quotient // in cYKq *.
apply: subset_trans (cent_sub_Fitting (quotient_sol _ solX)).
by rewrite subsetI quotientS.
Qed.

(* This is B & G, Theorem 7.6 (the Thompson Transitivity Theorem). *)
Theorem Thompson_transitivity p q A :
    A \in 'SCN_3[p] -> q \in p^' ->
  [transitive 'O_p^'('C(A)), on |/|*(A; q) | 'JG].
Proof.
case/bigcupP=> P; rewrite 2!inE => sylP /andP[SCN_A mA3].
have [defZ def_pi']: 'Z(A) = A /\ \pi(A)^' =i p^'.
  rewrite inE -andbA in SCN_A; case/and3P: SCN_A => sAP _ /eqP defCA.
  case: (eqsVneq A 1) mA3 => /= [-> | ntA _].
    rewrite /rank big1_seq // => p1 _; rewrite /p_rank big1 // => E.
    by rewrite inE; case/andP; move/trivgP->; rewrite cards1 logn1.
  have [p_pr _ [k ->]] := pgroup_pdiv (pgroupS sAP (pHall_pgroup sylP)) ntA.
  split=> [|p1]; last by rewrite !inE primes_exp // primes_prime ?inE.
  by apply/eqP; rewrite eqEsubset subsetIl subsetI subxx -{1}defCA subsetIr.
rewrite -(eq_pcore _ def_pi') -def_pi' => pi'q.
apply: normed_constrained_rank3_trans; rewrite ?defZ //.
by apply: SCN_normed_constrained sylP _; rewrite inE SCN_A ltnW.
Qed.

End Seven.