This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nmopreltpnf

Description: The norm of a Hilbert space operator is real iff it is less than infinity. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 nmoprepnf 
 |-  ( T : ~H --> ~H -> ( ( normop ` T ) e. RR <-> ( normop ` T ) =/= +oo ) )
2 nmopxr 
 |-  ( T : ~H --> ~H -> ( normop ` T ) e. RR* )
3 nltpnft 
 |-  ( ( normop ` T ) e. RR* -> ( ( normop ` T ) = +oo <-> -. ( normop ` T ) < +oo ) )
4 2 3 syl 
 |-  ( T : ~H --> ~H -> ( ( normop ` T ) = +oo <-> -. ( normop ` T ) < +oo ) )
5 4 necon2abid 
 |-  ( T : ~H --> ~H -> ( ( normop ` T ) < +oo <-> ( normop ` T ) =/= +oo ) )
6 1 5 bitr4d 
 |-  ( T : ~H --> ~H -> ( ( normop ` T ) e. RR <-> ( normop ` T ) < +oo ) )