Metamath Proof Explorer

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 e. BndLinOp -> T e. LinOp )

Proof

Step Hyp Ref Expression
1 elbdop 
 |-  ( T e. BndLinOp <-> ( T e. LinOp /\ ( normop ` T ) < +oo ) )
2 1 simplbi 
 |-  ( T e. BndLinOp -> T e. LinOp )