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 TBndLinOpT:

Proof

Step Hyp Ref Expression
1 bdopln TBndLinOpTLinOp
2 lnopf TLinOpT:
3 1 2 syl TBndLinOpT: