Theorem nmfnxr

Description: The norm of any Hilbert space functional is an extended real. (Contributed by NM, 9-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	nmfnxr	⊢ ( 𝑇 : ℋ ⟶ ℂ → ( normfn ‘ 𝑇 ) ∈ ℝ* )

Proof

Step	Hyp	Ref	Expression
1		nmfnval	⊢ ( 𝑇 : ℋ ⟶ ℂ → ( normfn ‘ 𝑇 ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ* , < ) )
2		nmfnsetre	⊢ ( 𝑇 : ℋ ⟶ ℂ → { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ⊆ ℝ )
3		ressxr	⊢ ℝ ⊆ ℝ*
4	2 3	sstrdi	⊢ ( 𝑇 : ℋ ⟶ ℂ → { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ⊆ ℝ* )
5		supxrcl	⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ⊆ ℝ* → sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ* , < ) ∈ ℝ* )
6	4 5	syl	⊢ ( 𝑇 : ℋ ⟶ ℂ → sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ* , < ) ∈ ℝ* )
7	1 6	eqeltrd	⊢ ( 𝑇 : ℋ ⟶ ℂ → ( normfn ‘ 𝑇 ) ∈ ℝ* )