proposition: Lemma FTtypeI_II_facts n (H := M`_\F) : FTtype M == n -> H ><| U = M ^`(n.-1)%g -> if 0 < n <= 2 then [/\ forall p S, p.-Sylow(U) S -> abelian S /\ ('r(S) <= 2)%N, forall X, X != set0 -> X \subset U^# -> 'C_H(X) != 1%g -> 'M('C(X)) = [set M] & let B := 'A(M) :\: 'A1(M) in B != set0 -> normedTI B G M ] else True.
proof: Proof. move=> typeM defMn; have [n12 | //] := ifP; rewrite -mem_iota !inE in n12. have defH: H = M`_\sigma. by rewrite -def_FTcore -?(Fcore_eq_FTcore _ _) // (eqP typeM) !inE orbA n12. have [K complU]: exists K : {group gT}, kappa_complement M U K. have [[V K] /= complV] := kappa_witness maxM. have [[hallV hallK gVK] [_ sUMn _ _ _]] := (complV, sdprod_context defMn). have hallU: \sigma_kappa(M)^'.-Hall(M) U. rewrite pHallE -(card_Hall hallV) (subset_trans sUMn) ?der_sub //=. rewrite -(@eqn_pmul2l #|H|) ?cardG_gt0 // (sdprod_card defMn) defH. rewrite (sdprod_card (sdprod_FTder maxM complV)) (eqP typeM). by case/pred2P: n12 => ->. have [x Mx defU] := Hall_trans (mmax_sol maxM) hallU hallV. exists (K :^ x)%G; split; rewrite ?pHallJ // defU -conjsMg. by rewrite -(gen_set_id gVK) groupP. have [part_a _ _ [part_b part_c]] := BGsummaryB maxM complU. rewrite eqEsubset FTsupp1_sub // andbT -setD_eq0 in part_c. split=> // X notX0 /subsetD1P[sXU notX1]; rewrite -cent_gen defH. apply: part_b; rewrite -?subG1 ?gen_subG //. by rewrite -setD_eq0 setDE (setIidPl _) // subsetC sub1set inE. 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)