proposition: Corollary tau3_primact_Msigma E3 : \tau3(M).-Hall(E) E3 -> semiprime M`_\sigma E3.
proof: Proof. move=> hallE3 x /setD1P[]; rewrite -cycle_eq1 -cycle_subG => ntX sXE3. have [sE3E t3E3 _] := and3P hallE3; rewrite -cent_cycle. have [[E1 hallE1] _] := ex_tau13_compl hallE. have [E2 _ complEi] := ex_tau2_compl hallE hallE1 hallE3. have [[sE3E' nsE3E] _ [_ cycE3] _ _] := sigma_compl_context maxM complEi. apply/eqP; rewrite eqEsubset andbC setIS ?centS // subsetI subsetIl /= centsC. pose p := pdiv #[x]; have p_pr: prime p by rewrite pdiv_prime ?cardG_gt1. have t3p: p \in \tau3(M) by rewrite (pgroupP (pgroupS sXE3 t3E3)) ?pdiv_dvd. have t13p: [|| p \in \tau1(M) | p \in \tau3(M)] by rewrite t3p orbT. have [y Xy oy]:= Cauchy p_pr (pdiv_dvd _). have ntY: <[y]> != 1 by rewrite -cardG_gt1 -orderE oy prime_gt1. have pY: p.-group <[y]> by rewrite /pgroup -orderE oy pnat_id. have [H maxNH] := mmax_exists (mFT_norm_proper ntY (mFT_pgroup_proper pY)). have sYE3: <[y]> \subset E3 by rewrite cycle_subG (subsetP sXE3). have sYE := subset_trans sYE3 sE3E; have sYM := subset_trans sYE sEM. have [_ cMsY _] := cent_norm_tau13_mmax t13p sYM pY maxNH. have [_ sNH] := setIdP maxNH. have sE3H': E3 \subset H^`(1). rewrite (subset_trans sE3E') ?dergS // (subset_trans _ sNH) ?normal_norm //. by rewrite (char_normal_trans _ nsE3E) // sub_cyclic_char. apply: subset_trans (cMsY E3 _ _) (centS _). - rewrite subsetI sE3E (subset_trans (cents_norm _) sNH) //. by rewrite sub_abelian_cent ?cyclic_abelian. - rewrite (pgroupS sE3H') //; apply/pgroupP=> q _ q_dv_H'. by rewrite !inE q_dv_H' !andbF. by rewrite setIS // (subset_trans _ sNH) // cents_norm ?centS ?cycle_subG. 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)