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 ⊢ T : ℋ ⟶ ℂ → norm fn ⁡ T ∈ ℝ *

Proof

Step Hyp Ref Expression
1 nmfnval ⊢ T : ℋ ⟶ ℂ → norm fn ⁡ T = sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ℝ * <
2 nmfnsetre ⊢ T : ℋ ⟶ ℂ → x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ⊆ ℝ
3 ressxr ⊢ ℝ ⊆ ℝ *
4 2 3 sstrdi ⊢ T : ℋ ⟶ ℂ → x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ⊆ ℝ *
5 supxrcl ⊢ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ⊆ ℝ * → sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ℝ * < ∈ ℝ *
6 4 5 syl ⊢ T : ℋ ⟶ ℂ → sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ℝ * < ∈ ℝ *
7 1 6 eqeltrd ⊢ T : ℋ ⟶ ℂ → norm fn ⁡ T ∈ ℝ *