proposition: Remark kappa_nonregular M p P : p \in \kappa(M) -> P \in 'E_p^1(M) -> 'C_(M`_\sigma)(P) != 1.
proof: Proof. move=> kMp EpP; have rpM := rank_kappa kMp. have [sPM abelP oP] := pnElemPcard EpP; have [pP _] := andP abelP. have [Q EpQ nregQ]: exists2 Q, Q \in 'E_p^1(M) & 'C_(M`_\sigma)(Q) != 1. by apply/exists_inP; rewrite unlock in kMp; case/andP: kMp. have [sQM abelQ oQ] := pnElemPcard EpQ; have [pQ _] := andP abelQ. have [S sylS sQS] := Sylow_superset sQM pQ; have [_ pS _] := and3P sylS. have [x Mx sPxS] := Sylow_Jsub sylS sPM pP. rewrite -(inj_eq (@conjsg_inj _ x)) conjs1g conjIg -centJ. rewrite (normsP (normal_norm (pcore_normal _ _))) // (subG1_contra _ nregQ) //. rewrite setIS ?centS // -(cardSg_cyclic _ sPxS sQS) ?cardJg ?oP ?oQ //. by rewrite (odd_pgroup_rank1_cyclic pS) ?mFT_odd // (p_rank_Sylow sylS) rpM. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype bigop order) mathcomp(finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall frobenius) mathcomp(ssralg ssrnum ssrint rat) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection12 BGsection13)