proposition: Lemma nonuniq_p2Elem_cent_sigma M Mstar p A A0 : M \in 'M -> Mstar \in 'M -> Mstar :!=: M -> A \in 'E_p^2(M) -> A0 \in 'E_p^1(A) -> 'N(A0) \subset Mstar -> [/\ p \notin \sigma(M) -> A \subset 'C(M`_\sigma :&: Mstar) & p \notin \alpha(M) -> A \subset 'C(M`_\alpha :&: Mstar)].
proof: Proof. move: Mstar => H maxM maxH neqMH Ep2A EpA0 sNH. have p_pr := pnElem_prime Ep2A. have [sAM abelA dimA] := pnElemP Ep2A; have [pA cAA _] := and3P abelA. have [sA0A _ _] := pnElemP EpA0; have pA0 := pgroupS sA0A pA. have sAH: A \subset H. by apply: subset_trans (cents_norm _) sNH; apply: subset_trans (centS sA0A). have nsHsH: H`_\sigma <| H by apply: pcore_normal. have [sHsH nHsH] := andP nsHsH; have nHsA := subset_trans sAH nHsH. have nsHsA_H: H`_\sigma <*> A <| H. have [sHp | sH'p] := boolP (p \in \sigma(H)). rewrite (joing_idPl _) ?pcore_normal //. by rewrite (sub_Hall_pcore (Msigma_Hall _)) // (pi_pgroup pA). have [P sylP sAP] := Sylow_superset sAH pA. have excH: exceptional_FTmaximal p H A0 A by split=> //; apply/pnElemP. exact: exceptional_mul_sigma_normal excH sylP sAP. have cAp' K: p^'.-group K -> A \subset 'N(K) -> K \subset H -> [~: K, A] \subset K :&: H`_\sigma. - move=> p'K nKA sKH; have nHsK := subset_trans sKH nHsH. rewrite subsetI commg_subl nKA /= -quotient_sub1 ?comm_subG // quotientR //=. have <-: K / H`_\sigma :&: A / H`_\sigma = 1. by rewrite setIC coprime_TIg ?coprime_morph ?(pnat_coprime pA p'K). rewrite subsetI commg_subl commg_subr /= -{2}(quotientYidr nHsA). by rewrite !quotient_norms //= joingC (subset_trans sKH) ?normal_norm. have [sMp | sM'p] := boolP (p \in \sigma(M)). split=> // aM'p; have notMGH: gval H \notin M :^: G. apply: mmax_norm_notJ maxM maxH pA0 (subset_trans sA0A sAM) sNH _. by rewrite sMp eq_sym neqMH. rewrite centsC (sameP commG1P trivgP). apply: subset_trans (cAp' _ _ _ (subsetIr _ _)) _. - exact: pi_p'group (pgroupS (subsetIl _ _) (pcore_pgroup _ _)) aM'p. - by rewrite (normsI _ (normsG sAH)) // (subset_trans sAM) ?gFnorm. by rewrite setIAC; case/sigma_disjoint: notMGH => // -> _ _; apply: subsetIl. suffices cMaA: A \subset 'C(M`_\sigma :&: H). by rewrite !{1}(subset_trans cMaA) ?centS ?setSI // Malpha_sub_Msigma. have [sHp | sH'p] := boolP (p \in \sigma(H)); last first. apply/commG1P; apply: contraNeq neqMH => ntA_MsH. have [P sylP sAP] := Sylow_superset sAH pA. have excH: exceptional_FTmaximal p H A0 A by split=> //; apply/pnElemP. have maxAM: M \in 'M(A) by apply/setIdP. rewrite (exceptional_sigma_uniq maxH excH sylP sAP maxAM) //. apply: contraNneq ntA_MsH => tiMsHs; rewrite -subG1. have [sHsA_H nHsA_H] := andP nsHsA_H. have <-: H`_\sigma <*> A :&: M`_\sigma = 1. apply/trivgP; rewrite -tiMsHs subsetI subsetIr /=. rewrite -quotient_sub1 ?subIset ?(subset_trans sHsA_H) //. rewrite quotientGI ?joing_subl //= joingC quotientYidr //. rewrite setIC coprime_TIg ?coprime_morph //. rewrite (pnat_coprime (pcore_pgroup _ _)) // (card_pnElem Ep2A). by rewrite pnatX ?orbF ?pnatE. rewrite commg_subI // subsetI ?joing_subr ?subsetIl. by rewrite (subset_trans sAM) ?gFnorm. by rewrite setIC subIset ?nHsA_H. have sAHs: A \subset H`_\sigma. by rewrite (sub_Hall_pcore (Msigma_Hall maxH)) // (pi_pgroup pA). have [S sylS sAS] := Sylow_superset sAHs pA; have [sSHs pS _] := and3P sylS. have nsHaH: H`_\alpha <| H := pcore_normal _ _; have [_ nHaH] := andP nsHaH. have nHaS := subset_trans (subset_trans sSHs sHsH) nHaH. have nsHaS_H: H`_\alpha <*> S <| H. rewrite -{2}(quotientGK nsHaH) (norm_joinEr nHaS) -quotientK //. rewrite cosetpre_normal; apply: char_normal_trans (quotient_normal _ nsHsH). rewrite /= (nilpotent_Hall_pcore _ (quotient_pHall _ sylS)) ?pcore_char //. exact: nilpotentS (quotientS _ (Msigma_der1 maxH)) (Malpha_quo_nil maxH). rewrite (sameP commG1P trivgP). have <-: H`_\alpha <*> S :&: M`_\sigma = 1. have: gval M \notin H :^: G. by apply: contra sM'p; case/imsetP=> x _ ->; rewrite sigmaJ. case/sigma_disjoint=> // _ ti_aHsM _. rewrite setIC coprime_TIg ?(pnat_coprime (pcore_pgroup _ _)) //=. rewrite norm_joinEr // [pnat _ _]pgroupM (pi_pgroup pS) // andbT. apply: sub_pgroup (pcore_pgroup _ _) => q aHq. by apply: contraFN (ti_aHsM q) => sMq; rewrite inE /= aHq. rewrite commg_subI // subsetI ?subsetIl. by rewrite (subset_trans sAS) ?joing_subr ?(subset_trans sAM) ?gFnorm. by rewrite setIC subIset 1?normal_norm. 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 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection11)