proposition: Lemma FTtypeII_ker_TI M : M \in 'M -> FTtype M == 2%N -> [/\ normedTI 'A0(M) G M, normedTI 'A(M) G M & normedTI 'A1(M) G M].
proof: Proof. move=> maxM typeM; have [sA1A sAA0] := (FTsupp1_sub maxM, FTsupp_sub0 M). have [sA10 sA0M] := (subset_trans sA1A sAA0, FTsupp0_sub M). have nzA1: 'A1(M) != set0 by rewrite setD_eq0 def_FTcore ?subG1 ?Msigma_neq1. have [nzA nzA0] := (subset_neq0 sA1A nzA1, subset_neq0 sA10 nzA1). suffices nTI_A0: normedTI 'A0(M) G M. by rewrite nTI_A0 !(normedTI_S _ _ _ nTI_A0) // ?FTsupp_norm ?FTsupp1_norm. have [U W W1 W2 defW [[MtypeP _ _ tiFM] _ _ _ _]] := FTtypeP 2 maxM typeM. apply/(Dade_normedTI_P (FT_Dade0_hyp maxM)); split=> // x A0x. rewrite /= def_FTsignalizer0 /'R_M //=; have [// | not_sCxM] := ifPn. have [y cxy /negP[]] := subsetPn not_sCxM. apply: subsetP cxy; rewrite -['C[x]]setTI (cent1_normedTI tiFM) //. have /setD1P[ntx Ms_x]: x \in 'A1(M). by have [_ [/subsetP-> // ]] := FTsupport_facts maxM; apply/setIdP. rewrite !inE ntx (subsetP (Fcore_sub_Fitting M)) //. by rewrite (Fcore_eq_FTcore _ _) ?(eqP typeM). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection10) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5)