proposition: Corollary mFT_sub_Sylow_trans : forall Q x, Q \subset P -> Q :^ x \subset P -> exists2 y, y \in 'N(P) & Q :^ x = Q :^ y.
proof: Proof. move=> Q x; have [-> /trivgP-> /trivgP-> | ntP sQP sQxP] := eqsVneq P 1. by exists 1; rewrite ?group1 ?conjs1g. have ltNG: 'N(P) \proper G := mFT_norm_proper ntP (mFT_pgroup_proper pP). have [M /=] := mmax_exists ltNG; case/setIdP=> maxM sNM. have [ltMG solM] := (mmax_proper maxM, mmax_sol maxM). have [pl1M sPM] := (mFT_proper_plength1 p ltMG, subset_trans (normG P) sNM). have sylP := pHall_subl sPM (subsetT M) sylP_G. have sMp: p \in \sigma(M) by apply/exists_inP; exists P. have [transCQ _ _] := sigma_group_trans maxM sMp (pgroupS sQP pP). have [||q cQq [u Mu defx]] := transCQ x; try exact: subset_trans _ sPM. have nQC := normP (subsetP (cent_sub Q) _ _). have [|q' cMQq' [y nMPy defu]] := plength1_Sylow_trans sylP pl1M solM sQP Mu. by rewrite defx conjsgM nQC in sQxP. have [[_ nPy] [_ cQq']] := (setIP nMPy, setIP cMQq'). by exists y; rewrite // defx defu !conjsgM 2?nQC. 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)