Theorem dmadjrn

Description: The adjoint of an operator belongs to the adjoint function's domain. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	dmadjrn	$$⊢T\in \mathrm{dom}{adj}_h\to {adj}_h\left(T\right)\in \mathrm{dom}{adj}_h$$

Proof

Step	Hyp	Ref	Expression
1		adj1o	$$⊢{adj}_h:\mathrm{dom}{adj}_h\underset{1-1\; onto}{⟶}\mathrm{dom}{adj}_h$$
2		f1of	$$⊢{adj}_h:\mathrm{dom}{adj}_h\underset{1-1\; onto}{⟶}\mathrm{dom}{adj}_h\to {adj}_h:\mathrm{dom}{adj}_h⟶\mathrm{dom}{adj}_h$$
3	1 2	ax-mp	$$⊢{adj}_h:\mathrm{dom}{adj}_h⟶\mathrm{dom}{adj}_h$$
4	3	ffvelcdmi	$$⊢T\in \mathrm{dom}{adj}_h\to {adj}_h\left(T\right)\in \mathrm{dom}{adj}_h$$