Theorem adjsslnop

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

	Ref	Expression
Assertion	adjsslnop	⊢ dom adjℎ ⊆ LinOp

Proof

Step	Hyp	Ref	Expression
1		adjadj	⊢ ( 𝑡 ∈ dom adjℎ → ( adjℎ ‘ ( adjℎ ‘ 𝑡 ) ) = 𝑡 )
2		dmadjrn	⊢ ( 𝑡 ∈ dom adjℎ → ( adjℎ ‘ 𝑡 ) ∈ dom adjℎ )
3		adjlnop	⊢ ( ( adjℎ ‘ 𝑡 ) ∈ dom adjℎ → ( adjℎ ‘ ( adjℎ ‘ 𝑡 ) ) ∈ LinOp )
4	2 3	syl	⊢ ( 𝑡 ∈ dom adjℎ → ( adjℎ ‘ ( adjℎ ‘ 𝑡 ) ) ∈ LinOp )
5	1 4	eqeltrrd	⊢ ( 𝑡 ∈ dom adjℎ → 𝑡 ∈ LinOp )
6	5	ssriv	⊢ dom adjℎ ⊆ LinOp