proposition: Lemma FTtype34_facts (H' := H^`(1)%g): [/\ p.-group H, U \subset 'C(H0), H0 :=: H' & C :=: U'].
proof: Proof. have nilH: nilpotent H := Fcore_nil M. have /sdprod_context[/andP[_ nHM] sUW1M _ _ _] := Ptype_Fcore_sdprod MtypeP. have coH_UW1: coprime #|H| #|U <*> W1| := Ptype_Fcore_coprime MtypeP. have [[_ mulHU _ tiHU] [nHU isomHU]] := (sdprodP defHU, sdprod_isom defHU). have{sUW1M} cH0U: U \subset 'C(H0). have frobUW1 := Ptype_compl_Frobenius maxM MtypeP notMtype5. have nH0_UW1 := subset_trans sUW1M nH0M; have [_ nH0W1] := joing_subP nH0_UW1. have [coH0_UW1 solH0] := (coprimeSg sH0H coH_UW1, solvableS sH0H solH). have [_ -> //] := Frobenius_Wielandt_fixpoint frobUW1 nH0_UW1 coH0_UW1 solH0. have ->: 'C_H0(W1) = H0 :&: 'C_H(W1) by rewrite setIA (setIidPl sH0H). have nH0C: 'C_H(W1) \subset 'N(H0) by rewrite subIset // normal_norm. rewrite cardMg_TI // -LagrangeMl -card_quotient {nH0C}//. rewrite coprime_quotient_cent ?(coprimeSg sHHU) //=. have [_ -> _] := Ptype_Fcore_factor_facts maxM MtypeP notMtype5. by rewrite (typeP_cent_core_compl MtypeP) def_p. have{isomHU} defC: C :=: U'. have [injHquo defHUb] := isomP isomHU. apply: (injm_morphim_inj injHquo); rewrite ?subsetIl ?morphim_der ?der_sub //. rewrite defHUb morphim_restrm -quotientE setIA setIid -quotientMidl /=. by rewrite (dprodW defHC) -defM'' -quotient_der // -mulHU mul_subG ?normG. have{coH_UW1} defH0: H0 :=: H'. pose Hhat := (H / H')%g; pose Uhat := (U / H')%g; pose HUhat := (HU / H')%g. have nH'H: H \subset 'N(H') by apply: gFnorm. have nH'U: U \subset 'N(H') by apply: gFnorm_trans. apply/eqP; rewrite eqEsubset andbC. rewrite der1_min ?(abelem_abelian abelHbar) ?normal_norm //=. rewrite -quotient_sub1 /= -/H'; last exact: subset_trans sH0H nH'H. suffices <-: 'C_Hhat(Uhat) = 1%g. by rewrite subsetI quotientS //= quotient_cents // centsC. suffices: ~~ ('C_Hhat(Uhat)^`(1)%g \proper 'C_Hhat(Uhat)). exact: contraNeq (sol_der1_proper (quotient_sol _ solH) (subsetIl Hhat _)). have {2}<-: HUhat^`(1)%g :&: 'C_Hhat(Uhat) = 'C_Hhat(Uhat). rewrite -quotient_der ?[HU^`(1)%g]defM''; last by rewrite -mulHU mul_subG. by rewrite (setIidPr _) ?subIset // quotientS ?joing_subl. suffices defHUhat: 'C_Hhat(Uhat) \x ([~: Hhat, Uhat] <*> Uhat) = HUhat. rewrite -(dprod_modl (der_dprod 1 defHUhat)) ?der_sub //= -/Hhat. rewrite [rhs in _ \x rhs](trivgP _) ?dprodg1 ?properxx //= -/Hhat. by have [_ _ _ <-] := dprodP defHUhat; rewrite setIC setIS ?der_sub. have coHUhat: coprime #|Hhat| #|Uhat|. by rewrite coprime_morph ?(coprimegS _ coH_UW1) ?joing_subl. have defHhat: 'C_Hhat(Uhat) \x [~: Hhat, Uhat] = Hhat. by rewrite dprodC coprime_abelian_cent_dprod ?der_abelian ?quotient_norms. rewrite /HUhat -(sdprodWY defHU) quotientY //= -(dprodWY defHhat). have [_ _ cCRhat tiCRhat] := dprodP defHhat. rewrite dprodEY ?joingA //; first by rewrite join_subG cCRhat centsC subsetIr. apply/trivgP; rewrite /= joingC norm_joinEl ?commg_normr //= -/Hhat -/Uhat. rewrite -tiCRhat !(setIAC _ 'C(_)) setSI // subsetI subsetIl /=. by rewrite -group_modr ?commg_subl ?quotient_norms //= coprime_TIg ?mul1g. suffices{defC defH0}: p.-group H by []. pose R := 'O_p^'(H); have hallR: p^'.-Hall(H) R := nilpotent_pcore_Hall _ nilH. have defRHp: R \x 'O_p(H) = H by rewrite dprodC nilpotent_pcoreC. suffices R_1: R :=: 1%g by rewrite -defRHp R_1 dprod1g pcore_pgroup. have /subsetIP[sRH cUR]: R \subset 'C_H(U). have oH: #|H| = (p ^ q * #|'C_H(U)|)%N. by have:= typeII_IV_core maxM MtypeP notMtype5 => /=; rewrite ifN => // -[]. apply/setIidPl/eqP; rewrite eqEcard subsetIl /= (card_Hall hallR) {}oH. rewrite (card_Hall (setI_normal_Hall _ hallR _)) ?subsetIl ?gFnormal //. rewrite partnM ?expn_gt0 ?cardG_gt0 //= part_p'nat ?mul1n ?pnatNK //. by rewrite pnatX ?pnat_id. suffices: ~~ (R^`(1)%g \proper R) by apply: contraNeq (sol_der1_proper solH _). have /setIidPr {2}<-: R \subset HU^`(1)%g. by rewrite [HU^`(1)%g]defM'' -(dprodWY defHC) sub_gen ?subsetU ?sRH. suffices defRHpU: R \x ('O_p(H) <*> U) = HU. rewrite -(dprod_modl (der_dprod 1 defRHpU)) ?der_sub //= -/R setIC. rewrite [rhs in _ \x rhs](trivgP _) ?dprodg1 ?properxx //= -/R. by have /dprodP[_ _ _ <-] := defRHpU; rewrite setIS ?der_sub. rewrite -(sdprodWY defHU) -[in RHS](dprodWY defRHp) -joingA. have [_ _ cRHp tiRHp] := dprodP defRHp. rewrite dprodEY //= -/R; first by rewrite join_subG cRHp centsC. rewrite joingC norm_joinEl 1?gFnorm_trans //. by rewrite -(setIidPl sRH) -setIA -group_modr ?gFsub // tiHU mul1g. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator gseries nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection15 BGsection16) mathcomp(ssrnum ssrint algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5) odd_order(PFsection6 PFsection7 PFsection8 PFsection9 PFsection10)