Theorem bdopln

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

	Ref	Expression
Assertion	bdopln	$$⊢T\in \mathrm{BndLinOp}\to T\in \mathrm{LinOp}$$

Proof

Step	Hyp	Ref	Expression
1		elbdop	$$⊢T\in \mathrm{BndLinOp}\leftrightarrow \left(T\in \mathrm{LinOp}\wedge {norm}_{\mathrm{op}}\left(T\right)<\mathrm{+\infty }\right)$$
2	1	simplbi	$$⊢T\in \mathrm{BndLinOp}\to T\in \mathrm{LinOp}$$