proposition: Proposition beta_subnorm_uniq p P X : p \in \beta(G) -> p.-Sylow(G) P -> X \subset P -> 'N_P(X)%G \in 'U.
proof: Proof. move=> b_p sylP sXP; set Q := 'N_P(X)%G. have pP := pHall_pgroup sylP; have pQ: p.-group Q := pgroupS (subsetIl _ _) pP. have [| rQle1] := ltnP 1 'r(Q); first exact: beta_noncyclic_uniq pQ. have cycQ: cyclic Q. by rewrite (odd_pgroup_rank1_cyclic pQ) ?mFT_odd -?rank_pgroup. have defQ: P :=: Q. apply: (nilpotent_sub_norm (pgroup_nil pP) (subsetIl _ _)). by rewrite setIS // char_norms // sub_cyclic_char // subsetI sXP normG. have:= forall_inP b_p P; rewrite inE negb_imply ltnNge; move/(_ sylP). by rewrite defQ -(rank_pgroup pQ) (leq_trans rQle1). 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)