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 : ~H --> ~H -> ( normop ` T ) e. RR* )

Proof

Step Hyp Ref Expression
1 nmopval 
 |-  ( T : ~H --> ~H -> ( normop ` T ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) )
2 nmopsetretHIL 
 |-  ( T : ~H --> ~H -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } C_ RR )
3 ressxr 
 |-  RR C_ RR*
4 2 3 sstrdi 
 |-  ( T : ~H --> ~H -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } C_ RR* )
5 supxrcl 
 |-  ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } C_ RR* -> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) e. RR* )
6 4 5 syl 
 |-  ( T : ~H --> ~H -> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) e. RR* )
7 1 6 eqeltrd 
 |-  ( T : ~H --> ~H -> ( normop ` T ) e. RR* )