proposition: Corollary tau2_regular M E E1 E2 E3 p A (Ms := M`_\sigma) : M \in 'M -> sigma_complement M E E1 E2 E3 -> p \in \tau2(M) -> A \in 'E_p^2(E) -> [/\ semiregular Ms E3, semiregular Ms 'C_E1(A) & A \subset E2].
proof: Proof. move=> maxM complEi t2Mp Ep2A; have p_pr := pnElem_prime Ep2A. have [hallE hallE1 hallE2 hallE3 _] := complEi. have [sEM sM'E _] := and3P hallE; have [sM'p _] := andP t2Mp. have [sAE abelA dimA] := pnElemP Ep2A; have [pA cAA _] := and3P abelA. have Ep2A_M: A \in 'E_p^2(M) by rewrite (subsetP (pnElemS _ _ sEM)). have [_ _ _ tiMsMA _] := tau2_context maxM t2Mp Ep2A_M. have [[nsAE _] _ _ _] := tau2_compl_context maxM hallE t2Mp Ep2A. have [sCAM _]: 'C(A) \subset M /\ _ := p2Elem_mmax maxM Ep2A_M. have sAE2: A \subset E2. exact: normal_sub_max_pgroup (Hall_max hallE2) (pi_pnat pA _) nsAE. split=> // x /setD1P[ntx]; last first. case/setIP; rewrite -cent_cycle -!cycle_subG => sXE1 cAX. pose q := pdiv #[x]; have piXq: q \in \pi(#[x]) by rewrite pi_pdiv order_gt1. have [Q sylQ] := Sylow_exists q <[x]>; have [sQX qQ _] := and3P sylQ. have [sE1E t1E1 _] := and3P hallE1; have sQE1 := subset_trans sQX sXE1. have sQM := subset_trans sQE1 (subset_trans sE1E sEM). have [H /setIdP[maxH sNQH]]: {H | H \in 'M('N(Q))}. apply: mmax_exists; rewrite mFT_norm_proper ?(mFT_pgroup_proper qQ) //. by rewrite -rank_gt0 (rank_pgroup qQ) (p_rank_Sylow sylQ) p_rank_gt0. apply/trivgP; rewrite -(tiMsMA H) ?setIS //. by rewrite (subset_trans _ sNQH) ?cents_norm ?centS. rewrite 3!inE maxH /=; apply/andP; split. apply: contra_orbit (mmax_norm_notJ maxM maxH qQ sQM sNQH _). by rewrite (pnatPpi (pgroupS sXE1 t1E1)) ?orbT. by rewrite (subset_trans _ sNQH) ?cents_norm // centsC (subset_trans sQX). rewrite -cent_cycle -cycle_subG => sXE3. pose q := pdiv #[x]; have piXq: q \in \pi(#[x]) by rewrite pi_pdiv order_gt1. have [Q sylQ] := Sylow_exists q <[x]>; have [sQX qQ _] := and3P sylQ. have [sE3E t3E3 _] := and3P hallE3; have sQE3 := subset_trans sQX sXE3. have sQM := subset_trans sQE3 (subset_trans sE3E sEM). have [H /setIdP[maxH sNQH]]: {H | H \in 'M('N(Q))}. apply: mmax_exists; rewrite mFT_norm_proper ?(mFT_pgroup_proper qQ) //. by rewrite -rank_gt0 (rank_pgroup qQ) (p_rank_Sylow sylQ) p_rank_gt0. apply/trivgP; rewrite -(tiMsMA H) ?setIS //. by rewrite (subset_trans _ sNQH) ?cents_norm ?centS. rewrite 3!inE maxH /=; apply/andP; split. apply: contra_orbit (mmax_norm_notJ maxM maxH qQ sQM sNQH _). by rewrite (pnatPpi (pgroupS sXE3 t3E3)) ?orbT. rewrite (subset_trans _ sNQH) ?cents_norm // (subset_trans _ (centS sQE3)) //. have coE3A: coprime #|E3| #|A|. by rewrite (pnat_coprime t3E3 (pi_pnat pA _)) ?tau3'2. rewrite (sameP commG1P trivgP) -(coprime_TIg coE3A) subsetI commg_subl. have [[_ nsE3E] _ _ _ _] := sigma_compl_context maxM complEi. by rewrite commg_subr (subset_trans sE3E) ?(subset_trans sAE) ?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)