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 TBndLinOpnormopT

Proof

Step Hyp Ref Expression
1 bdopf TBndLinOpT:
2 nmopgtmnf T:−∞<normopT
3 1 2 syl TBndLinOp−∞<normopT
4 elbdop TBndLinOpTLinOpnormopT<+∞
5 4 simprbi TBndLinOpnormopT<+∞
6 nmopxr T:normopT*
7 xrrebnd normopT*normopT−∞<normopTnormopT<+∞
8 1 6 7 3syl TBndLinOpnormopT−∞<normopTnormopT<+∞
9 3 5 8 mpbir2and TBndLinOpnormopT