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 ‘ 𝑇 ) ∈ ℝ )