# Metamath Proof Explorer

Description: The adjoint of the sum of two operators. Theorem 3.11(iii) of Beran p. 106. (Contributed by NM, 22-Feb-2006) (New usage is discouraged.)

Ref Expression
`|- ( ( S e. dom adjh /\ T e. dom adjh ) -> ( adjh ` ( S +op T ) ) = ( ( adjh ` S ) +op ( adjh ` T ) ) )`

### Proof

Step Hyp Ref Expression
` |-  ( S e. dom adjh -> S : ~H --> ~H )`
` |-  ( T e. dom adjh -> T : ~H --> ~H )`
` |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S +op T ) : ~H --> ~H )`
4 1 2 3 syl2an
` |-  ( ( S e. dom adjh /\ T e. dom adjh ) -> ( S +op T ) : ~H --> ~H )`
` |-  ( S e. dom adjh -> ( adjh ` S ) e. dom adjh )`
` |-  ( ( adjh ` S ) e. dom adjh -> ( adjh ` S ) : ~H --> ~H )`
7 5 6 syl
` |-  ( S e. dom adjh -> ( adjh ` S ) : ~H --> ~H )`
` |-  ( T e. dom adjh -> ( adjh ` T ) e. dom adjh )`
` |-  ( ( adjh ` T ) e. dom adjh -> ( adjh ` T ) : ~H --> ~H )`
10 8 9 syl
` |-  ( T e. dom adjh -> ( adjh ` T ) : ~H --> ~H )`
` |-  ( ( ( adjh ` S ) : ~H --> ~H /\ ( adjh ` T ) : ~H --> ~H ) -> ( ( adjh ` S ) +op ( adjh ` T ) ) : ~H --> ~H )`
12 7 10 11 syl2an
` |-  ( ( S e. dom adjh /\ T e. dom adjh ) -> ( ( adjh ` S ) +op ( adjh ` T ) ) : ~H --> ~H )`
` |-  ( ( S e. dom adjh /\ x e. ~H /\ y e. ~H ) -> ( ( S ` x ) .ih y ) = ( x .ih ( ( adjh ` S ) ` y ) ) )`
14 13 3expb
` |-  ( ( S e. dom adjh /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( S ` x ) .ih y ) = ( x .ih ( ( adjh ` S ) ` y ) ) )`
` |-  ( ( ( S e. dom adjh /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( S ` x ) .ih y ) = ( x .ih ( ( adjh ` S ) ` y ) ) )`
` |-  ( ( T e. dom adjh /\ x e. ~H /\ y e. ~H ) -> ( ( T ` x ) .ih y ) = ( x .ih ( ( adjh ` T ) ` y ) ) )`
17 16 3expb
` |-  ( ( T e. dom adjh /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( T ` x ) .ih y ) = ( x .ih ( ( adjh ` T ) ` y ) ) )`
` |-  ( ( ( S e. dom adjh /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( T ` x ) .ih y ) = ( x .ih ( ( adjh ` T ) ` y ) ) )`
19 15 18 oveq12d
` |-  ( ( ( S e. dom adjh /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( S ` x ) .ih y ) + ( ( T ` x ) .ih y ) ) = ( ( x .ih ( ( adjh ` S ) ` y ) ) + ( x .ih ( ( adjh ` T ) ` y ) ) ) )`
20 1 ffvelrnda
` |-  ( ( S e. dom adjh /\ x e. ~H ) -> ( S ` x ) e. ~H )`
` |-  ( ( ( S e. dom adjh /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( S ` x ) e. ~H )`
22 2 ffvelrnda
` |-  ( ( T e. dom adjh /\ x e. ~H ) -> ( T ` x ) e. ~H )`
` |-  ( ( ( S e. dom adjh /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( T ` x ) e. ~H )`
24 simprr
` |-  ( ( ( S e. dom adjh /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> y e. ~H )`
25 ax-his2
` |-  ( ( ( S ` x ) e. ~H /\ ( T ` x ) e. ~H /\ y e. ~H ) -> ( ( ( S ` x ) +h ( T ` x ) ) .ih y ) = ( ( ( S ` x ) .ih y ) + ( ( T ` x ) .ih y ) ) )`
26 21 23 24 25 syl3anc
` |-  ( ( ( S e. dom adjh /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( S ` x ) +h ( T ` x ) ) .ih y ) = ( ( ( S ` x ) .ih y ) + ( ( T ` x ) .ih y ) ) )`
27 simprl
` |-  ( ( ( S e. dom adjh /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> x e. ~H )`
` |-  ( ( S e. dom adjh /\ y e. ~H ) -> ( ( adjh ` S ) ` y ) e. ~H )`
` |-  ( ( ( S e. dom adjh /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( adjh ` S ) ` y ) e. ~H )`
` |-  ( ( T e. dom adjh /\ y e. ~H ) -> ( ( adjh ` T ) ` y ) e. ~H )`
` |-  ( ( ( S e. dom adjh /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( adjh ` T ) ` y ) e. ~H )`
32 his7
` |-  ( ( x e. ~H /\ ( ( adjh ` S ) ` y ) e. ~H /\ ( ( adjh ` T ) ` y ) e. ~H ) -> ( x .ih ( ( ( adjh ` S ) ` y ) +h ( ( adjh ` T ) ` y ) ) ) = ( ( x .ih ( ( adjh ` S ) ` y ) ) + ( x .ih ( ( adjh ` T ) ` y ) ) ) )`
33 27 29 31 32 syl3anc
` |-  ( ( ( S e. dom adjh /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( ( ( adjh ` S ) ` y ) +h ( ( adjh ` T ) ` y ) ) ) = ( ( x .ih ( ( adjh ` S ) ` y ) ) + ( x .ih ( ( adjh ` T ) ` y ) ) ) )`
34 19 26 33 3eqtr4rd
` |-  ( ( ( S e. dom adjh /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( ( ( adjh ` S ) ` y ) +h ( ( adjh ` T ) ` y ) ) ) = ( ( ( S ` x ) +h ( T ` x ) ) .ih y ) )`
35 7 10 anim12i
` |-  ( ( S e. dom adjh /\ T e. dom adjh ) -> ( ( adjh ` S ) : ~H --> ~H /\ ( adjh ` T ) : ~H --> ~H ) )`
36 hosval
` |-  ( ( ( adjh ` S ) : ~H --> ~H /\ ( adjh ` T ) : ~H --> ~H /\ y e. ~H ) -> ( ( ( adjh ` S ) +op ( adjh ` T ) ) ` y ) = ( ( ( adjh ` S ) ` y ) +h ( ( adjh ` T ) ` y ) ) )`
37 36 3expa
` |-  ( ( ( ( adjh ` S ) : ~H --> ~H /\ ( adjh ` T ) : ~H --> ~H ) /\ y e. ~H ) -> ( ( ( adjh ` S ) +op ( adjh ` T ) ) ` y ) = ( ( ( adjh ` S ) ` y ) +h ( ( adjh ` T ) ` y ) ) )`
38 35 37 sylan
` |-  ( ( ( S e. dom adjh /\ T e. dom adjh ) /\ y e. ~H ) -> ( ( ( adjh ` S ) +op ( adjh ` T ) ) ` y ) = ( ( ( adjh ` S ) ` y ) +h ( ( adjh ` T ) ` y ) ) )`
` |-  ( ( ( S e. dom adjh /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( adjh ` S ) +op ( adjh ` T ) ) ` y ) = ( ( ( adjh ` S ) ` y ) +h ( ( adjh ` T ) ` y ) ) )`
40 39 oveq2d
` |-  ( ( ( S e. dom adjh /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( x .ih ( ( ( adjh ` S ) +op ( adjh ` T ) ) ` y ) ) = ( x .ih ( ( ( adjh ` S ) ` y ) +h ( ( adjh ` T ) ` y ) ) ) )`
41 1 2 anim12i
` |-  ( ( S e. dom adjh /\ T e. dom adjh ) -> ( S : ~H --> ~H /\ T : ~H --> ~H ) )`
42 hosval
` |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( S +op T ) ` x ) = ( ( S ` x ) +h ( T ` x ) ) )`
43 42 3expa
` |-  ( ( ( S : ~H --> ~H /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( S +op T ) ` x ) = ( ( S ` x ) +h ( T ` x ) ) )`
44 41 43 sylan
` |-  ( ( ( S e. dom adjh /\ T e. dom adjh ) /\ x e. ~H ) -> ( ( S +op T ) ` x ) = ( ( S ` x ) +h ( T ` x ) ) )`
` |-  ( ( ( S e. dom adjh /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( S +op T ) ` x ) = ( ( S ` x ) +h ( T ` x ) ) )`
` |-  ( ( ( S e. dom adjh /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( S +op T ) ` x ) .ih y ) = ( ( ( S ` x ) +h ( T ` x ) ) .ih y ) )`
` |-  ( ( ( S e. dom adjh /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( S +op T ) ` x ) .ih y ) = ( x .ih ( ( ( adjh ` S ) +op ( adjh ` T ) ) ` y ) ) )`
` |-  ( ( S e. dom adjh /\ T e. dom adjh ) -> A. x e. ~H A. y e. ~H ( ( ( S +op T ) ` x ) .ih y ) = ( x .ih ( ( ( adjh ` S ) +op ( adjh ` T ) ) ` y ) ) )`
` |-  ( ( ( S +op T ) : ~H --> ~H /\ ( ( adjh ` S ) +op ( adjh ` T ) ) : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( ( ( S +op T ) ` x ) .ih y ) = ( x .ih ( ( ( adjh ` S ) +op ( adjh ` T ) ) ` y ) ) ) -> ( adjh ` ( S +op T ) ) = ( ( adjh ` S ) +op ( adjh ` T ) ) )`
` |-  ( ( S e. dom adjh /\ T e. dom adjh ) -> ( adjh ` ( S +op T ) ) = ( ( adjh ` S ) +op ( adjh ` T ) ) )`