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 ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) → ( adjℎ ‘ ( 𝑆 +op 𝑇 ) ) = ( ( adjℎ ‘ 𝑆 ) +op ( adjℎ ‘ 𝑇 ) ) )

Proof

Step Hyp Ref Expression
1 dmadjop ⊢ ( 𝑆 ∈ dom adjℎ → 𝑆 : ℋ ⟶ ℋ )
2 dmadjop ⊢ ( 𝑇 ∈ dom adjℎ → 𝑇 : ℋ ⟶ ℋ )
3 hoaddcl ⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑆 +op 𝑇 ) : ℋ ⟶ ℋ )
4 1 2 3 syl2an ⊢ ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) → ( 𝑆 +op 𝑇 ) : ℋ ⟶ ℋ )
5 dmadjrn ⊢ ( 𝑆 ∈ dom adjℎ → ( adjℎ ‘ 𝑆 ) ∈ dom adjℎ )
6 dmadjop ⊢ ( ( adjℎ ‘ 𝑆 ) ∈ dom adjℎ → ( adjℎ ‘ 𝑆 ) : ℋ ⟶ ℋ )
7 5 6 syl ⊢ ( 𝑆 ∈ dom adjℎ → ( adjℎ ‘ 𝑆 ) : ℋ ⟶ ℋ )
8 dmadjrn ⊢ ( 𝑇 ∈ dom adjℎ → ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ )
9 dmadjop ⊢ ( ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ → ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ )
10 8 9 syl ⊢ ( 𝑇 ∈ dom adjℎ → ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ )
11 hoaddcl ⊢ ( ( ( adjℎ ‘ 𝑆 ) : ℋ ⟶ ℋ ∧ ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ ) → ( ( adjℎ ‘ 𝑆 ) +op ( adjℎ ‘ 𝑇 ) ) : ℋ ⟶ ℋ )
12 7 10 11 syl2an ⊢ ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) → ( ( adjℎ ‘ 𝑆 ) +op ( adjℎ ‘ 𝑇 ) ) : ℋ ⟶ ℋ )
13 adj2 ⊢ ( ( 𝑆 ∈ dom adjℎ ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ( adjℎ ‘ 𝑆 ) ‘ 𝑦 ) ) )
14 13 3expb ⊢ ( ( 𝑆 ∈ dom adjℎ ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ( adjℎ ‘ 𝑆 ) ‘ 𝑦 ) ) )
15 14 adantlr ⊢ ( ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ( adjℎ ‘ 𝑆 ) ‘ 𝑦 ) ) )
16 adj2 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) )
17 16 3expb ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) )
18 17 adantll ⊢ ( ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) )
19 15 18 oveq12d ⊢ ( ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) + ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ) = ( ( 𝑥 ·ih ( ( adjℎ ‘ 𝑆 ) ‘ 𝑦 ) ) + ( 𝑥 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ) )
20 1 ffvelrnda ⊢ ( ( 𝑆 ∈ dom adjℎ ∧ 𝑥 ∈ ℋ ) → ( 𝑆 ‘ 𝑥 ) ∈ ℋ )
21 20 ad2ant2r ⊢ ( ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑆 ‘ 𝑥 ) ∈ ℋ )
22 2 ffvelrnda ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
23 22 ad2ant2lr ⊢ ( ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
24 simprr ⊢ ( ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → 𝑦 ∈ ℋ )
25 ax-his2 ⊢ ( ( ( 𝑆 ‘ 𝑥 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) ·ih 𝑦 ) = ( ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) + ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ) )
26 21 23 24 25 syl3anc ⊢ ( ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) ·ih 𝑦 ) = ( ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑦 ) + ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ) )
27 simprl ⊢ ( ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → 𝑥 ∈ ℋ )
28 adjcl ⊢ ( ( 𝑆 ∈ dom adjℎ ∧ 𝑦 ∈ ℋ ) → ( ( adjℎ ‘ 𝑆 ) ‘ 𝑦 ) ∈ ℋ )
29 28 ad2ant2rl ⊢ ( ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( adjℎ ‘ 𝑆 ) ‘ 𝑦 ) ∈ ℋ )
30 adjcl ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑦 ∈ ℋ ) → ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ∈ ℋ )
31 30 ad2ant2l ⊢ ( ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ∈ ℋ )
32 his7 ⊢ ( ( 𝑥 ∈ ℋ ∧ ( ( adjℎ ‘ 𝑆 ) ‘ 𝑦 ) ∈ ℋ ∧ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ∈ ℋ ) → ( 𝑥 ·ih ( ( ( adjℎ ‘ 𝑆 ) ‘ 𝑦 ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ) = ( ( 𝑥 ·ih ( ( adjℎ ‘ 𝑆 ) ‘ 𝑦 ) ) + ( 𝑥 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ) )
33 27 29 31 32 syl3anc ⊢ ( ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ih ( ( ( adjℎ ‘ 𝑆 ) ‘ 𝑦 ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ) = ( ( 𝑥 ·ih ( ( adjℎ ‘ 𝑆 ) ‘ 𝑦 ) ) + ( 𝑥 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ) )
34 19 26 33 3eqtr4rd ⊢ ( ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ih ( ( ( adjℎ ‘ 𝑆 ) ‘ 𝑦 ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ) = ( ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) ·ih 𝑦 ) )
35 7 10 anim12i ⊢ ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) → ( ( adjℎ ‘ 𝑆 ) : ℋ ⟶ ℋ ∧ ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ ) )
36 hosval ⊢ ( ( ( adjℎ ‘ 𝑆 ) : ℋ ⟶ ℋ ∧ ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( adjℎ ‘ 𝑆 ) +op ( adjℎ ‘ 𝑇 ) ) ‘ 𝑦 ) = ( ( ( adjℎ ‘ 𝑆 ) ‘ 𝑦 ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) )
37 36 3expa ⊢ ( ( ( ( adjℎ ‘ 𝑆 ) : ℋ ⟶ ℋ ∧ ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ ) ∧ 𝑦 ∈ ℋ ) → ( ( ( adjℎ ‘ 𝑆 ) +op ( adjℎ ‘ 𝑇 ) ) ‘ 𝑦 ) = ( ( ( adjℎ ‘ 𝑆 ) ‘ 𝑦 ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) )
38 35 37 sylan ⊢ ( ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) ∧ 𝑦 ∈ ℋ ) → ( ( ( adjℎ ‘ 𝑆 ) +op ( adjℎ ‘ 𝑇 ) ) ‘ 𝑦 ) = ( ( ( adjℎ ‘ 𝑆 ) ‘ 𝑦 ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) )
39 38 adantrl ⊢ ( ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( ( adjℎ ‘ 𝑆 ) +op ( adjℎ ‘ 𝑇 ) ) ‘ 𝑦 ) = ( ( ( adjℎ ‘ 𝑆 ) ‘ 𝑦 ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) )
40 39 oveq2d ⊢ ( ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ih ( ( ( adjℎ ‘ 𝑆 ) +op ( adjℎ ‘ 𝑇 ) ) ‘ 𝑦 ) ) = ( 𝑥 ·ih ( ( ( adjℎ ‘ 𝑆 ) ‘ 𝑦 ) +ℎ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ) )
41 1 2 anim12i ⊢ ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) → ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) )
42 hosval ⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) )
43 42 3expa ⊢ ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) )
44 41 43 sylan ⊢ ( ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) )
45 44 adantrr ⊢ ( ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) )
46 45 oveq1d ⊢ ( ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) = ( ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) ·ih 𝑦 ) )
47 34 40 46 3eqtr4rd ⊢ ( ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ( ( adjℎ ‘ 𝑆 ) +op ( adjℎ ‘ 𝑇 ) ) ‘ 𝑦 ) ) )
48 47 ralrimivva ⊢ ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) → ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ( ( adjℎ ‘ 𝑆 ) +op ( adjℎ ‘ 𝑇 ) ) ‘ 𝑦 ) ) )
49 adjeq ⊢ ( ( ( 𝑆 +op 𝑇 ) : ℋ ⟶ ℋ ∧ ( ( adjℎ ‘ 𝑆 ) +op ( adjℎ ‘ 𝑇 ) ) : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ( ( adjℎ ‘ 𝑆 ) +op ( adjℎ ‘ 𝑇 ) ) ‘ 𝑦 ) ) ) → ( adjℎ ‘ ( 𝑆 +op 𝑇 ) ) = ( ( adjℎ ‘ 𝑆 ) +op ( adjℎ ‘ 𝑇 ) ) )
50 4 12 48 49 syl3anc ⊢ ( ( 𝑆 ∈ dom adjℎ ∧ 𝑇 ∈ dom adjℎ ) → ( adjℎ ‘ ( 𝑆 +op 𝑇 ) ) = ( ( adjℎ ‘ 𝑆 ) +op ( adjℎ ‘ 𝑇 ) ) )