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\in \mathrm{dom}{adj}_h\to T:\mathscr{H}⟶\mathscr{H}$$

Proof

Step	Hyp	Ref	Expression
1		dmadjss	$$⊢\mathrm{dom}{adj}_h\subseteq {\mathscr{H}}^{\mathscr{H}}$$
2	1	sseli	$$⊢T\in \mathrm{dom}{adj}_h\to T\in \left({\mathscr{H}}^{\mathscr{H}}\right)$$
3		ax-hilex	$$⊢\mathscr{H}\in \mathrm{V}$$
4	3 3	elmap	$$⊢T\in \left({\mathscr{H}}^{\mathscr{H}}\right)\leftrightarrow T:\mathscr{H}⟶\mathscr{H}$$
5	2 4	sylib	$$⊢T\in \mathrm{dom}{adj}_h\to T:\mathscr{H}⟶\mathscr{H}$$