This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑇 ) ∈ ℝ* )