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 ) )