proposition: Corollary mFT_subnorm_Sylow Q : Q \subset P -> p.-Sylow('N(Q)) 'N_P(Q).
proof: Proof. move=> sQP; have pQ := pgroupS sQP pP. have [S /= sylS] := Sylow_exists p 'N(Q); have [sNS pS _] := and3P sylS. have sQS: Q \subset S := normal_sub_max_pgroup (Hall_max sylS) pQ (normalG Q). have [x _ sSxP] := Sylow_Jsub sylP_G (subsetT S) pS. have sQxP: Q :^ x \subset P by rewrite (subset_trans _ sSxP) ?conjSg. have [y nPy defQy] := mFT_sub_Sylow_trans sQP sQxP. have nQxy: x * y^-1 \in 'N(Q) by rewrite inE conjsgM defQy actK. have sSxyP: S :^ (x * y^-1) \subset P by rewrite conjsgM sub_conjgV (normP nPy). have sylSxy: p.-Sylow('N(Q)) (S :^ (x * y^-1)) by rewrite pHallJ. have pNPQ: p.-group 'N_P(Q) := pgroupS (subsetIl P 'N(Q)) pP. by rewrite (sub_pHall sylSxy pNPQ) ?subsetIr // subsetI sSxyP (@pHall_sub _ p). 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)