proposition: Lemma cyclic_primact_Msigma p P : p.-Sylow(E) P -> cyclic P -> semiprime M`_\sigma P.
proof: Proof. move=> sylP cycP x /setD1P[]; rewrite -cycle_eq1 -cycle_subG => ntX sXP. have [sPE pP _] := and3P sylP; rewrite -cent_cycle. have sPM := subset_trans sPE sEM; have sXM := subset_trans sXP sPM. have pX := pgroupS sXP pP; have ltXG := mFT_pgroup_proper pX. have t13p: (p \in \tau1(M)) || (p \in \tau3(M)). rewrite (tau1E maxM hallE) (tau3E maxM hallE) -p_rank_gt0 -(rank_Sylow sylP). rewrite eqn_leq rank_gt0 (subG1_contra sXP) //= andbT -andb_orl orNb. by rewrite -abelian_rank1_cyclic ?cyclic_abelian. have [H maxNH] := mmax_exists (mFT_norm_proper ntX ltXG). have [cMsX _ _] := cent_norm_tau13_mmax t13p sXM pX maxNH. have [_ sNH] := setIdP maxNH. apply/eqP; rewrite eqEsubset andbC setIS ?centS // subsetI subsetIl /= centsC. apply: subset_trans (cMsX P _ pP) (centS _). rewrite subsetI sPM (subset_trans (cents_norm _) sNH) //. by rewrite sub_abelian_cent // cyclic_abelian. by rewrite setIS // (subset_trans (cent_sub _) sNH). 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)