Metamath Proof Explorer

Theorem bdopf

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

Ref Expression
Assertion bdopf 
|- ( T e. BndLinOp -> T : ~H --> ~H )

Proof

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 )