Metamath Proof Explorer

Theorem bdopadj

Description: Every bounded linear Hilbert space operator has an adjoint. (Contributed by NM, 22-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion bdopadj 
|- ( T e. BndLinOp -> T e. dom adjh )

Proof

Step Hyp Ref Expression
1 bdopssadj 
 |-  BndLinOp C_ dom adjh
2 1 sseli 
 |-  ( T e. BndLinOp -> T e. dom adjh )