proposition: Lemma FTtypeII_support_facts T L (Q := T`_\F) (H := L`_\F) : FTtype S == 2%N -> typeP_pair S T defW -> L \in 'M('N(U)) -> [/\ [Frobenius L with kernel H], U \subset H & H ><| W1 = L \/ (exists2 y, y \in Q & H ><| (W1 <*> W2 :^ y) = L)].
proof: Proof. move=> Stype2 pairST /setIdP[maxL sNU_L]. have [pgt0 qgt0] := (ltnW (ltnW pgt2), ltnW (ltnW qgt2)). have [[_ _ maxT] _ _ _ allST] := pairST. have [[_ ntU _ _] _ not_sNU_S _ _] := compl_of_typeII maxS StypeP Stype2. have [[_ _ frobUW1 cUU] _ _ _ _] := Sfacts. have xdefW: W2 \x W1 = W by rewrite dprodC. have [V TtypeP] := typeP_pairW (typeP_pair_sym xdefW pairST). have [abelQ oQ]: q.-abelem Q /\ #|Q| = (q ^ p)%N. by have [] := FTtypeP_facts maxT TtypeP. have sUL: U \subset L := subset_trans (normG U) sNU_L. have [/mulG_sub[sPPU sUPU] sPUS] := (sdprodW defPU, der_sub 1 S). have nUW1: W1 \subset 'N(U) by have [_ []] := StypeP. have sW1L := subset_trans nUW1 sNU_L. have Ltype1: FTtype L == 1%N. apply: contraR not_sNU_S => /allST/setUP[]// /imsetP[y _ defL]. have hallU: \pi(U).-Hall(S) U. have /Hall_pi/(subHall_Hall _ (piSg sUPU)): Hall PU U. have /pHall_Hall:= pHall_subl sPPU sPUS (Fcore_Hall S). by rewrite (sdprod_Hall defPU). by apply; rewrite Hall_pi // -(coprime_sdprod_Hall_l defS). have hallUy: \pi(U).-Hall(S) (U :^ y^-1). by rewrite pHallE sub_conjgV -defL sUL /= cardJg -(card_Hall hallU). have [x /conjGid <- ->] := Hall_trans (mmax_sol maxS) hallU hallUy. by rewrite !normJ conjSg sub_conjgV -defL. have oH: #|H| = (q ^ p)%N by rewrite /H defL FcoreJ cardJg. have sW1H: W1 \subset H. rewrite (sub_normal_Hall (Fcore_Hall L)) ?gFnormal //=. by rewrite oH pi_of_exp ?prime_gt0 // pgroup_pi. have regUW1: 'C_U(W1) = 1%g := Frobenius_trivg_cent frobUW1. have /negP[] := ntU; rewrite -subG1 -regUW1 subsetIidl (sameP commG1P trivgP). have /coprime_TIg <-: coprime #|U| #|H|. by rewrite oH coprime_pexpr ?(coprimeSg sUPU). rewrite commg_subI //; last by rewrite subsetI sW1H. by rewrite subsetIidl (subset_trans sUL) ?gFnorm. have frobL := FTtype1_Frobenius maxL Ltype1. have solH: solvable H by rewrite nilpotent_sol ?Fcore_nil. have coHW1: coprime #|H| #|W1|. rewrite -(coprime_pexpr _ _ pgt0) -oQ. apply/(coprimegS (Fcore_sub_FTcore maxT))/(coprimeSg (Fcore_sub_FTcore maxL)). have [_ -> //] := FT_Dade_support_partition gT. have: FTtype T != 1%N := FTtypeP_neq1 maxT TtypeP. by apply: contra => /imsetP[y _ ->] /=; rewrite FTtypeJ. have tiHW1: H :&: W1 = 1%g := coprime_TIg coHW1. have sUH: U \subset H; last split=> //. have [ntH _ /andP[sHL nHL] regHL] := Frobenius_kerP frobL. have regHE E: gval E != 1%g -> E \subset L -> H :&: E = 1%g -> 'C_H(E) = 1%g. move=> ntE sEL tiHE; apply: contraNeq ntE => /trivgPn[x /setIP[Hx cEx] ntx]. rewrite -subG1 -tiHE subsetIidr (subset_trans _ (regHL x _)) ?inE ?ntx //. by rewrite subsetI sEL sub_cent1. suffices /trivgPn[x /setIP[Hx Ux] ntx]: H :&: U != 1%g. apply: subset_trans (regHL x _); last by rewrite !inE ntx. by rewrite subsetI sUL sub_cent1 (subsetP cUU). apply: contraNneq (ntH) => tiHU; rewrite trivg_card1. have [nHU nHW1] := (subset_trans sUL nHL, subset_trans sW1L nHL). have nHUW1: U <*> W1 \subset 'N(H) by rewrite join_subG nHU. have coHUW1: coprime #|H| #|U <*> W1|. have [/eqP defUW1 _] := andP frobUW1. rewrite (sdprodWY defUW1) -(sdprod_card defUW1) coprimeMr coHW1 andbT. have defHU: H ><| U = H <*> U by rewrite sdprodEY. rewrite (coprime_sdprod_Hall_l defHU). apply: pHall_Hall (pHall_subl (joing_subl _ _) _ (Fcore_Hall L)). by rewrite join_subG sHL. have [_ _] := Frobenius_Wielandt_fixpoint frobUW1 nHUW1 coHUW1 solH. by move->; rewrite regHE // cards1 exp1n. have [E sW1E frobHE]: exists2 E, W1 \subset gval E & [Frobenius L = H ><| E]. have [E frobHE] := existsP frobL; have [/eqP defL _] := andP frobHE. have hallE: \pi(H)^'.-Hall(L) E. by rewrite -(compl_pHall E (Fcore_Hall L)) sdprod_compl. have [|x Lx sW1Ex] := Hall_subJ (mmax_sol maxL) hallE sW1L. by rewrite /pgroup -coprime_pi' ?cardG_gt0. rewrite -(FrobeniusJ x) conjGid // (normsP (gFnorm _ _)) // in frobHE. by exists (E :^ x)%G. have [defL ntH ntE _ _] := Frobenius_context frobHE. have [_ sEL _ nHE _] := sdprod_context defL. have solE := solvableS sEL (mmax_sol maxL). have [regHE regEH] := (Frobenius_reg_ker frobHE, Frobenius_reg_compl frobHE). have qW1: q.-group W1 by apply: pnat_id. have cycEr (r : nat) R: r.-group R -> R \subset E -> cyclic R. move=> rR sRE; have nHR := subset_trans sRE nHE. apply: odd_regular_pgroup_cyclic rR (mFT_odd _) ntH nHR _. by move=> y /setD1P[nty Ry]; rewrite regHE // !inE nty (subsetP sRE). have /normal_norm nW1E: W1 <| E. exact: prime_odd_regular_normal (mFT_odd E) _ _ _ (Frobenius_reg_ker frobHE). have defNW1: Q ><| W2 = 'N(W1). by have [] := FTtypeP_norm_cent_compl maxT TtypeP. have [nsQN sW2N _ _ _] := sdprod_context defNW1. have sylQ: q.-Sylow('N(W1)) Q. rewrite /pHall normal_sub // abelem_pgroup //=. by rewrite -(index_sdprod defNW1) pnatE //= !inE eq_sym. have hallW2: q^'.-Hall('N(W1)) W2 by rewrite -(compl_pHall _ sylQ) sdprod_compl. pose Q1 := Q :&: E; have sylQ1: q.-Sylow(E) Q1 by apply: setI_normal_Hall nW1E. have defQ1: Q1 = W1. have abelQ1: q.-abelem Q1 := abelemS (subsetIl Q E) abelQ. have sW1Q: W1 \subset Q by have [_ _ _ []] := TtypeP. have sW1Q1: W1 \subset Q1 by apply/subsetIP. have ntQ1: Q1 != 1%g by apply: subG1_contra ntW1. apply/esym/eqP; rewrite eqEcard sW1Q1 (cyclic_abelem_prime abelQ1) //=. by rewrite (cycEr q) ?(pHall_pgroup sylQ1) ?subsetIr. have [P2 hallP2] := Hall_exists q^' solE; have [sP2E q'P2 _] := and3P hallP2. have defE: W1 ><| P2 = E. apply/(sdprod_normal_p'HallP _ hallP2); rewrite /= -defQ1 //. by rewrite /Q1 setIC norm_normalI // (subset_trans nW1E) ?normal_norm. have [P2_1 | ntP2] := eqsVneq P2 1%g. by left; rewrite -defE P2_1 sdprodg1 in defL. have solNW1: solvable 'N(W1). by rewrite mFT_sol ?mFT_norm_proper // mFT_sol_proper (solvableS sW1E). have [zy /=] := Hall_subJ solNW1 hallW2 (subset_trans sP2E nW1E) q'P2. rewrite -{1}(sdprodWC defNW1) => /mulsgP[z y W2z Qy ->{zy}]. rewrite conjsgM (conjGid W2z) {z W2z} => sP2W2y. right; exists y => //; congr (_ ><| _ = _): defL. rewrite -(sdprodWY defE); congr (W1 <*> _). by apply/eqP; rewrite eqEsubset sP2W2y prime_meetG ?cardJg ?(setIidPr _). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime binomial ssralg poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct center cyclic commutator gseries nilpotent) mathcomp(pgroup sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(ssrnum rat algC cyclotomic algnum) mathcomp(classfun character integral_char inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4) odd_order(PFsection5 PFsection6 PFsection7 PFsection8 PFsection9) odd_order(PFsection10 PFsection11 PFsection12)