proposition: Theorem BGsummaryE : [/\ forall M, M \in 'M -> #|class_support M^~~ G| = (#|M`_\sigma|.-1 * #|G : M|)%N, {in \pi(G), forall p, exists2 M : {group gT}, M \in 'M & p \in \sigma(M)} /\ {in 'M &, forall M H, gval H \notin M :^: G -> [predI \sigma(M) & \sigma(H)] =i pred0} & let PG := [set class_support M^~~ G | M : {group gT} in 'M] in [/\ partition PG (cover PG), 'M_'P = set0 :> {set {group gT}} -> cover PG = G^# & forall M K, M \in 'M_'P -> \kappa(M).-Hall(M) K -> let Kstar := 'C_(M`_\sigma)(K) in let Zhat := (K <*> Kstar) :\: (K :|: Kstar) in partition [set class_support Zhat G; cover PG] G^#]].
proof: Proof. split=> [||PG]; first exact: card_class_support_sigma. by split=> [p /sigma_mmax_exists[M]|]; [exists M | apply: sigma_partition]. have [noPmax | ntPmax] := eqVneq 'M_'P (set0 : {set {group gT}}). rewrite noPmax; move/eqP in noPmax; have [partPG _] := mFT_partition gT. have /and3P[/eqP-> _ _] := partPG noPmax; rewrite partPG //. by split=> // M K; rewrite inE. have [_ partZPG] := mFT_partition gT. have partPG: partition PG (cover PG). have [M PmaxM] := set0Pn _ ntPmax; have [maxM _] := setDP PmaxM. have [K hallK] := Hall_exists \kappa(M) (mmax_sol maxM). have{partZPG} [/and3P[_ tiPG]] := partZPG M K PmaxM hallK. rewrite inE => /norP[_ notPGset0] _; apply/and3P; split=> //; apply/trivIsetP. by apply: sub_in2 (trivIsetP tiPG) => C; apply: setU1r. split=> // [noPmax | M K PmaxM hallK]; first by case/eqP: ntPmax. have [/=] := partZPG M K PmaxM hallK; rewrite -/PG; set Z := class_support _ G. case/and3P=> /eqP defG1 tiZPG; rewrite 2!inE => /norP[nzZ _] notPGZ. have [_ tiPG nzPG] := and3P partPG; have [maxM _] := setDP PmaxM. rewrite /cover big_setU1 //= -/(cover PG) in defG1. rewrite /trivIset /cover !big_setU1 //= (eqnP tiPG) -/(cover PG) in tiZPG. have tiZ_PG: Z :&: cover PG = set0. by apply/eqP; rewrite setI_eq0 -leq_card_setU eq_sym. have notUPGZ: Z \notin [set cover PG]. by rewrite inE; apply: contraNneq nzZ => defZ; rewrite -tiZ_PG -defZ setIid. rewrite /partition /trivIset /(cover _) !big_setU1 // !big_set1 /= -defG1. rewrite eqxx tiZPG !inE negb_or nzZ /= eq_sym; apply: contraNneq nzPG => PG0. apply/imsetP; exists M => //; apply/eqP; rewrite eq_sym -subset0 -PG0. by rewrite (bigcup_max (class_support M^~~ G)) //; apply: imset_f. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype) mathcomp(bigop finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall frobenius) odd_order(BGsection1 BGsection2 BGsection3 BGsection4 BGsection5) odd_order(BGsection6 BGsection7 BGsection9 BGsection10 BGsection12) odd_order(BGsection13 BGsection14 BGsection15)