proposition: Corollary mFT_Sylow_der1 : P \subset 'N(P)^`(1).
proof: Proof. have [-> | ntP] := eqsVneq P 1; first exact: sub1G. have ltNG: 'N(P) \proper G := mFT_norm_proper ntP (mFT_pgroup_proper pP). have [M /setIdP[/= maxM sNM]] := mmax_exists ltNG. 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. apply: subset_trans (dergS 1 (subsetIr M 'N(P))) => /=. apply: plength1_Sylow_sub_der1 sylP pl1M (subset_trans _ (Msigma_der1 maxM)). by rewrite (sub_Hall_pcore (Msigma_Hall maxM)) ?(pi_pgroup pP). 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)