Step | Hyp | Ref
| Expression |
1 | | dmadjop 31396 |
. . 3
โข (๐ โ dom
adjโ โ ๐: โโถ โ) |
2 | | dmadjop 31396 |
. . 3
โข (๐ โ dom
adjโ โ ๐: โโถ โ) |
3 | | hoaddcl 31266 |
. . 3
โข ((๐: โโถ โ โง
๐: โโถ โ)
โ (๐ +op
๐): โโถ
โ) |
4 | 1, 2, 3 | syl2an 596 |
. 2
โข ((๐ โ dom
adjโ โง ๐ โ dom adjโ) โ
(๐ +op ๐): โโถ
โ) |
5 | | dmadjrn 31403 |
. . . 4
โข (๐ โ dom
adjโ โ (adjโโ๐) โ dom
adjโ) |
6 | | dmadjop 31396 |
. . . 4
โข
((adjโโ๐) โ dom adjโ โ
(adjโโ๐): โโถ โ) |
7 | 5, 6 | syl 17 |
. . 3
โข (๐ โ dom
adjโ โ (adjโโ๐): โโถ โ) |
8 | | dmadjrn 31403 |
. . . 4
โข (๐ โ dom
adjโ โ (adjโโ๐) โ dom
adjโ) |
9 | | dmadjop 31396 |
. . . 4
โข
((adjโโ๐) โ dom adjโ โ
(adjโโ๐): โโถ โ) |
10 | 8, 9 | syl 17 |
. . 3
โข (๐ โ dom
adjโ โ (adjโโ๐): โโถ โ) |
11 | | hoaddcl 31266 |
. . 3
โข
(((adjโโ๐): โโถ โ โง
(adjโโ๐): โโถ โ) โ
((adjโโ๐) +op
(adjโโ๐)): โโถ
โ) |
12 | 7, 10, 11 | syl2an 596 |
. 2
โข ((๐ โ dom
adjโ โง ๐ โ dom adjโ) โ
((adjโโ๐) +op
(adjโโ๐)): โโถ
โ) |
13 | | adj2 31442 |
. . . . . . . 8
โข ((๐ โ dom
adjโ โง ๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
((adjโโ๐)โ๐ฆ))) |
14 | 13 | 3expb 1120 |
. . . . . . 7
โข ((๐ โ dom
adjโ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
((adjโโ๐)โ๐ฆ))) |
15 | 14 | adantlr 713 |
. . . . . 6
โข (((๐ โ dom
adjโ โง ๐ โ dom adjโ) โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โ
((๐โ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih
((adjโโ๐)โ๐ฆ))) |
16 | | adj2 31442 |
. . . . . . . 8
โข ((๐ โ dom
adjโ โง ๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
((adjโโ๐)โ๐ฆ))) |
17 | 16 | 3expb 1120 |
. . . . . . 7
โข ((๐ โ dom
adjโ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
((adjโโ๐)โ๐ฆ))) |
18 | 17 | adantll 712 |
. . . . . 6
โข (((๐ โ dom
adjโ โง ๐ โ dom adjโ) โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โ
((๐โ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih
((adjโโ๐)โ๐ฆ))) |
19 | 15, 18 | oveq12d 7429 |
. . . . 5
โข (((๐ โ dom
adjโ โง ๐ โ dom adjโ) โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โ
(((๐โ๐ฅ)
ยทih ๐ฆ) + ((๐โ๐ฅ) ยทih ๐ฆ)) = ((๐ฅ ยทih
((adjโโ๐)โ๐ฆ)) + (๐ฅ ยทih
((adjโโ๐)โ๐ฆ)))) |
20 | 1 | ffvelcdmda 7086 |
. . . . . . 7
โข ((๐ โ dom
adjโ โง ๐ฅ โ โ) โ (๐โ๐ฅ) โ โ) |
21 | 20 | ad2ant2r 745 |
. . . . . 6
โข (((๐ โ dom
adjโ โง ๐ โ dom adjโ) โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โ
(๐โ๐ฅ) โ โ) |
22 | 2 | ffvelcdmda 7086 |
. . . . . . 7
โข ((๐ โ dom
adjโ โง ๐ฅ โ โ) โ (๐โ๐ฅ) โ โ) |
23 | 22 | ad2ant2lr 746 |
. . . . . 6
โข (((๐ โ dom
adjโ โง ๐ โ dom adjโ) โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โ
(๐โ๐ฅ) โ โ) |
24 | | simprr 771 |
. . . . . 6
โข (((๐ โ dom
adjโ โง ๐ โ dom adjโ) โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โ
๐ฆ โ
โ) |
25 | | ax-his2 30591 |
. . . . . 6
โข (((๐โ๐ฅ) โ โ โง (๐โ๐ฅ) โ โ โง ๐ฆ โ โ) โ (((๐โ๐ฅ) +โ (๐โ๐ฅ)) ยทih ๐ฆ) = (((๐โ๐ฅ) ยทih ๐ฆ) + ((๐โ๐ฅ) ยทih ๐ฆ))) |
26 | 21, 23, 24, 25 | syl3anc 1371 |
. . . . 5
โข (((๐ โ dom
adjโ โง ๐ โ dom adjโ) โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โ
(((๐โ๐ฅ) +โ (๐โ๐ฅ)) ยทih ๐ฆ) = (((๐โ๐ฅ) ยทih ๐ฆ) + ((๐โ๐ฅ) ยทih ๐ฆ))) |
27 | | simprl 769 |
. . . . . 6
โข (((๐ โ dom
adjโ โง ๐ โ dom adjโ) โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โ
๐ฅ โ
โ) |
28 | | adjcl 31440 |
. . . . . . 7
โข ((๐ โ dom
adjโ โง ๐ฆ โ โ) โ
((adjโโ๐)โ๐ฆ) โ โ) |
29 | 28 | ad2ant2rl 747 |
. . . . . 6
โข (((๐ โ dom
adjโ โง ๐ โ dom adjโ) โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โ
((adjโโ๐)โ๐ฆ) โ โ) |
30 | | adjcl 31440 |
. . . . . . 7
โข ((๐ โ dom
adjโ โง ๐ฆ โ โ) โ
((adjโโ๐)โ๐ฆ) โ โ) |
31 | 30 | ad2ant2l 744 |
. . . . . 6
โข (((๐ โ dom
adjโ โง ๐ โ dom adjโ) โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โ
((adjโโ๐)โ๐ฆ) โ โ) |
32 | | his7 30598 |
. . . . . 6
โข ((๐ฅ โ โ โง
((adjโโ๐)โ๐ฆ) โ โ โง
((adjโโ๐)โ๐ฆ) โ โ) โ (๐ฅ ยทih
(((adjโโ๐)โ๐ฆ) +โ
((adjโโ๐)โ๐ฆ))) = ((๐ฅ ยทih
((adjโโ๐)โ๐ฆ)) + (๐ฅ ยทih
((adjโโ๐)โ๐ฆ)))) |
33 | 27, 29, 31, 32 | syl3anc 1371 |
. . . . 5
โข (((๐ โ dom
adjโ โง ๐ โ dom adjโ) โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โ
(๐ฅ
ยทih (((adjโโ๐)โ๐ฆ) +โ
((adjโโ๐)โ๐ฆ))) = ((๐ฅ ยทih
((adjโโ๐)โ๐ฆ)) + (๐ฅ ยทih
((adjโโ๐)โ๐ฆ)))) |
34 | 19, 26, 33 | 3eqtr4rd 2783 |
. . . 4
โข (((๐ โ dom
adjโ โง ๐ โ dom adjโ) โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โ
(๐ฅ
ยทih (((adjโโ๐)โ๐ฆ) +โ
((adjโโ๐)โ๐ฆ))) = (((๐โ๐ฅ) +โ (๐โ๐ฅ)) ยทih ๐ฆ)) |
35 | 7, 10 | anim12i 613 |
. . . . . . 7
โข ((๐ โ dom
adjโ โง ๐ โ dom adjโ) โ
((adjโโ๐): โโถ โ โง
(adjโโ๐): โโถ
โ)) |
36 | | hosval 31248 |
. . . . . . . 8
โข
(((adjโโ๐): โโถ โ โง
(adjโโ๐): โโถ โ โง ๐ฆ โ โ) โ
(((adjโโ๐) +op
(adjโโ๐))โ๐ฆ) = (((adjโโ๐)โ๐ฆ) +โ
((adjโโ๐)โ๐ฆ))) |
37 | 36 | 3expa 1118 |
. . . . . . 7
โข
((((adjโโ๐): โโถ โ โง
(adjโโ๐): โโถ โ) โง ๐ฆ โ โ) โ
(((adjโโ๐) +op
(adjโโ๐))โ๐ฆ) = (((adjโโ๐)โ๐ฆ) +โ
((adjโโ๐)โ๐ฆ))) |
38 | 35, 37 | sylan 580 |
. . . . . 6
โข (((๐ โ dom
adjโ โง ๐ โ dom adjโ) โง
๐ฆ โ โ) โ
(((adjโโ๐) +op
(adjโโ๐))โ๐ฆ) = (((adjโโ๐)โ๐ฆ) +โ
((adjโโ๐)โ๐ฆ))) |
39 | 38 | adantrl 714 |
. . . . 5
โข (((๐ โ dom
adjโ โง ๐ โ dom adjโ) โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โ
(((adjโโ๐) +op
(adjโโ๐))โ๐ฆ) = (((adjโโ๐)โ๐ฆ) +โ
((adjโโ๐)โ๐ฆ))) |
40 | 39 | oveq2d 7427 |
. . . 4
โข (((๐ โ dom
adjโ โง ๐ โ dom adjโ) โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โ
(๐ฅ
ยทih (((adjโโ๐) +op
(adjโโ๐))โ๐ฆ)) = (๐ฅ ยทih
(((adjโโ๐)โ๐ฆ) +โ
((adjโโ๐)โ๐ฆ)))) |
41 | 1, 2 | anim12i 613 |
. . . . . . 7
โข ((๐ โ dom
adjโ โง ๐ โ dom adjโ) โ
(๐: โโถ โ
โง ๐: โโถ
โ)) |
42 | | hosval 31248 |
. . . . . . . 8
โข ((๐: โโถ โ โง
๐: โโถ โ
โง ๐ฅ โ โ)
โ ((๐ +op
๐)โ๐ฅ) = ((๐โ๐ฅ) +โ (๐โ๐ฅ))) |
43 | 42 | 3expa 1118 |
. . . . . . 7
โข (((๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ ((๐ +op
๐)โ๐ฅ) = ((๐โ๐ฅ) +โ (๐โ๐ฅ))) |
44 | 41, 43 | sylan 580 |
. . . . . 6
โข (((๐ โ dom
adjโ โง ๐ โ dom adjโ) โง
๐ฅ โ โ) โ
((๐ +op ๐)โ๐ฅ) = ((๐โ๐ฅ) +โ (๐โ๐ฅ))) |
45 | 44 | adantrr 715 |
. . . . 5
โข (((๐ โ dom
adjโ โง ๐ โ dom adjโ) โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โ
((๐ +op ๐)โ๐ฅ) = ((๐โ๐ฅ) +โ (๐โ๐ฅ))) |
46 | 45 | oveq1d 7426 |
. . . 4
โข (((๐ โ dom
adjโ โง ๐ โ dom adjโ) โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โ
(((๐ +op ๐)โ๐ฅ) ยทih ๐ฆ) = (((๐โ๐ฅ) +โ (๐โ๐ฅ)) ยทih ๐ฆ)) |
47 | 34, 40, 46 | 3eqtr4rd 2783 |
. . 3
โข (((๐ โ dom
adjโ โง ๐ โ dom adjโ) โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โ
(((๐ +op ๐)โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
(((adjโโ๐) +op
(adjโโ๐))โ๐ฆ))) |
48 | 47 | ralrimivva 3200 |
. 2
โข ((๐ โ dom
adjโ โง ๐ โ dom adjโ) โ
โ๐ฅ โ โ
โ๐ฆ โ โ
(((๐ +op ๐)โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
(((adjโโ๐) +op
(adjโโ๐))โ๐ฆ))) |
49 | | adjeq 31443 |
. 2
โข (((๐ +op ๐): โโถ โ โง
((adjโโ๐) +op
(adjโโ๐)): โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(((๐ +op ๐)โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
(((adjโโ๐) +op
(adjโโ๐))โ๐ฆ))) โ
(adjโโ(๐ +op ๐)) = ((adjโโ๐) +op
(adjโโ๐))) |
50 | 4, 12, 48, 49 | syl3anc 1371 |
1
โข ((๐ โ dom
adjโ โง ๐ โ dom adjโ) โ
(adjโโ(๐ +op ๐)) = ((adjโโ๐) +op
(adjโโ๐))) |