proposition: Theorem cent_tau1Elem_Msigma p r P R (Ms := M`_\sigma) : p \in \tau1(M) -> P \in 'E_p^1(E) -> R \in 'E_r^1('C_E(P)) -> 'C_Ms(P) \subset 'C_Ms(R).
proof: Proof. have /andP[sMsM nMsM]: Ms <| M := pcore_normal _ M. have coMsE: coprime #|Ms| #|E| := coprime_sigma_compl hallE. pose Ma := M`_\alpha; have sMaMs: Ma \subset Ms := Malpha_sub_Msigma maxM. rewrite pnElemI -setIdE => t1Mp EpP /setIdP[ErR cPR]. without loss symPR: p r P R EpP ErR cPR t1Mp / r \in \tau1(M) -> 'C_Ma(P) \subset 'C_Ma(R) -> 'C_Ma(P) = 'C_Ma(R). - move=> IH; apply: (IH p r) => // t1Mr sCaPR; apply/eqP; rewrite eqEsubset. rewrite sCaPR -(setIidPl sMaMs) -!setIA setIS ?(IH r p) 1?centsC // => _. by case/eqVproper; rewrite // /proper sCaPR andbF. do [rewrite !subsetI !subsetIl /=; set cRCaP := _ \subset _] in symPR *. pose Mz := 'O_(if cRCaP then \sigma(M) else \alpha(M))(M); pose C := 'C_Mz(P). suffices: C \subset 'C(R) by rewrite /C /Mz /cRCaP; case: ifP => // ->. have sMzMs: Mz \subset Ms by rewrite /Mz; case: ifP => // _. have sCMs: C \subset Ms by rewrite subIset ?sMzMs. have [[sPE abelP dimP] [sRE abelR dimR]] := (pnElemP EpP, pnElemP ErR). have [sPM sRM] := (subset_trans sPE sEM, subset_trans sRE sEM). have [[pP cPP _] [rR _]] := (and3P abelP, andP abelR). have coCR: coprime #|C| #|R| := coprimeSg sCMs (coprimegS sRE coMsE). have ntP: P :!=: 1 by apply: nt_pnElem EpP _. pose ST := [set S | Sylow C (gval S) & R \subset 'N(S)]. have sST_CP S: S \in ST -> S \subset C by case/setIdP=> /SylowP[q _ /andP[]]. rewrite -{sST_CP}[C](Sylow_transversal_gen sST_CP) => [|q _]; last first. have nMzR: R \subset 'N(Mz) by rewrite (subset_trans sRM) // gFnorm. have{nMzR} nCR: R \subset 'N(C) by rewrite normsI // norms_cent // cents_norm. have solC := solvableS (subset_trans sCMs sMsM) (mmax_sol maxM). have [S sylS nSR] := coprime_Hall_exists q nCR coCR solC. by exists S; rewrite // inE (p_Sylow sylS) nSR. rewrite gen_subG; apply/bigcupsP=> S /setIdP[/SylowP[q _ sylS] nSR] {ST}. have [sSC qS _] := and3P sylS. have [sSMs [sSMz cPS]] := (subset_trans sSC sCMs, subsetIP sSC). rewrite (sameP commG1P eqP) /=; set Q := [~: S, R]; apply/idPn => ntQ. have sQS: Q \subset S by [rewrite commg_subl]; have qQ := pgroupS sQS qS. have piQq: q \in \pi(Q) by rewrite -p_rank_gt0 -(rank_pgroup qQ) rank_gt0. have{piQq} [nQR piSq] := (commg_normr R S : R \subset 'N(Q), piSg sQS piQq). have [H maxNH] := mmax_exists (mFT_norm_proper ntP (mFT_pgroup_proper pP)). have [maxH sNH] := setIdP maxNH; have sCPH := subset_trans (cent_sub _) sNH. have [sPH sRH] := (subset_trans cPP sCPH, subset_trans cPR sCPH). have [sSM sSH] := (subset_trans sSMs sMsM, subset_trans cPS sCPH). have [sQM sQH] := (subset_trans sQS sSM, subset_trans sQS sSH). have ntMsH_R: [~: Ms :&: H, R] != 1. by rewrite (subG1_contra _ ntQ) ?commSg // subsetI sSMs. have sR_EH: R \subset E :&: H by apply/subsetIP. have ntMsH_MH: [~: Ms :&: H, M :&: H] != 1. by rewrite (subG1_contra _ ntMsH_R) ?commgS // (subset_trans sR_EH) ?setSI. have t13Mp: p \in [predU \tau1(M) & \tau3(M)] by apply/orP; left. have [_ cMsH_t1H' [//|sHp bHp]] := cent_norm_tau13_mmax t13Mp sPM pP maxNH. have{cMsH_t1H'} t1Hr: r \in \tau1(H). apply: contraR ntMsH_R => t1H'r; rewrite (sameP eqP commG1P) centsC. by rewrite cMsH_t1H' // (pi_pgroup rR). have ntCHaRQ: 'C_(H`_\alpha)(R <*> Q) != 1. rewrite centY (subG1_contra _ ntP) ?subsetI //= centsC cPR centsC. rewrite (subset_trans sQS cPS) (subset_trans _ (Mbeta_sub_Malpha H)) //. by rewrite (sub_Hall_pcore (Mbeta_Hall maxH)) // (pi_pgroup pP) ?bHp. have not_MGH: gval H \notin M :^: G. by apply: contraL sHp => /imsetP[x _ ->]; rewrite sigmaJ; case/andP: t1Mp. have neqHM: H :!=: M := contra_orbit _ _ not_MGH. have cSS: abelian S. apply: contraR neqHM => /(nonabelian_Uniqueness qS)uniqS. by rewrite (eq_uniq_mmax (def_uniq_mmax uniqS maxM sSM) maxH sSH). have tiQcR: 'C_Q(R) = 1 by rewrite coprime_abel_cent_TI // (coprimeSg sSC). have sMq: q \in \sigma(M) := pnatPpi (pcore_pgroup _ M) (piSg sSMs piSq). have aH'q: q \notin \alpha(H). have [|_ tiHaMs _] := sigma_disjoint maxH maxM; first by rewrite orbit_sym. by apply: contraFN (tiHaMs q) => aHq; apply/andP. have piRr: r \in \pi(R) by rewrite -p_rank_gt0 p_rank_abelem ?dimR. have ErH_R: R \in 'E_r^1(H) by rewrite !inE sRH abelR dimR. have{piRr} sM'r: r \in \sigma(M)^' := pnatPpi (pgroupS sRE sM'E) piRr. have r'q: q \in r^' by apply: contraTneq sMq => ->. have ntHa: H`_\alpha != 1 by rewrite (subG1_contra _ ntCHaRQ) ?subsetIl. have uniqNQ: 'M('N(Q)) = [set H]. apply: contraNeq ntCHaRQ; rewrite joingC. by case/(cent_Malpha_reg_tau1 _ _ r'q ErH_R) => //; case=> //= _ -> _. have maxNQ_H: H \in 'M('N(Q)) :\ M by rewrite uniqNQ !inE neqHM /=. have{maxNQ_H} [_ _] := sigma_subgroup_embedding maxM sMq sQM qQ ntQ maxNQ_H. have [sHq [_ st1HM [_ ntMa]] | _ [_ _ sM'MH]] := ifP; last first. have piPp: p \in \pi(P) by rewrite -p_rank_gt0 p_rank_abelem ?dimP. have sPMH: P \subset M :&: H by apply/subsetIP. by have/negP[] := pnatPpi (pgroupS sPMH (pHall_pgroup sM'MH)) piPp. have{st1HM} t1Mr: r \in \tau1(M). by case/orP: (st1HM r t1Hr); rewrite //= (contraNF ((alpha_sub_sigma _) r)). have aM'q: q \notin \alpha(M). have [_ tiMaHs _] := sigma_disjoint maxM maxH not_MGH. by apply: contraFN (tiMaHs q) => aMq; apply/andP. have ErM_R: R \in 'E_r^1(M) by rewrite !inE sRM abelR dimR. have: 'M('N(Q)) != [set M] by rewrite uniqNQ (inj_eq (@set1_inj _)). case/(cent_Malpha_reg_tau1 _ _ r'q ErM_R) => //. case=> //= ntCMaP tiCMaPQ _; case/negP: ntCMaP. rewrite -subG1 -{}tiCMaPQ centY setICA subsetIidr /= -/Ma -/Q centsC. apply/commG1P/three_subgroup; apply/commG1P. by rewrite commGC (commG1P _) ?sub1G ?subsetIr. apply: subset_trans (subsetIr Ma _); rewrite /= -symPR //. rewrite commg_subl normsI //; last by rewrite norms_cent // cents_norm. by rewrite (subset_trans sSM) ?gFnorm. apply: contraR aM'q => not_cRCaP; apply: pnatPpi (pgroupS sSMz _) piSq. by rewrite (negPf not_cRCaP) pcore_pgroup. 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 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection12)