Theorem adjcl

Description: Closure of the adjoint of a Hilbert space operator. (Contributed by NM, 17-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	adjcl	$$⊢\left(T\in \mathrm{dom}{adj}_h\wedge A\in \mathscr{H}\right)\to {adj}_h\left(T\right)\left(A\right)\in \mathscr{H}$$

Proof

Step	Hyp	Ref	Expression
1		dmadjrn	$$⊢T\in \mathrm{dom}{adj}_h\to {adj}_h\left(T\right)\in \mathrm{dom}{adj}_h$$
2		dmadjop	$$⊢{adj}_h\left(T\right)\in \mathrm{dom}{adj}_h\to {adj}_h\left(T\right):\mathscr{H}⟶\mathscr{H}$$
3	1 2	syl	$$⊢T\in \mathrm{dom}{adj}_h\to {adj}_h\left(T\right):\mathscr{H}⟶\mathscr{H}$$
4	3	ffvelrnda	$$⊢\left(T\in \mathrm{dom}{adj}_h\wedge A\in \mathscr{H}\right)\to {adj}_h\left(T\right)\left(A\right)\in \mathscr{H}$$