Theorem elbdop

Description: Property defining a bounded linear Hilbert space operator. (Contributed by NM, 18-Jan-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	elbdop	$$⊢T\in \mathrm{BndLinOp}\leftrightarrow \left(T\in \mathrm{LinOp}\wedge {norm}_{\mathrm{op}}\left(T\right)<\mathrm{+\infty }\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢t=T\to {norm}_{\mathrm{op}}\left(t\right)={norm}_{\mathrm{op}}\left(T\right)$$
2	1	breq1d	$$⊢t=T\to \left({norm}_{\mathrm{op}}\left(t\right)<\mathrm{+\infty }\leftrightarrow {norm}_{\mathrm{op}}\left(T\right)<\mathrm{+\infty }\right)$$
3		df-bdop	$$⊢\mathrm{BndLinOp}=\left\{t\in \mathrm{LinOp}|{norm}_{\mathrm{op}}\left(t\right)<\mathrm{+\infty }\right\}$$
4	2 3	elrab2	$$⊢T\in \mathrm{BndLinOp}\leftrightarrow \left(T\in \mathrm{LinOp}\wedge {norm}_{\mathrm{op}}\left(T\right)<\mathrm{+\infty }\right)$$