proposition: Proposition commG_sigma'_1Elem_cyclic p K P (K0 := [~: K, P]) : K \subset M -> sigma'.-group K -> p \in sigma' -> P \in 'E_p^1('N_M(K)) -> 'C_(M`_\sigma)(P) = 1 -> p^'.-group K -> abelian K -> [/\ K0 \subset 'C(M`_\sigma), cyclic K0 & K0 <| M].
proof: Proof. move=> sKM sg'K sg'p EpP regP p'K cKK. have nK0P: P \subset 'N(K0) := commg_normr P K. have p_pr := pnElem_prime EpP; have [sPMN _ oP] := pnElemPcard EpP. have [sPM nKP]: P \subset M /\ P \subset 'N(K) by apply/subsetIP. have /andP[sMsM nMsM]: M`_\sigma <| M := pcore_normal _ _. have sK0K: K0 \subset K by rewrite commg_subl. have [sK0M sg'K0]:= (subset_trans sK0K sKM, pgroupS sK0K sg'K). have [nMsK0 nMsP] := (subset_trans sK0M nMsM, subset_trans sPM nMsM). have coKP: coprime #|K| #|P| by rewrite oP coprime_sym prime_coprime -?p'natE. have coK0Ms: coprime #|K0| #|M`_\sigma|. by rewrite coprime_sym (pnat_coprime (pcore_pgroup _ _)). have nilK0Ms: nilpotent (K0 <*> M`_\sigma). have mulK0MsP: K0 <*> M`_\sigma ><| P = K0 <*> M`_\sigma <*> P. rewrite sdprodEY ?normsY // coprime_TIg //= norm_joinEl //. rewrite coprime_cardMg // coprimeMl (coprimeSg sK0K) //. by rewrite oP (pnat_coprime (pcore_pgroup _ _)) ?pnatE. apply: (prime_Frobenius_sol_kernel_nil mulK0MsP); rewrite ?oP //=. by rewrite (solvableS _ solM) // !join_subG sK0M pcore_sub. rewrite norm_joinEl // -subcent_TImulg ?subsetI ?nK0P //. by rewrite coprime_abel_cent_TI ?mul1g. exact: coprime_TIg. have cMsK0: K0 \subset 'C(M`_\sigma). rewrite (sub_nilpotent_cent2 nilK0Ms) ?joing_subl ?joing_subr //. exact: pnat_coprime (pcore_pgroup _ _) sg'K0. have [cycY nsYM] := sub'cent_sigma_cyclic sK0M sg'K0. set Y := _ :&: _ in cycY nsYM. have sK0Y: K0 \subset Y by rewrite !subsetI subxx cMsK0 commgSS. split=> //; first exact: cyclicS sK0Y cycY. by apply: char_normal_trans nsYM; rewrite 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)