proposition: Lemma tau13_primact_Msigma M E E1 E2 E3 : M \in 'M -> sigma_complement M E E1 E2 E3 -> ~ semiregular E3 E1 -> semiprime M`_\sigma (E3 <*> E1).
proof: Proof. move=> maxM complEi not_regE13; set Ms := M`_\sigma. have [hallE hallE1 hallE2 hallE3 _] := complEi. have [[sE1E t1E1 _] [sE3E t3E3 _]] := (and3P hallE1, and3P hallE3). have [[sEM _ _] [_ t2E2 _]] := (and3P hallE, and3P hallE2). have [[_ nsE3E] _ [_ cycE3] [defE _] tiE3cE]:= sigma_compl_context maxM complEi. have [[_ nE3E] [sMsM nMsM]] := (andP nsE3E, andP (pcore_normal _ M : Ms <| M)). have [P]: exists2 P, P \in 'E^1(E1) & 'C_E3(P) != 1. apply/exists_inP; rewrite -negb_forall_in; apply/forall_inP=> regE13. apply: not_regE13 => x /setD1P[]; rewrite -cycle_subG -cycle_eq1 -rank_gt0. case/rank_geP=> P E1xP sXE1; apply/trivgP; move: E1xP. rewrite /= -(setIidPr sXE1) nElemI -setIdE => /setIdP[E1_P sPX]. by rewrite -(eqP (regE13 P E1_P)) -cent_cycle setIS ?centS. rewrite -{1}(setIidPr sE1E) nElemI -setIdE => /setIdP[/nElemP[p EpP] sPE1]. rewrite -{1}(setIidPl sE3E) -setIA setIC -rank_gt0 => /rank_geP[R]. rewrite nElemI -setIdE => /setIdP[/nElemP[r ErR] sRE3]. have t1p: p \in \tau1(M). rewrite (pnatPpi (pgroupS sPE1 t1E1)) //= (card_p1Elem EpP). by rewrite pi_of_prime ?inE ?(pnElem_prime EpP) //. have prE1 := tau1_primact_Msigma maxM hallE hallE1. have prE3 := tau3_primact_Msigma maxM hallE hallE3. have sCsPR: 'C_Ms(P) \subset 'C_Ms(R) by apply: cent_tau1Elem_Msigma EpP ErR. have [eqCsPR | ltCsPR] := eqVproper sCsPR. move=> x; case/setD1P; rewrite -cycle_eq1 -cycle_subG => ntX sXE31. apply/eqP; rewrite -cent_cycle eqEsubset andbC setIS ?centS //=. have eqCsE13: 'C_Ms(E1) = 'C_Ms(E3). rewrite -(cent_semiprime prE1 sPE1) ?(nt_pnElem EpP) //. by rewrite -(cent_semiprime prE3 sRE3) ?(nt_pnElem ErR). rewrite centY setICA eqCsE13 -setICA setIid. have sE31E: E3 <*> E1 \subset E by apply/joing_subP. have nE3E1 := subset_trans sE1E nE3E. pose y := x.`_\tau1(M); have sYX: <[y]> \subset <[x]> := cycleX x _. have sXE := subset_trans sXE31 sE31E; have sYE := subset_trans sYX sXE. have [t1'x | not_t1'x] := boolP (\tau1(M)^'.-elt x). rewrite (cent_semiprime prE3 _ ntX) // (sub_normal_Hall hallE3) //. apply: pnat_dvd t3E3; rewrite -(Gauss_dvdr _ (p'nat_coprime t1'x t1E1)). by rewrite mulnC (dvdn_trans _ (dvdn_cardMg _ _)) -?norm_joinEr ?cardSg. have{not_t1'x} ntY: #[y] != 1%N by rewrite order_constt partn_eq1. apply: subset_trans (setIS _ (centS sYX)) _. have [solE nMsE] := (sigma_compl_sol hallE, subset_trans sEM nMsM). have [u Eu sYuE1] := Hall_Jsub solE hallE1 sYE (p_elt_constt _ _). rewrite -(conjSg _ _ u) !conjIg -!centJ (normsP nMsE) ?(normsP nE3E) //=. by rewrite -eqCsE13 (cent_semiprime prE1 sYuE1) // trivg_card1 cardJg. have ntCsR: 'C_Ms(R) != 1. by rewrite -proper1G (sub_proper_trans _ ltCsPR) ?sub1G. have ntR: R :!=: 1 by rewrite (nt_pnElem ErR). have [cEPR abelR dimR] := pnElemP ErR; have [rR _ _] := and3P abelR. have{cEPR} [sRE cPR] := subsetIP cEPR; have sRM := subset_trans sRE sEM. have E2_1: E2 :=: 1. have [x defR] := cyclicP (cyclicS sRE3 cycE3). apply: contraNeq ntCsR; rewrite -rank_gt0; have [q _ ->] := rank_witness E2. rewrite p_rank_gt0 defR cent_cycle. move/(pnatPpi t2E2) => t2q. have [A Eq2A _] := ex_tau2Elem hallE t2q. have [-> //] := tau2_regular maxM complEi t2q Eq2A. by rewrite !inE -cycle_subG -cycle_eq1 -defR sRE3 (nt_pnElem ErR). have nRE: E \subset 'N(R) by rewrite (char_norm_trans _ nE3E) ?sub_cyclic_char. have [H maxNH] := mmax_exists (mFT_norm_proper ntR (mFT_pgroup_proper rR)). have [maxH sNH] := setIdP maxNH; have sEH := subset_trans nRE sNH. have ntCsR_P: [~: 'C_Ms(R), P] != 1. rewrite (sameP eqP commG1P); apply: contra (proper_subn ltCsPR). by rewrite subsetI subsetIl. have sCsR_MsH: 'C_Ms(R) \subset Ms :&: H. exact: setIS Ms (subset_trans (cent_sub R) sNH). have ntMsH_P: [~: Ms :&: H, P] != 1 by rewrite (subG1_contra _ ntCsR_P) ?commSg. have tiE1cMsH: 'C_E1(Ms :&: H) = 1. apply: contraNeq (proper_subn ltCsPR) => ntCE1MsH. rewrite (cent_semiprime prE1 sPE1) ?(nt_pnElem EpP) //. rewrite -(cent_semiprime prE1 (subsetIl _ _) ntCE1MsH) /=. by rewrite subsetI subsetIl centsC subIset // orbC centS. have t3r: r \in \tau3(M). by rewrite (pnatPpi t3E3) ?(piSg sRE3) // -p_rank_gt0 p_rank_abelem ?dimR. have t13r: (r \in \tau1(M)) || (r \in \tau3(M)) by rewrite t3r orbT. have [sE1H sRH] := (subset_trans sE1E sEH, subset_trans sRE sEH). have [_ ct1H'R [|sHr _]] := cent_norm_tau13_mmax maxM hallE t13r sRM rR maxNH. rewrite (subG1_contra _ ntMsH_P) // commgS // (subset_trans sPE1) //. by rewrite subsetI (subset_trans sE1E). have t1H_E1: \tau1(H).-group E1. apply/pgroupP=> q q_pr /Cauchy[] // x E1x ox. apply: contraLR (prime_gt1 q_pr) => t1H'q; rewrite -ox cardG_gt1 negbK. rewrite -subG1 -tiE1cMsH subsetI cycle_subG E1x /= ct1H'R //. by rewrite (setIidPl sEH) cycle_subG (subsetP sE1E). by rewrite /pgroup -orderE ox pnatE. have sH'_E1: \sigma(H)^'.-group E1 by apply: sub_pgroup t1H_E1 => q /andP[]. have [F hallF sE1F] := Hall_superset (mmax_sol maxH) sE1H sH'_E1. have [F1 hallF1 sE1F1] := Hall_superset (sigma_compl_sol hallF) sE1F t1H_E1. have{sHr} sRHs: R \subset H`_\sigma. by rewrite (sub_Hall_pcore (Msigma_Hall maxH)) ?(pi_pgroup rR). have cRE1: E1 \subset 'C(R). rewrite centsC (centsS sE1F1) // -subsetIidl subsetI subxx -sRHs -subsetI. have prF1 := tau1_primact_Msigma maxH hallF hallF1. rewrite -(cent_semiprime prF1 (subset_trans sPE1 sE1F1)); last first. exact: nt_pnElem EpP _. by rewrite subsetI sRHs. case/negP: ntR; rewrite -subG1 -tiE3cE subsetI sRE3 centsC -(sdprodW defE). by rewrite E2_1 sdprod1g mul_subG // sub_abelian_cent ?cyclic_abelian. 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)