proposition: Corollary cent_Hall_sigma_sdprod M H pi : M \in 'M -> pi.-Hall(M`_\sigma) H -> H :!=: 1 -> exists X, [/\ gval X \subset M, cyclic X, \tau2(M).-group X & 'C_(M`_\sigma)(H) ><| X = 'C_M(H)].
proof: Proof. move=> maxM hallH ntH; have hallMs := Msigma_Hall maxM. have nsMsM: M`_\sigma <| M := pcore_normal _ M; have [sMsM nMsM] := andP nsMsM. have sMs := pHall_pgroup hallMs; have [sHMs piH _] := and3P hallH. have k'CH: \kappa(M)^'.-group 'C_M(H). apply/idPn; rewrite negb_and cardG_gt0 all_predC negbK => /hasP[p piCHp kMp]. have PmaxM: M \in 'M_'P by apply/PtypeP; split; last exists p. have [X]: exists X, X \in 'E_p^1('C_M(H)). by apply/p_rank_geP; rewrite p_rank_gt0. case/pnElemP; case/subsetIP=> sXM cHX abelX dimX; have [pX _] := andP abelX. have [K hallK sXK] := Hall_superset (mmax_sol maxM) sXM (pi_pgroup pX kMp). have E1X: X \in 'E^1(K) by apply/nElemP; exists p; apply/pnElemP. have [q q_pr rqH] := rank_witness H; have [S sylS] := Sylow_exists q H. have piSq: q \in \pi(S). by rewrite -p_rank_gt0 (p_rank_Sylow sylS) -rqH rank_gt0. have [_ [defNK defNX] _ [_ not_sylCP _] _] := Ptype_structure PmaxM hallK. have{defNX} [defNX _] := defNX X E1X. have [[_ nsKs] [_ mulKKs _ _]] := (dprod_normal2 defNK, dprodP defNK). have s'K := sub_pgroup (@kappa_sigma' _ _) (pHall_pgroup hallK). have [_ hallKs] := coprime_mulGp_Hall mulKKs s'K (pgroupS (subsetIl _ _) sMs). have [sSH _] := andP sylS. have sylS_Ms := subHall_Sylow hallH (pnatPpi piH (piSg sSH piSq)) sylS. have [sSMs _] := andP sylS_Ms; have sS := pgroupS sSMs sMs. have sylS_M := subHall_Sylow hallMs (pnatPpi sS piSq) sylS_Ms. have sSKs: S \subset 'C_(M`_\sigma)(K). rewrite (sub_normal_Hall hallKs) //= -defNX subsetI (pHall_sub sylS_M) /=. by rewrite cents_norm // centsC (centsS sSH). by have [_ /negP] := not_sylCP q (piSg sSKs piSq) S sylS_M. have solCH := solvableS (subsetIl M 'C(H)) (mmax_sol maxM). have [X hallX] := Hall_exists \sigma(M)^' solCH; exists X. have nsCsH: 'C_(M`_\sigma)(H) <| 'C_M(H) by rewrite /normal setSI // normsIG. have hallCs: \sigma(M).-Hall('C_M(H)) 'C_(M`_\sigma)(H). by rewrite -(setIidPl sMsM) -setIA (setI_normal_Hall nsMsM) ?subsetIl. rewrite (sdprod_normal_p'HallP nsCsH hallX hallCs). have [-> | ntX] := eqsVneq X 1; first by rewrite sub1G cyclic1 pgroup1. have [sXCH s'X _] := and3P hallX; have [sXM cHX] := subsetIP sXCH. have sk'X: \sigma_kappa(M)^'.-group X. apply/pgroupP=> p p_pr p_dv_X; apply/norP=> /=. by split; [apply: (pgroupP s'X) | apply: (pgroupP (pgroupS sXCH k'CH))]. have [K hallK] := Hall_exists \kappa(M) (mmax_sol maxM). have [U complU] := ex_kappa_compl maxM hallK; have [hallU _ _] := complU. have [a Ma sXaU] := Hall_Jsub (mmax_sol maxM) hallU sXM sk'X. have [_ _ cycX _ _] := kappa_structure maxM complU. rewrite -(cyclicJ _ a) -(pgroupJ _ _ a); have [||//] := cycX _ sXaU. by rewrite -(isog_eq1 (conj_isog X a)). rewrite -(normsP nMsM a Ma) centJ -conjIg -(isog_eq1 (conj_isog _ a)). by rewrite (subG1_contra _ ntH) // subsetI sHMs centsC. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq choice div fintype) mathcomp(path bigop finset prime fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor pgroup cyclic commutator) mathcomp(center 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)