proposition: Proposition max_normed_2Elem_signaliser p q (A Q : {group gT}) : p != q -> A \in 'E_p^2(G) :&: 'E*_p(G) -> Q \in |/|*(A; q) -> q %| #|'C(A)| -> exists2 P : {group gT}, p.-Sylow(G) P /\ A \subset P & [/\ 'O_p^'('C(P)) * ('N(P) :&: 'N(Q)) = 'N(P), P \subset 'N(Q)^`(1) & q.-narrow Q -> P \subset 'C(Q)].
proof: Proof. move=> neq_pq /setIP[Ep2A EpmA] maxQ piCAq. have [_ abelA dimA] := pnElemP Ep2A; have [pA cAA _] := and3P abelA. have [p_pr oA] := (pnElem_prime Ep2A, card_pnElem Ep2A). have{dimA} rA2: 'r(A) = 2 by rewrite (rank_abelem abelA). have{EpmA} ncA: normed_constrained A. have ntA: A :!=: 1 by rewrite -rank_gt0 rA2. exact: plength_1_normed_constrained ntA EpmA (mFT_proper_plength1 _). pose pi := \pi(A); pose K := 'O_pi^'('C(A)). have def_pi : pi =i (p : nat_pred). by move=> r; rewrite !inE /= oA primesX ?primes_prime ?inE. have pi'q : q \notin pi by rewrite def_pi !inE eq_sym. have transKA: [transitive K, on |/|*(A; q) | 'JG]. by rewrite normed_constrained_rank2_trans // (center_idP cAA) rA2. have [P0 sylP0 sAP0] := Sylow_superset (subsetT _) pA. have pP0: p.-group P0 := pHall_pgroup sylP0. have piP0: pi.-group P0 by rewrite (eq_pgroup _ def_pi). have{pP0} snAP0: A <|<| P0 := nilpotent_subnormal (pgroup_nil pP0) sAP0. have{pi'q snAP0 ncA piP0} [//|] := normed_trans_superset ncA pi'q snAP0 piP0. rewrite /= -/pi -/K => -> transKP submaxPA maxPfactoring. have{transKP} [Q0 maxQ0 _] := imsetP transKP. have{transKA} [k Kk defQ] := atransP2 transKA (subsetP submaxPA _ maxQ0) maxQ. set P := P0 :^ k; have{sylP0} sylP: p.-Sylow(G) P by rewrite pHallJ ?in_setT. have nAK: K \subset 'N(A) by rewrite cents_norm ?pcore_sub. have{sAP0 nAK K Kk} sAP: A \subset P by rewrite -(normsP nAK k Kk) conjSg. exists [group of P] => //. have{maxPfactoring} [sPNQ' defNP] := maxPfactoring _ maxQ0. move/(congr1 ('Js%act^~ k)): defNP sPNQ'; rewrite -(conjSg _ _ k) /=. rewrite conjsMg !conjIg !conjsRg -!derg1 -!normJ -pcoreJ -centJ -/P. rewrite -(congr_group defQ) (eq_pcore _ (eq_negn def_pi)) => defNP sPNQ'. have{} sPNQ': P \subset 'N(Q)^`(1). by rewrite (setIidPl (mFT_Sylow_der1 sylP)) in sPNQ'. split=> // narrowQ; have [-> | ntQ] := eqsVneq Q 1; first exact: cents1. pose AutQ := conj_aut Q @* 'N(Q). have qQ: q.-group Q by case/mem_max_normed: maxQ. have ltNG: 'N(Q) \proper G by rewrite mFT_norm_proper // (mFT_pgroup_proper qQ). have{ltNG} qAutQ': q.-group AutQ^`(1). have qAutQq: q.-group 'O_q(AutQ) := pcore_pgroup _ _. rewrite (pgroupS _ qAutQq) // der1_min ?gFnorm //. have solAutQ: solvable AutQ by rewrite morphim_sol -?mFT_sol_proper. have [oddQ oddAutQ]: odd #|Q| /\ odd #|AutQ| by rewrite morphim_odd mFT_odd. by have /(Aut_narrow qQ)[] := Aut_conj_aut Q 'N(Q). have nQP: P \subset 'N(Q) := subset_trans sPNQ' (der_sub 1 _). rewrite (sameP setIidPl eqP) eqEsubset subsetIl /=. rewrite -quotient_sub1 ?normsI ?normG ?norms_cent //= -ker_conj_aut subG1. rewrite trivg_card1 (card_isog (first_isog_loc _ _)) //= -trivg_card1 -subG1. have q'AutP: q^'.-group (conj_aut Q @* P). by rewrite morphim_pgroup //; apply: pi_pnat (pHall_pgroup sylP) _. rewrite -(coprime_TIg (pnat_coprime qAutQ' q'AutP)) subsetI subxx. by rewrite /= -morphim_der // morphimS. 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)