proposition: Corollary mFT_Sylow_normalS Q R : p.-group R -> Q \subset P :&: R -> Q <| 'N(P) -> Q <| 'N(R).
proof: Proof. move=> pR /subsetIP[sQP sQR] /andP[nQP nQ_NP]. have [x _ sRxP] := Sylow_Jsub sylP_G (subsetT R) pR. rewrite /normal normsG //; apply/subsetP=> y nRy. have sQxP: Q :^ x \subset P by rewrite (subset_trans _ sRxP) ?conjSg. have sQyxP: Q :^ (y * x) \subset P. by rewrite actM (subset_trans _ sRxP) // -(normP nRy) !conjSg. have [t tNP defQx] := mFT_sub_Sylow_trans sQP sQxP. have [z zNP defQxy] := mFT_sub_Sylow_trans sQP sQyxP. by rewrite inE -(conjSg _ _ x) -actM /= defQx defQxy !(normsP nQ_NP). 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)