Theorem elbdop2

Description: Property defining a bounded linear Hilbert space operator. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	elbdop2	|- ( T e. BndLinOp <-> ( T e. LinOp /\ ( normop ` T ) e. RR ) )

Proof

Step	Hyp	Ref	Expression
1		elbdop	|- ( T e. BndLinOp <-> ( T e. LinOp /\ ( normop ` T ) < +oo ) )
2		lnopf	|- ( T e. LinOp -> T : ~H --> ~H )
3		nmopreltpnf	|- ( T : ~H --> ~H -> ( ( normop ` T ) e. RR <-> ( normop ` T ) < +oo ) )
4	2 3	syl	|- ( T e. LinOp -> ( ( normop ` T ) e. RR <-> ( normop ` T ) < +oo ) )
5	4	pm5.32i	|- ( ( T e. LinOp /\ ( normop ` T ) e. RR ) <-> ( T e. LinOp /\ ( normop ` T ) < +oo ) )
6	1 5	bitr4i	|- ( T e. BndLinOp <-> ( T e. LinOp /\ ( normop ` T ) e. RR ) )