Description: A bounded linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 2Feb2006) (New usage is discouraged.)
Ref  Expression  

Assertion  bdopf   ( T e. BndLinOp > T : ~H > ~H ) 
Step  Hyp  Ref  Expression 

1  bdopln   ( T e. BndLinOp > T e. LinOp ) 

2  lnopf   ( T e. LinOp > T : ~H > ~H ) 

3  1 2  syl   ( T e. BndLinOp > T : ~H > ~H ) 