proposition: Lemma FTtypeP_norm_cent_compl : P ><| W1 = 'N(W2) /\ P ><| W1 = 'C(W2).
proof: Proof. have [/mulG_sub[_ sW1S] /mulG_sub[sPPU sUPU]] := (sdprodW defS, sdprodW defPU). have nPW1: W1 \subset 'N(P) by rewrite (subset_trans sW1S) ?gFnorm. have [[_ _ frobUW1 cUU] [abelP _] _ _ _] := Sfacts. have [pP cPP _] := and3P abelP; have [_ _ cW12 tiW12] := dprodP defW. have cW2P: P \subset 'C(W2) by rewrite sub_abelian_cent. suffices sNPW2: 'N(W2) \subset P <*> W1. have cW2PW1: P <*> W1 \subset 'C(W2) by rewrite join_subG cW2P centsC. rewrite sdprodEY ?coprime_TIg ?(coprimeSg sPPU) //. split; apply/eqP; rewrite eqEsubset ?(subset_trans cW2PW1) ?cent_sub //. by rewrite (subset_trans (cent_sub _)). have tiP: normedTI P^# G S. have [_ _ _] := compl_of_typeII_IV maxS StypeP notStype5. by rewrite -defH FTtypeP_reg_Fcore dprodg1. have ->: 'N(W2) = 'N_S(W2). apply/esym/setIidPr/subsetP=> y nW2y; have [x W2x ntx] := trivgPn _ ntW2. have [_ _ tiP_J] := normedTI_memJ_P tiP. by rewrite -(tiP_J x) ?inE ?conjg_eq1 // ntx (subsetP sW2P) ?memJ_norm. rewrite -{1}(sdprodW defS) setIC -group_modr ?cents_norm 1?centsC //=. rewrite mulG_subG joing_subr /= -(sdprodW defPU) setIC. rewrite -group_modl ?cents_norm //= mulG_subG joing_subl /= andbT. set K := 'N_U(W2); have sKPU: K \subset PU by rewrite subIset ?sUPU. have{sKPU} nPKW1: K <*> W1 \subset 'N(P). by rewrite gFnorm_trans ?normsG // -(sdprodWY defS) genS ?setSU. have nW2KW1: K <*> W1 \subset 'N(W2). by rewrite join_subG subsetIr cents_norm // centsC. have coPKW1: coprime #|P| #|K <*> W1|. by rewrite (coprimegS _ (Ptype_Fcore_coprime StypeP)) ?genS ?setSU ?subsetIl. have p'KW1: p^'.-group (K <*> W1). by rewrite /pgroup p'natE // -prime_coprime ?(coprimeSg sW2P). have [Q1 defP nQ1KW1] := Maschke_abelem abelP p'KW1 sW2P nPKW1 nW2KW1. have [-> | ntK] := eqVneq K 1%g; first by rewrite sub1G. have frobKW1: [Frobenius K <*> W1 = K ><| W1]. apply: Frobenius_subl frobUW1; rewrite ?subsetIl //. rewrite normsI ?norms_norm //; first by have [_ []] := StypeP. by rewrite cents_norm // centsC. have regQ1W1: 'C_Q1(W1) = 1%g. have [_ /mulG_sub[_ /setIidPl defQ1] _ tiW2Q1] := dprodP defP. by rewrite -defQ1 -setIA (typeP_cent_core_compl StypeP) setIC. have cQ1K: K \subset 'C(Q1). have /mulG_sub[_ sQ1P] := dprodW defP; have coQ1KW1 := coprimeSg sQ1P coPKW1. have solQ1 := solvableS sQ1P (abelian_sol cPP). by have [_ ->] := Frobenius_Wielandt_fixpoint frobKW1 nQ1KW1 coQ1KW1 solQ1. have /subsetIP[_ cW1K]: K \subset 'C_(K <*> W1)(W2). have cCW1: W1 \subset 'C_(K <*> W1)(W2) by rewrite subsetI joing_subr centsC. apply: contraR ntW1 => /(Frobenius_normal_proper_ker frobKW1) ltCK. rewrite -subG1; have [/eqP/sdprodP[_ _ _ <-] _] := andP frobKW1. rewrite subsetIidr (subset_trans cCW1) // proper_sub //. rewrite ltCK //; last by rewrite norm_normalI ?norms_cent. by rewrite (solvableS _ (abelian_sol cUU)) ?subsetIl. case/negP: ntK; rewrite -subG1 -FTtypeP_reg_Fcore subsetI subsetIl /=. by rewrite -(dprodW defP) centM subsetI cW1K. 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)