proposition: Corollary tau13_nonregular M E E1 E2 E3 : M \in 'M -> sigma_complement M E E1 E2 E3 -> ~ semiregular M`_\sigma E3 -> [/\ E1 :!=: 1, E3 ><| E1 = E, semiprime M`_\sigma E & forall X, X \in 'E^1(E) -> X <| E].
proof: Proof. move=> maxM complEi not_regE3Ms. have [hallE hallE1 hallE2 hallE3 _] := complEi. have [[sE1E t1E1 _] [sE3E t3E3 _]] := (and3P hallE1, and3P hallE3). have{hallE2} E2_1: E2 :==: 1. apply/idPn; rewrite -rank_gt0; have [p _ ->] := rank_witness E2. rewrite p_rank_gt0 => /(pnatPpi (pHall_pgroup hallE2))t2p. have [A Ep2A _] := ex_tau2Elem hallE t2p. by apply: not_regE3Ms; case: (tau2_regular maxM complEi t2p Ep2A). have [_ ntE1 [cycE1 cycE3] [defE _] _] := sigma_compl_context maxM complEi. rewrite (eqP E2_1) sdprod1g in defE; have{} ntE1 := ntE1 E2_1. have [nsE3E _ mulE31 nE31 _] := sdprod_context defE. have cE3E1 P: P \in 'E^1(E1) -> P \subset 'C(E3). by case/nElemP=> p EpP; apply/idPn => /(tau13_regular maxM complEi EpP)[]. split=> // [|X EpX]. rewrite -mulE31 -norm_joinEr //. have [-> | ntE3] := eqsVneq E3 1. by rewrite joing1G; apply: (tau1_primact_Msigma maxM hallE hallE1). apply: tau13_primact_Msigma maxM complEi _ => regE13. have:= ntE1; rewrite -rank_gt0; case/rank_geP=> P EpP. have cPE3: E3 \subset 'C(P) by rewrite centsC cE3E1. have [p Ep1P] := nElemP EpP; have [sPE1 _ _] := pnElemP Ep1P. have ntP: P :!=: 1 by apply: (nt_pnElem Ep1P). by case/negP: ntE3; rewrite -(setIidPl cPE3) (cent_semiregular regE13 _ ntP). have [p Ep1X] := nElemP EpX; have [sXE abelX oX] := pnElemPcard Ep1X. have [p_pr ntX] := (pnElem_prime Ep1X, nt_pnElem Ep1X isT). have tau31p: p \in [predU \tau3(M) & \tau1(M)]. rewrite (pgroupP (pgroupS sXE _)) ?oX // -mulE31 pgroupM. rewrite (sub_pgroup _ t3E3) => [|q t3q]; last by rewrite inE /= t3q. by rewrite (sub_pgroup _ t1E1) // => q t1q; rewrite inE /= t1q orbT. have [/= t3p | t1p] := orP tau31p. rewrite (char_normal_trans _ nsE3E) ?sub_cyclic_char //. by rewrite (sub_normal_Hall hallE3) // (pi_pgroup (abelem_pgroup abelX)). have t1X := pi_pgroup (abelem_pgroup abelX) t1p. have [e Ee sXeE1] := Hall_Jsub (sigma_compl_sol hallE) hallE1 sXE t1X. rewrite /normal sXE -(conjSg _ _ e) conjGid //= -normJ -mulE31 mulG_subG. rewrite andbC sub_abelian_norm ?cyclic_abelian ?cents_norm // centsC cE3E1 //. rewrite -(setIidPr sE1E) nElemI !inE sXeE1 andbT. by rewrite -(pnElemJ e) conjGid // def_pnElem in Ep1X; case/setIP: Ep1X. 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)