proposition: Theorem abelian_tau2_norm_Sylow M E p A S : M \in 'M -> \sigma(M)^'.-Hall(M) E -> p \in \tau2(M) -> A \in 'E_p^2(E) -> p.-Sylow(G) S -> A \subset S -> abelian S -> forall X, X \subset 'N(S) -> 'C_S(X) <| 'N(S) /\ [~: S, X] <| 'N(S).
proof: Proof. move=> maxM hallE t2Mp Ep2A sylS sAS cSS X nSX. have [_ sNS'F sFCS _ _] := abelian_tau2_sub_Fitting maxM hallE t2Mp Ep2A sylS sAS cSS. have{sNS'F sFCS} sNS'CS: 'N(S)^`(1) \subset 'C(S) := subset_trans sNS'F sFCS. have nCSX_NS: 'N(S) \subset 'N('C(S) * X). rewrite -quotientK ?norms_cent // -{1}(quotientGK (cent_normal S)). by rewrite morphpre_norms // sub_abelian_norm ?quotientS ?sub_der1_abelian. rewrite /normal subIset ?comm_subG ?normG //=; split. have ->: 'C_S(X) = 'C_S('C(S) * X). by rewrite centM setIA; congr (_ :&: _); rewrite (setIidPl _) // centsC. by rewrite normsI ?norms_cent. have CS_S_1: [~: 'C(S), S] = 1 by apply/commG1P. by rewrite commGC -[[~: X, S]]mul1g -CS_S_1 -commMG ?CS_S_1 ?norms1 ?normsR. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq choice div fintype) mathcomp(path bigop finset prime fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor pgroup cyclic commutator) mathcomp(center gseries nilpotent sylow abelian maximal hall frobenius) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection11)