proposition: Theorem tau1_primact_Msigma E1 : \tau1(M).-Hall(E) E1 -> semiprime M`_\sigma E1.
proof: Proof. move=> hallE1 x /setD1P[]; rewrite -cycle_eq1 -cycle_subG => ntX sXE1. rewrite -cent_cycle; have [sE1E t1E1 _] := and3P hallE1. have [_ [E3 hallE3]] := ex_tau13_compl hallE. have{hallE3} [E2 _ complEi] := ex_tau2_compl hallE hallE1 hallE3. have [_ _ [cycE1 _] _ _ {E2 E3 complEi}] := sigma_compl_context maxM complEi. apply/eqP; rewrite eqEsubset andbC setIS ?centS //= subsetI subsetIl /=. have [p _ rX] := rank_witness <[x]>; rewrite -rank_gt0 {}rX in ntX. have t1p: p \in \tau1(M) by rewrite (pnatPpi t1E1) // (piSg sXE1) -?p_rank_gt0. have{ntX} [P EpP] := p_rank_geP ntX; have{EpP} [sPX abelP dimP] := pnElemP EpP. have{sXE1} sPE1 := subset_trans sPX sXE1. have{dimP} EpP: P \in 'E_p^1(E) by rewrite !inE abelP dimP (subset_trans sPE1). apply: {x sPX abelP} subset_trans (setIS _ (centS sPX)) _; rewrite centsC. rewrite -(Sylow_gen E1) gen_subG; apply/bigcupsP=> S; case/SylowP=> r _ sylS. have [[sSE1 rS _] [-> | ntS]] := (and3P sylS, eqsVneq S 1); first exact: sub1G. have [cycS sSE] := (cyclicS sSE1 cycE1, subset_trans sSE1 sE1E). have /p_rank_geP[R ErR]: 0 < 'r_r(S) by rewrite -rank_pgroup ?rank_gt0. have{ErR} [sRS abelR dimR] := pnElemP ErR; have sRE1 := subset_trans sRS sSE1. have{abelR dimR} ErR: R \in 'E_r^1('C_E(P)). rewrite !inE abelR dimR (subset_trans sRE1) // subsetI sE1E. by rewrite sub_abelian_cent ?cyclic_abelian. rewrite centsC (subset_trans (cent_tau1Elem_Msigma t1p EpP ErR)) //. have [y defR]: exists y, R :=: <[y]> by apply/cyclicP; apply: cyclicS cycS. have sylS_E: r.-Sylow(E) S. apply: subHall_Sylow hallE1 (pnatPpi t1E1 _) (sylS). by rewrite -p_rank_gt0 -(rank_Sylow sylS) rank_gt0. rewrite defR cent_cycle (cyclic_primact_Msigma sylS_E cycS) ?subsetIr //. by rewrite !inE -cycle_subG -cycle_eq1 -defR (nt_pnElem ErR). 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)