Metamath Proof Explorer

Theorem dmadjop

Description: A member of the domain of the adjoint function is a Hilbert space operator. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion dmadjop T dom adj h T :


Step Hyp Ref Expression
1 dmadjss dom adj h
2 1 sseli T dom adj h T
3 ax-hilex V
4 3 3 elmap T T :
5 2 4 sylib T dom adj h T :