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

Metamath Proof Explorer

Theorem nmopxr

Description: The norm of a Hilbert space operator is an extended real. (Contributed by NM, 9-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmopxr ⊢ T : ℋ ⟶ ℋ → norm op ⁡ T ∈ ℝ *

Proof

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