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 adjh C_ LinOp

Proof

Step Hyp Ref Expression
1 adjadj 
 |-  ( t e. dom adjh -> ( adjh ` ( adjh ` t ) ) = t )
2 dmadjrn 
 |-  ( t e. dom adjh -> ( adjh ` t ) e. dom adjh )
3 adjlnop 
 |-  ( ( adjh ` t ) e. dom adjh -> ( adjh ` ( adjh ` t ) ) e. LinOp )
4 2 3 syl 
 |-  ( t e. dom adjh -> ( adjh ` ( adjh ` t ) ) e. LinOp )
5 1 4 eqeltrrd 
 |-  ( t e. dom adjh -> t e. LinOp )
6 5 ssriv 
 |-  dom adjh C_ LinOp