proposition: Corollary nonuniq_norm_Sylow_pprod p H S : H \in 'M -> H :!=: M -> p.-Sylow(G) S -> 'N(S) \subset H :&: M -> M`_\beta * (H :&: M) = M /\ \alpha(M) =i \beta(M).
proof: Proof. move=> maxH neqHM sylS_G sN_HM; have [sNH sNM] := subsetIP sN_HM. have [sSM sSH] := (subset_trans (normG S) sNM, subset_trans (normG S) sNH). have [sylS pS] := (pHall_subl sSM (subsetT M) sylS_G, pHall_pgroup sylS_G). have sMp: p \in \sigma(M) by apply/exists_inP; exists S. have aM'p: p \in \alpha(M)^'. apply: contra neqHM; rewrite !inE -(rank_Sylow sylS) => rS. have uniqS: S \in 'U := rank3_Uniqueness (mFT_pgroup_proper pS) rS. by rewrite (eq_uniq_mmax (def_uniq_mmax uniqS maxM sSM) maxH sSH). have sSM': S \subset M^`(1). by rewrite (subset_trans _ sMsM') ?(sub_Hall_pcore hallMs) ?(pi_pgroup pS). have nMbS := subset_trans sSM (normal_norm nsMbM). have nMbSM: M`_\beta <*> S <| M. rewrite -{2}(quotientGK nsMbM) -quotientYK ?cosetpre_normal //=. have sylS_M' := pHall_subl sSM' sM'M sylS. rewrite (eq_Hall_pcore _ (quotient_pHall nMbS sylS_M')); last first. exact: nilpotent_pcore_Hall Mbeta_quo_nil. by rewrite gFnormal_trans ?quotient_normal ?gFnormal. have defM: M`_\beta * 'N_M(S) = M. have sSNM: S \subset 'N_M(S) by rewrite subsetI sSM normG. rewrite -(mulSGid sSNM) /= mulgA -norm_joinEr //. by rewrite (Frattini_arg _ (pHall_subl _ _ sylS_G)) ?joing_subr ?subsetT. split=> [|q]. apply/eqP; rewrite setIC eqEsubset mulG_subG subsetIl pcore_sub /=. by rewrite -{1}defM mulgS ?setIS. apply/idP/idP=> [aMq|]; last exact: beta_sub_alpha. apply: contraR neqHM => bM'q; have bM'p := contra (@beta_sub_alpha _ M p) aM'p. have [|_ uniqNM _] := beta'_cent_Sylow bM'q bM'p pS. by apply: contraR aM'p; rewrite sSM'; case: eqP => //= <- _. rewrite (eq_uniq_mmax (def_uniq_mmax (uniqNM aMq) maxM (subsetIl _ _)) maxH) //. by rewrite subIset ?(subset_trans (cent_sub _)) ?orbT. 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) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9)