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

Metamath Proof Explorer

Theorem nmopre

Description: The norm of a bounded operator is a real number. (Contributed by NM, 29-Jan-2006) (New usage is discouraged.)

Ref Expression
Assertion nmopre ( 𝑇 ∈ BndLinOp → ( normop ‘ 𝑇 ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 bdopf ⊢ ( 𝑇 ∈ BndLinOp → 𝑇 : ℋ ⟶ ℋ )
2 nmopgtmnf ⊢ ( 𝑇 : ℋ ⟶ ℋ → -∞ < ( normop ‘ 𝑇 ) )
3 1 2 syl ⊢ ( 𝑇 ∈ BndLinOp → -∞ < ( normop ‘ 𝑇 ) )
4 elbdop ⊢ ( 𝑇 ∈ BndLinOp ↔ ( 𝑇 ∈ LinOp ∧ ( normop ‘ 𝑇 ) < +∞ ) )
5 4 simprbi ⊢ ( 𝑇 ∈ BndLinOp → ( normop ‘ 𝑇 ) < +∞ )
6 nmopxr ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( normop ‘ 𝑇 ) ∈ ℝ* )
7 xrrebnd ⊢ ( ( normop ‘ 𝑇 ) ∈ ℝ* → ( ( normop ‘ 𝑇 ) ∈ ℝ ↔ ( -∞ < ( normop ‘ 𝑇 ) ∧ ( normop ‘ 𝑇 ) < +∞ ) ) )
8 1 6 7 3syl ⊢ ( 𝑇 ∈ BndLinOp → ( ( normop ‘ 𝑇 ) ∈ ℝ ↔ ( -∞ < ( normop ‘ 𝑇 ) ∧ ( normop ‘ 𝑇 ) < +∞ ) ) )
9 3 5 8 mpbir2and ⊢ ( 𝑇 ∈ BndLinOp → ( normop ‘ 𝑇 ) ∈ ℝ )