Metamath Proof Explorer

Theorem adjadd

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
Assertion adjadd 
|- ( ( S e. dom adjh /\ T e. dom adjh ) -> ( adjh ` ( S +op T ) ) = ( ( adjh ` S ) +op ( adjh ` T ) ) )

Proof

Step Hyp Ref Expression
1 dmadjop 
 |-  ( S e. dom adjh -> S : ~H --> ~H )
2 dmadjop 
 |-  ( T e. dom adjh -> T : ~H --> ~H )
3 hoaddcl 
 |-  ( ( 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 )
5 dmadjrn 
 |-  ( S e. dom adjh -> ( adjh ` S ) e. dom adjh )
6 dmadjop 
 |-  ( ( adjh ` S ) e. dom adjh -> ( adjh ` S ) : ~H --> ~H )
7 5 6 syl 
 |-  ( S e. dom adjh -> ( adjh ` S ) : ~H --> ~H )
8 dmadjrn 
 |-  ( T e. dom adjh -> ( adjh ` T ) e. dom adjh )
9 dmadjop 
 |-  ( ( adjh ` T ) e. dom adjh -> ( adjh ` T ) : ~H --> ~H )
10 8 9 syl 
 |-  ( T e. dom adjh -> ( adjh ` T ) : ~H --> ~H )
11 hoaddcl 
 |-  ( ( ( 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 )
13 adj2 
 |-  ( ( 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 ) ) )
15 14 adantlr 
 |-  ( ( ( S e. dom adjh /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( S ` x ) .ih y ) = ( x .ih ( ( adjh ` S ) ` y ) ) )
16 adj2 
 |-  ( ( 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 ) ) )
18 17 adantll 
 |-  ( ( ( 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 )
21 20 ad2ant2r 
 |-  ( ( ( 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 )
23 22 ad2ant2lr 
 |-  ( ( ( 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 )
28 adjcl 
 |-  ( ( S e. dom adjh /\ y e. ~H ) -> ( ( adjh ` S ) ` y ) e. ~H )
29 28 ad2ant2rl 
 |-  ( ( ( S e. dom adjh /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( adjh ` S ) ` y ) e. ~H )
30 adjcl 
 |-  ( ( T e. dom adjh /\ y e. ~H ) -> ( ( adjh ` T ) ` y ) e. ~H )
31 30 ad2ant2l 
 |-  ( ( ( 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 ) ) )
39 38 adantrl 
 |-  ( ( ( 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 ) ) )
45 44 adantrr 
 |-  ( ( ( S e. dom adjh /\ T e. dom adjh ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( S +op T ) ` x ) = ( ( S ` x ) +h ( T ` x ) ) )
46 45 oveq1d 
 |-  ( ( ( 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 ) )
47 34 40 46 3eqtr4rd 
 |-  ( ( ( 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 ) ) )
48 47 ralrimivva 
 |-  ( ( 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 ) ) )
49 adjeq 
 |-  ( ( ( 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 ) ) )
50 4 12 48 49 syl3anc 
 |-  ( ( S e. dom adjh /\ T e. dom adjh ) -> ( adjh ` ( S +op T ) ) = ( ( adjh ` S ) +op ( adjh ` T ) ) )