proposition: Lemma FTprTIsign j : delta_ j = 1.
proof: Proof. have [[_ _ frobUW1 cUU] _ _ cohS _] := FTtypeP_facts. have [-> | nz_j] := eqVneq j 0; first exact: prTIsign0. suffices: (1 == delta_ j %[mod q])%C. rewrite signrE /eqCmod addrC opprB subrK dvdC_nat. by case: (Idelta j); rewrite ?subr0 // gtnNdvd. apply: eqCmod_trans (prTIirr1_mod ptiWS 0 j); rewrite -/(mu2_ 0 j) -/q. have ->: mu2_ 0 j 1%g = u%:R. by apply: (mulfI (neq0CG W1)); rewrite -prTIred_1 -/mu_ mu1uq // mulnC natrM. rewrite eqCmod_sym /eqCmod -(@natrB _ u 1) ?indexg_gt0 // subn1 dvdC_nat. have nC_UW1: U <*> W1 \subset 'N(C). have /sdprodP[_ _ nPUW1 _] := Ptype_Fcore_sdprod StypeP. by rewrite normsI ?norms_cent // join_subG normG; have [_ []] := StypeP. have coUq: coprime #|U| q by have /sdprod_context[_ /coprimeSg->] := defPU. have /Frobenius_dvd_ker1: [Frobenius U <*> W1 / C = (U / C) ><| (W1 / C)]. have [defUW1 _ _ _ _] := Frobenius_context frobUW1. rewrite Frobenius_coprime_quotient // /normal ?subIset ?joing_subl //. split=> [|x /(Frobenius_reg_ker frobUW1)->]; last exact: sub1G. rewrite properEneq subsetIl -CHbar_C andbT. by have [] := Ptype_Fcore_factor_facts maxS StypeP notStype5. have [nCU nCW1] := joing_subP nC_UW1; rewrite !card_quotient // -/u. by rewrite -indexgI setIC setIAC (coprime_TIg coUq) setI1g indexg1. 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)