proposition: Theorem FT_Dade_support_partition : [/\ \pi(G) =i [pred p | [exists M : {group gT} in 'M, p \in \pi(M`_\s)]], {in 'M &, forall M L, gval L \notin M :^: G -> coprime #|M`_\s| #|L`_\s| }, {in 'M, forall M, #|'A1~(M)| = (#|M`_\s|.-1 * #|G : M|)%N} & let PG := [set 'A1~(Mi) | Mi : {group gT} in 'M^G] in [/\ {in 'M^G &, injective (fun M => 'A1~(M))}, all_FTtype1 -> partition PG G^# & forall S T W W1 W2 (defW : W1 \x W2 = W), let VG := class_support (cyclicTIset defW) G in typeP_pair S T defW -> partition (VG |: PG) G^# /\ VG \notin PG]].
proof: Proof. have defDsup M: M \in 'M -> class_support M^~~ G = 'A1~(M). move=> maxM; rewrite class_supportEr /'A1~(M) /'A1(M) def_FTcore //. rewrite -(eq_bigr _ (fun _ _ => bigcupJ _ _ _ _)) exchange_big /=. apply: eq_bigr => x Ms_x; rewrite -class_supportEr. rewrite -norm_rlcoset ?(subsetP (cent_sub _)) ?cent_FT_signalizer //=. congr (class_support (_ :* x) G); rewrite /'R_M. have [_ _ /(_ x Ms_x)[_ defCx _] /(_ x Ms_x)defNF]:= BGsummaryD maxM. have [sCxM | /defNF[[_ <-]] //] := ifPn. apply/eqP; rewrite trivg_card1 -(eqn_pmul2r (cardG_gt0 'C_M[x])). by rewrite (sdprod_card defCx) mul1n /= (setIidPr _). have [b [a1 a2] [/and3P[_ _ not_PG_set0] _ _]] := BGsummaryE gT. split=> [p | M L maxM maxL /a2 | M maxM | {b a1 a2}PG]. - apply/idP/exists_inP=> [/a1[M maxM sMp] | [M _]]. by exists M => //; rewrite def_FTcore // pi_Msigma. exact: piSg (subsetT _) p. - move/(_ maxM maxL)=> coML; rewrite coprime_pi' // !def_FTcore //. apply: sub_pgroup (pcore_pgroup _ L) => p; apply/implyP. by rewrite implybN /= pi_Msigma // implybE -negb_and [_ && _]coML. - by rewrite -defDsup // def_FTcore // b. have [/subsetP sMG_M _ injMG sM_MG] := mmax_transversalP gT. have{PG} ->: PG = [set class_support M^~~ G | M : {group gT} in 'M]. apply/setP=> AG; apply/imsetP/imsetP=> [] [M maxM ->]. by move/sMG_M in maxM; exists M; rewrite ?defDsup //. have [x MG_Mx] := sM_MG M maxM. by exists (M :^ x)%G; rewrite // defDsup ?mmaxJ ?FT_Dade1_supportJ. have [c1 c2] := mFT_partition gT. split=> [M H maxM maxH eq_MH | Gtype1 | S T W W1 W2 defW VG pairST]. - apply: injMG => //; move/sMG_M in maxM; move/sMG_M in maxH. apply/orbit_eqP/idPn => not_HG_M. have /negP[]: ~~ [disjoint 'A1~(M) & 'A1~(H)]. rewrite eq_MH -setI_eq0 setIid -defDsup //. by apply: contraNneq not_PG_set0 => <-; apply: imset_f. rewrite -!defDsup // -setI_eq0 class_supportEr big_distrl -subset0. apply/bigcupsP=> x /class_supportGidr <- /=; rewrite -conjIg sub_conjg conj0g. rewrite class_supportEr big_distrr /=; apply/bigcupsP=> {}x _. rewrite subset0 setI_eq0 -sigma_supportJ sigma_support_disjoint ?mmaxJ //. by rewrite (orbit_transl _ (mem_orbit _ _ _)) ?in_setT // orbit_sym. - rewrite c1 // setD_eq0; apply/subsetP=> M maxM. by rewrite FTtype_Fmax ?(forall_inP Gtype1). have [[[cycW maxS _] _ _ _ _] [U_S StypeP]] := (pairST, typeP_pairW pairST). have Stype'1 := FTtypeP_neq1 maxS StypeP. have maxP_S: S \in TypeP_maxgroups _ by rewrite FTtype_Pmax. have hallW1: \kappa(S).-Hall(S) W1. have [[U1 K] /= complU1] := kappa_witness maxS. have ntK: K :!=: 1%g by rewrite -(trivgPmax maxS complU1). have [[defS_K _ _] [//|defS' _] _ _ _] := kappa_structure maxS complU1. rewrite {}defS' in defS_K. have /imsetP[x Sx defK] := of_typeP_compl_conj StypeP defS_K. by have [_ hallK _] := complU1; rewrite defK pHallJ in hallK. have{cycW} [[ntW1 ntW2] [cycW _ _]] := (cycTI_nontrivial cycW, cycW). suffices defW2: 'C_(S`_\sigma)(W1) = W2. by have [] := c2 _ _ maxP_S hallW1; rewrite defW2 /= (dprodWY defW). have [U1 complU1] := ex_kappa_compl maxS hallW1. have [[_ [_ _ sW2'F] _] _ _ _] := BGsummaryC maxS complU1 ntW1. rewrite -(setIidPr sW2'F) setIA (setIidPl (Fcore_sub_Msigma maxS)). exact: typeP_cent_core_compl StypeP. 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)