proposition: Theorem sigma_group_trans M p X : M \in 'M -> p \in \sigma(M) -> p.-group X -> [/\ forall g, X \subset M -> X :^ g \subset M -> exists2 c, c \in 'C(X) & exists2 m, m \in M & g = c * m, [transitive 'C(X), on [set Mg in M :^: G | X \subset Mg] | 'Js ] & X \subset M -> 'C(X) * 'N_M(X) = 'N(X)].
proof: 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.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype) mathcomp(bigop finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9)