Metamath Proof Explorer

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 h ⊆ LinOp

Proof

Step Hyp Ref Expression
1 adjadj ⊢ t ∈ dom ⁡ adj h → adj h ⁡ adj h ⁡ t = t
2 dmadjrn ⊢ t ∈ dom ⁡ adj h → adj h ⁡ t ∈ dom ⁡ adj h
3 adjlnop ⊢ adj h ⁡ t ∈ dom ⁡ adj h → adj h ⁡ adj h ⁡ t ∈ LinOp
4 2 3 syl ⊢ t ∈ dom ⁡ adj h → adj h ⁡ adj h ⁡ t ∈ LinOp
5 1 4 eqeltrrd ⊢ t ∈ dom ⁡ adj h → t ∈ LinOp
6 5 ssriv ⊢ dom ⁡ adj h ⊆ LinOp