proposition: Lemma FT_signalizer_baseJ x z : 'N[x ^ z] :=: 'N[x] :^ z.
proof: Proof. case MSx_gt1: (#|'M_\sigma[x]| > 1); last first. by rewrite /'N[x] /'N[_] cycleJ card_sigma_mmaxJ MSx_gt1 conjs1g. have [x1 | ntx] := eqVneq x 1. rewrite x1 conj1g /'N[1] /= norm1. case: pickP => [M maxTM | _]; last by rewrite if_same conjs1g. by have [maxM] := setIdP maxTM; case/idPn; rewrite proper_subn ?mmax_proper. apply: congr_group; apply/eqP; rewrite eq_sym -in_set1. have ell1xz: \ell_\sigma(x ^ z) == 1%N. by rewrite ell_sigmaJ; apply/ell_sigma1P; rewrite -cards_eq0 -lt0n ltnW. have [_ [|<- _ _ _ _]] := FT_signalizer_context ell1xz. by rewrite cycleJ card_sigma_mmaxJ. rewrite -conjg_set1 normJ mmax_ofJ; rewrite ell_sigmaJ in ell1xz. by have [_ [//|-> _ _ _ _]] := FT_signalizer_context ell1xz; apply: set11. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype bigop order) mathcomp(finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall frobenius) mathcomp(ssralg ssrnum ssrint rat) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection12 BGsection13)