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𝑇 ) ≠ +∞ ) )