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 e. dom adjh -> T : ~H --> ~H )

Proof

Step	Hyp	Ref	Expression
1		dmadjss	|- dom adjh C_ ( ~H ^m ~H )
2	1	sseli	|- ( T e. dom adjh -> T e. ( ~H ^m ~H ) )
3		ax-hilex	|- ~H e. _V
4	3 3	elmap	|- ( T e. ( ~H ^m ~H ) <-> T : ~H --> ~H )
5	2 4	sylib	|- ( T e. dom adjh -> T : ~H --> ~H )