Theorem adjsslnop

Description: Every operator with an adjoint is linear. (Contributed by NM, 17-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	adjsslnop	$$⊢\mathrm{dom}{adj}_h\subseteq \mathrm{LinOp}$$

Proof

Step	Hyp	Ref	Expression
1		adjadj	$$⊢t\in \mathrm{dom}{adj}_h\to {adj}_h\left({adj}_h\left(t\right)\right)=t$$
2		dmadjrn	$$⊢t\in \mathrm{dom}{adj}_h\to {adj}_h\left(t\right)\in \mathrm{dom}{adj}_h$$
3		adjlnop	$$⊢{adj}_h\left(t\right)\in \mathrm{dom}{adj}_h\to {adj}_h\left({adj}_h\left(t\right)\right)\in \mathrm{LinOp}$$
4	2 3	syl	$$⊢t\in \mathrm{dom}{adj}_h\to {adj}_h\left({adj}_h\left(t\right)\right)\in \mathrm{LinOp}$$
5	1 4	eqeltrrd	$$⊢t\in \mathrm{dom}{adj}_h\to t\in \mathrm{LinOp}$$
6	5	ssriv	$$⊢\mathrm{dom}{adj}_h\subseteq \mathrm{LinOp}$$