proposition: Corollary mFT_partition : let Pcover := [set class_support M^~~ G | M : {group gT} in 'M] in [/\ 'M_'P == set0 :> {set {group gT}} -> partition Pcover G^# & forall M K, M \in 'M_'P -> \kappa(M).-Hall(M) K -> let Ks := 'C_(M `_\sigma)(K) in let Z := K <*> Ks in let Zhat := Z :\: (K :|: Ks) in let ClZhat := class_support Zhat G in partition (ClZhat |: Pcover) G^# /\ ClZhat \notin Pcover].
proof: Proof. move=> Pcover; have notPcover0: set0 \notin Pcover. apply/imsetP=> [[M maxM]]; apply/eqP; rewrite eq_sym; apply/set0Pn. have [x Ms_x ntx] := trivgPn _ (Msigma_neq1 maxM); exists x. rewrite class_supportEl; apply/bigcupP; exists x; last exact: class_refl. by apply/bigcupP; exists x; [apply/setD1P | apply: lcoset_refl]. have tiPcover: trivIset Pcover. apply/trivIsetP=> _ _ /imsetP[M maxM ->] /imsetP[H maxH ->] notMGH. rewrite -setI_eq0 !{1}class_supportEr big_distrr big1 //= => a Ga. rewrite big_distrl big1 //= => b Gb; apply/eqP. rewrite -!{1}sigma_supportJ setI_eq0 sigma_support_disjoint ?mmaxJ //. apply: contra notMGH; rewrite {a Ga}(orbit_transl _ (mem_orbit _ _ Ga)). rewrite {b Gb}(orbit_eqP (mem_orbit _ _ Gb))=> /imsetP[c Gc ->] /=. by rewrite sigma_supportJ class_supportGidl. have ntPcover: cover Pcover \subset G^#. apply/bigcupsP=> _ /imsetP[M maxM ->]; rewrite class_supportEr. apply/bigcupsP=> a _; rewrite subsetD1 subsetT mem_conjg conj1g {a}//=. move/ell_sigma0P: (@erefl gT 1); rewrite cards_eq0; apply: contraL. case/bigcupP=> x Ms_x xR1; apply/set0Pn; exists x. exact: mem_sigma_cover_decomposition (Msigma_ell1 maxM Ms_x) xR1. split=> [MP0 | M K PmaxM hallK Ks Z Zhat ClZhat]. rewrite /partition eqEsubset ntPcover tiPcover notPcover0 !andbT /=. apply/subsetP=> x; rewrite !inE andbT => ntx. have:= sigma_decomposition_dichotomy ntx. have [[y ell1y yRx] _ | _] := exists_inP. have [nty /set0Pn[M /setIdP[maxM Ms_y]]] := ell_sigma1P _ ell1y. apply/bigcupP; exists (class_support M^~~ G); first exact: imset_f. rewrite -(conjg1 x) imset2_f ?inE //. apply/bigcupP; exists y; last by rewrite mem_lcoset. by rewrite !inE nty -cycle_subG. case/exists_inP=> y _; move: (_ * x) => y' /existsP[M]. case/and3P => /setIdP[maxM _] /setD1P[nty' /setIP[My' _]] kMy' {y}. case/set0Pn: MP0; exists M; rewrite 2!inE maxM andbT. apply: contra nty' => kM'M; rewrite -order_eq1 (pnat_1 kMy') //. exact: mem_p_elt kM'M My'. have [_ [defNK _] [ntKs _] _ _] := Ptype_structure PmaxM hallK. have [Mst [PmaxMst _] [_ [hallKst _] [defK _]]] := Ptype_embedding PmaxM hallK. rewrite -/Ks -/Z -/Zhat in ntKs hallKst * => _ [_ _ conjMMst _]. have [_ _ [ntK _] _ _] := Ptype_structure PmaxMst hallKst. have [maxM _] := setDP PmaxM; rewrite defK in ntK. have [|//|tiZPcover notPcovZ]: _ /\ ClZhat \notin _ := trivIsetU1 _ tiPcover _. move=> HcovG; case/imsetP=> H maxH ->{HcovG}. rewrite -setI_eq0 /ClZhat !class_supportEr big_distrr big1 //= => a _. rewrite big_distrl big1 //= => b _; apply/eqP; rewrite -cards_eq0. rewrite -(cardJg _ b^-1) conjIg conjsgK -conjsgM -sigma_supportJ cards_eq0. wlog ->: a b H maxH / H :^ (a * b^-1) = H. by move/(_ a a (H :^ (a * b^-1))%G); rewrite mmaxJ mulgV act1 => ->. rewrite setIC big_distrl big1 //= => y Hs_y; apply/setP=> x; rewrite in_set0. rewrite 3!inE mem_lcoset negb_or -andbA; apply/and4P=> [[yRx notKx notKs_x]]. rewrite /Z cent_joinEr ?subsetIr //; case/mulsgP=> z z' Kz Ks_z' defx. have:= sigma_decomposition_dichotomy (group1_contra notKx). rewrite (introT exists_inP) /=; last first. by exists y; rewrite // (Msigma_ell1 maxH). have [Ms_z' cKz'] := setIP Ks_z'; case/exists_inP; exists z'. rewrite (Msigma_ell1 maxM) ?inE // Ms_z' andbT. by apply: contraNneq notKx => z'1; rewrite defx z'1 mulg1. apply/existsP; exists M; rewrite inE maxM cycle_subG Ms_z'. rewrite defx -(centP cKz') // mulKg (mem_p_elt (pHall_pgroup hallK)) //=. rewrite 3!inE (subsetP (pHall_sub hallK)) //= cent1C !andbT. rewrite andbC cent1C (subsetP _ _ Kz) ?sub_cent1 //=. by apply: contraNneq notKs_x => z1; rewrite defx z1 mul1g. split=> //; rewrite /partition eqEsubset 2!inE {}tiZPcover negb_or notPcover0. rewrite /cover big_setU1 {notPcovZ}//= subUset ntPcover subsetD1 subsetT. rewrite {}/ClZhat {}/Zhat !andbT /= andbC; apply/and3P; split. - have [[y Ks_y nty] [y' Ky' nty']] := (trivgPn _ ntKs, trivgPn _ ntK). rewrite eq_sym; apply/set0Pn; exists ((y' * y) ^ 1). apply: imset2_f; rewrite 2?inE // groupMl // groupMr // -/Ks negb_or. have [_ _ _ tiKKs] := dprodP defNK. rewrite -[Z]genM_join ?mem_gen ?mem_mulg //= andbT; apply/andP; split. by apply: contra nty => Ky; rewrite -in_set1 -set1gE -tiKKs inE Ky. by apply: contra nty' => Ks_y'; rewrite -in_set1 -set1gE -tiKKs inE Ky'. - rewrite class_supportEr; apply/bigcupP=> [[a _]]. by rewrite mem_conjg conj1g 2!inE !group1. apply/subsetP=> x; case/setD1P=> ntx _; apply/setUP. case: exists_inP (sigma_decomposition_dichotomy ntx) => [[y ell1y yRx] _ | _]. have [nty] := ell_sigma1P _ ell1y; case/set0Pn=> H; case/setIdP=> maxH Hs_y. right; apply/bigcupP; exists (class_support H^~~ G); first exact: imset_f. rewrite -[x]conjg1 imset2_f ?inE //; apply/bigcupP. by exists y; rewrite ?mem_lcoset // !inE nty -cycle_subG. case/exists_inP=> y ell1y /existsP[H]; set y' := y^-1 * x. case/and3P=> /setIdP[maxH Hs_y] /setD1P[nty' /setIP[Hy' cyy']] kHy'. rewrite {ntK ntKs maxM defNK}/Z /Ks; left. wlog{Ks Mst PmaxMst hallKst conjMMst defK maxH} defH: M K PmaxM hallK / H :=: M. move=> IH; have PmaxH: H \in 'M_'P. apply/PtypeP; split=> //; exists (pdiv #[y']). by rewrite (pnatPpi kHy') // pi_pdiv order_gt1. have [|] := setUP (conjMMst H PmaxH); case/imsetP=> a Ga defH. have:= IH _ (K :^ a)%G _ _ defH. rewrite (eq_pHall _ _ (kappaJ _ _)) pHallJ2 PtypeJ MsigmaJ centJ. by rewrite -conjIg -conjUg -conjYg -conjDg class_supportGidl //; apply. have:= IH _ [group of Ks :^ a] _ _ defH. rewrite (eq_pHall _ _ (kappaJ _ _)) pHallJ2 PtypeJ MsigmaJ centJ. rewrite -conjIg -conjUg -conjYg -conjDg setUC joingC defK. by rewrite class_supportGidl //; apply. have /andP[sMsM nMsM]: M`_\sigma <| M := pcore_normal _ M. have{Hs_y} Ms_y: y \in M`_\sigma by rewrite -defH -cycle_subG. wlog{H defH Hy' kHy'} Ky': K hallK / y' \in K. have [maxM _] := setDP PmaxM; rewrite -cycle_subG defH in Hy' kHy'. have [a Ma Ka_y'] := Hall_subJ (mmax_sol maxM) hallK Hy' kHy'. move/(_ (K :^ a)%G); rewrite pHallJ // -cycle_subG. rewrite -{1 2}(normsP nMsM a Ma) centJ -conjIg -conjYg -conjUg -conjDg. by rewrite class_supportGidl ?inE //; apply. rewrite -[x]conjg1 imset2_f ?group1 //. have [Mst _ [_ _ _ [cycZ _ defZ _ _] _]] := Ptype_embedding PmaxM hallK. rewrite -(mulKVg y x) -/y' 2!inE negb_or andbC. do [set Ks := 'C_(_)(K); set Z := K <*> _] in cycZ defZ *. have Ks_y: y \in Ks. have cKZ := sub_abelian_cent (cyclic_abelian cycZ) (joing_subl K Ks). rewrite inE Ms_y (subsetP cKZ) // -(defZ y'); last by rewrite !inE nty'. by rewrite inE cent1C (subsetP sMsM). have [_ [defNK _] _ _ _] := Ptype_structure PmaxM hallK. have{defNK} [_ _ cKKs tiKKs] := dprodP defNK. rewrite [Z]joingC cent_joinEl // mem_mulg // groupMr // groupMl //= -/Ks. apply/andP; split. have [nty _] := ell_sigma1P _ ell1y. by apply: contra nty => Ky; rewrite -in_set1 -set1gE -tiKKs inE Ky. by apply: contra nty' => Ks_y'; rewrite -in_set1 -set1gE -tiKKs inE Ky'. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype bigop order) mathcomp(finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall frobenius) mathcomp(ssralg ssrnum ssrint rat) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection12 BGsection13)