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 
|- ( T e. BndLinOp -> ( normop ` T ) e. RR )

Proof

Step Hyp Ref Expression
1 bdopf 
 |-  ( T e. BndLinOp -> T : ~H --> ~H )
2 nmopgtmnf 
 |-  ( T : ~H --> ~H -> -oo < ( normop ` T ) )
3 1 2 syl 
 |-  ( T e. BndLinOp -> -oo < ( normop ` T ) )
4 elbdop 
 |-  ( T e. BndLinOp <-> ( T e. LinOp /\ ( normop ` T ) < +oo ) )
5 4 simprbi 
 |-  ( T e. BndLinOp -> ( normop ` T ) < +oo )
6 nmopxr 
 |-  ( T : ~H --> ~H -> ( normop ` T ) e. RR* )
7 xrrebnd 
 |-  ( ( normop ` T ) e. RR* -> ( ( normop ` T ) e. RR <-> ( -oo < ( normop ` T ) /\ ( normop ` T ) < +oo ) ) )
8 1 6 7 3syl 
 |-  ( T e. BndLinOp -> ( ( normop ` T ) e. RR <-> ( -oo < ( normop ` T ) /\ ( normop ` T ) < +oo ) ) )
9 3 5 8 mpbir2and 
 |-  ( T e. BndLinOp -> ( normop ` T ) e. RR )