proposition: Lemma cent1_sigma'_Zgroup P : p.-Sylow(M) P -> P :!=: 1 -> exists x, [/\ x \in 'Ohm_1('Z(P))^#, 'M('C[x]) != [set M] & Zgroup 'C_(M`_\alpha)[x]].
proof: Proof. move=> sylP ntP; have [sPM pP _] := and3P sylP; have nilP := pgroup_nil pP. set T := 'Ohm_1('Z(P)); have charT: T \char P by rewrite !gFchar_trans. suffices [x Tx not_uCx]: exists2 x, x \in T^# & 'M('C[x]) != [set M]. exists x; split=> //; rewrite odd_rank1_Zgroup ?mFT_odd //= leqNgt. apply: contra not_uCx; rewrite -cent_cycle; set X := <[x]> => rCMaX. have{Tx} [ntX Tx] := setD1P Tx; rewrite -cycle_eq1 -/X in ntX. have sXP: X \subset P by rewrite cycle_subG (subsetP (char_sub charT)). rewrite (@def_uniq_mmaxS _ M 'C_M(X)) ?subsetIr ?mFT_cent_proper //. apply: def_uniq_mmax; rewrite ?subsetIl //. rewrite cent_alpha'_uniq ?(subset_trans sXP) ?(pi_pgroup (pgroupS sXP pP)) //. by apply: contra s'p; apply: alpha_sub_sigma. apply/exists_inP; rewrite -negb_forall_in; apply: contra s'p. move/forall_inP => uCT; apply/exists_inP; exists P => //. apply/subsetP=> u nPu; have [y Ty]: exists y, y \in T^#. by apply/set0Pn; rewrite setD_eq0 subG1 Ohm1_eq1 center_nil_eq1. rewrite -(norm_mmax maxM) (sameP normP eqP) (inj_eq (@group_inj gT)) -in_set1. have Tyu: y ^ u \in T^#. by rewrite memJ_norm // normD1 (subsetP (char_norms charT)). by rewrite -(eqP (uCT _ Tyu)) -conjg_set1 normJ mmax_ofJ (eqP (uCT _ Ty)) set11. 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)