# Metamath Proof Explorer

## Theorem nmoprepnf

Description: The norm of a Hilbert space operator is either real or plus infinity. (Contributed by NM, 5-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmoprepnf
`|- ( T : ~H --> ~H -> ( ( normop ` T ) e. RR <-> ( normop ` T ) =/= +oo ) )`

### Proof

Step Hyp Ref Expression
1 nmopsetretHIL
` |-  ( T : ~H --> ~H -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } C_ RR )`
2 nmopsetn0
` |-  ( normh ` ( T ` 0h ) ) e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) }`
3 2 ne0ii
` |-  { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } =/= (/)`
4 supxrre2
` |-  ( ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } C_ RR /\ { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } =/= (/) ) -> ( sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) e. RR <-> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) =/= +oo ) )`
5 1 3 4 sylancl
` |-  ( T : ~H --> ~H -> ( sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) e. RR <-> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) =/= +oo ) )`
6 nmopval
` |-  ( T : ~H --> ~H -> ( normop ` T ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) )`
7 6 eleq1d
` |-  ( T : ~H --> ~H -> ( ( normop ` T ) e. RR <-> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) e. RR ) )`
8 6 neeq1d
` |-  ( T : ~H --> ~H -> ( ( normop ` T ) =/= +oo <-> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) =/= +oo ) )`
9 5 7 8 3bitr4d
` |-  ( T : ~H --> ~H -> ( ( normop ` T ) e. RR <-> ( normop ` T ) =/= +oo ) )`