proposition: Proposition sub'cent_sigma_cyclic K (Y := 'C_K(M`_\sigma) :&: M^`(1)) : K \subset M -> sigma'.-group K -> cyclic Y /\ Y <| M.
proof: Proof. move=> sKM sg'K; pose Z := 'O_sigma'('F(M)). have nsZM: Z <| M by rewrite !gFnormal_trans. have [sZM nZM] := andP nsZM; have Fnil := Fitting_nil M. have rZle1: 'r(Z) <= 1. apply: leq_trans (rankS _) (sub'cent_sigma_rank1 sZM (pcore_pgroup _ _)). rewrite subsetI subxx (sameP commG1P trivgP) /=. rewrite -(TI_pcoreC \sigma(M) M 'F(M)) subsetI commg_subl commg_subr. by rewrite (subset_trans sZM) ?gFnorm ?gFsub_trans. have{rZle1} cycZ: cyclic Z. have nilZ: nilpotent Z := nilpotentS (gFsub _ _) Fnil. by rewrite nil_Zgroup_cyclic // odd_rank1_Zgroup // mFT_odd. have cZM': M^`(1) \subset 'C_M(Z). rewrite der1_min ?normsI ?normG ?norms_cent //= -ker_conj_aut. rewrite (isog_abelian (first_isog_loc _ _)) //. by rewrite (abelianS (Aut_conj_aut _ _)) // Aut_cyclic_abelian. have sYF: Y \subset 'F(M). apply: subset_trans (cent_sub_Fitting (mmax_sol maxM)). have [_ /= <- _ _] := dprodP (nilpotent_pcoreC \sigma(M) Fnil). by rewrite centM setICA setISS // setIC subIset ?centS // pcore_Fitting. have{sYF} sYZ: Y \subset Z. rewrite (sub_Hall_pcore (nilpotent_pcore_Hall _ Fnil)) //=. by rewrite -setIA (pgroupS (subsetIl K _)). by rewrite (cyclicS sYZ cycZ) (char_normal_trans _ nsZM) // sub_cyclic_char. 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) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9)