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

Proof

Step Hyp Ref Expression
1 nmfnsetre ⊢ T : ℋ ⟶ ℂ → x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ⊆ ℝ
2 nmfnsetn0 ⊢ T ⁡ 0 ℎ ∈ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y
3 2 ne0ii ⊢ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ≠ ∅
4 supxrre2 ⊢ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ⊆ ℝ ∧ x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ≠ ∅ → sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ℝ * < ∈ ℝ ↔ sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ℝ * < ≠ +∞
5 1 3 4 sylancl ⊢ T : ℋ ⟶ ℂ → sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ℝ * < ∈ ℝ ↔ sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ℝ * < ≠ +∞
6 nmfnval ⊢ T : ℋ ⟶ ℂ → norm fn ⁡ T = sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ℝ * <
7 6 eleq1d ⊢ T : ℋ ⟶ ℂ → norm fn ⁡ T ∈ ℝ ↔ sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ℝ * < ∈ ℝ
8 6 neeq1d ⊢ T : ℋ ⟶ ℂ → norm fn ⁡ T ≠ +∞ ↔ sup x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = T ⁡ y ℝ * < ≠ +∞
9 5 7 8 3bitr4d ⊢ T : ℋ ⟶ ℂ → norm fn ⁡ T ∈ ℝ ↔ norm fn ⁡ T ≠ +∞