Metamath Proof Explorer

Theorem nmoprepnf

Description: The norm of a Hilbert space operator is either real or plus infinity. (Contributed by NM, 5-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmoprepnf ⊢ T : ℋ ⟶ ℋ → norm op ⁡ T ∈ ℝ ↔ norm op ⁡ T ≠ +∞

Proof

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