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	⊢ ( 𝑇 ∈ BndLinOp → 𝑇 ∈ LinOp )

Proof

Step	Hyp	Ref	Expression
1		elbdop	⊢ ( 𝑇 ∈ BndLinOp ↔ ( 𝑇 ∈ LinOp ∧ ( normop ‘ 𝑇 ) < +∞ ) )
2	1	simplbi	⊢ ( 𝑇 ∈ BndLinOp → 𝑇 ∈ LinOp )