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

Metamath Proof Explorer

Theorem nmfnrepnf

Description: The norm of a Hilbert space functional is either real or plus infinity. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

Ref Expression
Assertion nmfnrepnf ( 𝑇 : ℋ ⟶ ℂ → ( ( normfn ‘ 𝑇 ) ∈ ℝ ↔ ( normfn ‘ 𝑇 ) ≠ +∞ ) )

Proof

Step Hyp Ref Expression
1 nmfnsetre ⊢ ( 𝑇 : ℋ ⟶ ℂ → { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ⊆ ℝ )
2 nmfnsetn0 ⊢ ( abs ‘ ( 𝑇 ‘ 0ℎ ) ) ∈ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) }
3 2 ne0ii ⊢ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ≠ ∅
4 supxrre2 ⊢ ( ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ⊆ ℝ ∧ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ≠ ∅ ) → ( sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ* , < ) ∈ ℝ ↔ sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ* , < ) ≠ +∞ ) )
5 1 3 4 sylancl ⊢ ( 𝑇 : ℋ ⟶ ℂ → ( sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ* , < ) ∈ ℝ ↔ sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ* , < ) ≠ +∞ ) )
6 nmfnval ⊢ ( 𝑇 : ℋ ⟶ ℂ → ( normfn ‘ 𝑇 ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ* , < ) )
7 6 eleq1d ⊢ ( 𝑇 : ℋ ⟶ ℂ → ( ( normfn ‘ 𝑇 ) ∈ ℝ ↔ sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ* , < ) ∈ ℝ ) )
8 6 neeq1d ⊢ ( 𝑇 : ℋ ⟶ ℂ → ( ( normfn ‘ 𝑇 ) ≠ +∞ ↔ sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ) } , ℝ* , < ) ≠ +∞ ) )
9 5 7 8 3bitr4d ⊢ ( 𝑇 : ℋ ⟶ ℂ → ( ( normfn ‘ 𝑇 ) ∈ ℝ ↔ ( normfn ‘ 𝑇 ) ≠ +∞ ) )