Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . . . . 6
โข (((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ ๐ด โ
โ) |
2 | | ffvelcdm 7033 |
. . . . . . 7
โข ((๐: โโถ โ โง
๐ฅ โ โ) โ
(๐โ๐ฅ) โ โ) |
3 | 2 | 3ad2antl2 1187 |
. . . . . 6
โข (((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ (๐โ๐ฅ) โ
โ) |
4 | | ffvelcdm 7033 |
. . . . . . 7
โข ((๐: โโถ โ โง
๐ฅ โ โ) โ
(๐โ๐ฅ) โ โ) |
5 | 4 | 3ad2antl3 1188 |
. . . . . 6
โข (((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ (๐โ๐ฅ) โ
โ) |
6 | | ax-hvdistr1 29992 |
. . . . . 6
โข ((๐ด โ โ โง (๐โ๐ฅ) โ โ โง (๐โ๐ฅ) โ โ) โ (๐ด ยทโ ((๐โ๐ฅ) +โ (๐โ๐ฅ))) = ((๐ด ยทโ (๐โ๐ฅ)) +โ (๐ด ยทโ (๐โ๐ฅ)))) |
7 | 1, 3, 5, 6 | syl3anc 1372 |
. . . . 5
โข (((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ (๐ด
ยทโ ((๐โ๐ฅ) +โ (๐โ๐ฅ))) = ((๐ด ยทโ (๐โ๐ฅ)) +โ (๐ด ยทโ (๐โ๐ฅ)))) |
8 | | hosval 30724 |
. . . . . . . 8
โข ((๐: โโถ โ โง
๐: โโถ โ
โง ๐ฅ โ โ)
โ ((๐ +op
๐)โ๐ฅ) = ((๐โ๐ฅ) +โ (๐โ๐ฅ))) |
9 | 8 | oveq2d 7374 |
. . . . . . 7
โข ((๐: โโถ โ โง
๐: โโถ โ
โง ๐ฅ โ โ)
โ (๐ด
ยทโ ((๐ +op ๐)โ๐ฅ)) = (๐ด ยทโ ((๐โ๐ฅ) +โ (๐โ๐ฅ)))) |
10 | 9 | 3expa 1119 |
. . . . . 6
โข (((๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ (๐ด
ยทโ ((๐ +op ๐)โ๐ฅ)) = (๐ด ยทโ ((๐โ๐ฅ) +โ (๐โ๐ฅ)))) |
11 | 10 | 3adantl1 1167 |
. . . . 5
โข (((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ (๐ด
ยทโ ((๐ +op ๐)โ๐ฅ)) = (๐ด ยทโ ((๐โ๐ฅ) +โ (๐โ๐ฅ)))) |
12 | | homval 30725 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐: โโถ โ โง
๐ฅ โ โ) โ
((๐ด
ยทop ๐)โ๐ฅ) = (๐ด ยทโ (๐โ๐ฅ))) |
13 | 12 | 3expa 1119 |
. . . . . . 7
โข (((๐ด โ โ โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
((๐ด
ยทop ๐)โ๐ฅ) = (๐ด ยทโ (๐โ๐ฅ))) |
14 | 13 | 3adantl3 1169 |
. . . . . 6
โข (((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ ((๐ด
ยทop ๐)โ๐ฅ) = (๐ด ยทโ (๐โ๐ฅ))) |
15 | | homval 30725 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐: โโถ โ โง
๐ฅ โ โ) โ
((๐ด
ยทop ๐)โ๐ฅ) = (๐ด ยทโ (๐โ๐ฅ))) |
16 | 15 | 3expa 1119 |
. . . . . . 7
โข (((๐ด โ โ โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
((๐ด
ยทop ๐)โ๐ฅ) = (๐ด ยทโ (๐โ๐ฅ))) |
17 | 16 | 3adantl2 1168 |
. . . . . 6
โข (((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ ((๐ด
ยทop ๐)โ๐ฅ) = (๐ด ยทโ (๐โ๐ฅ))) |
18 | 14, 17 | oveq12d 7376 |
. . . . 5
โข (((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ (((๐ด
ยทop ๐)โ๐ฅ) +โ ((๐ด ยทop ๐)โ๐ฅ)) = ((๐ด ยทโ (๐โ๐ฅ)) +โ (๐ด ยทโ (๐โ๐ฅ)))) |
19 | 7, 11, 18 | 3eqtr4d 2783 |
. . . 4
โข (((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ (๐ด
ยทโ ((๐ +op ๐)โ๐ฅ)) = (((๐ด ยทop ๐)โ๐ฅ) +โ ((๐ด ยทop ๐)โ๐ฅ))) |
20 | | hoaddcl 30742 |
. . . . . . 7
โข ((๐: โโถ โ โง
๐: โโถ โ)
โ (๐ +op
๐): โโถ
โ) |
21 | 20 | anim2i 618 |
. . . . . 6
โข ((๐ด โ โ โง (๐: โโถ โ โง
๐: โโถ
โ)) โ (๐ด โ
โ โง (๐
+op ๐):
โโถ โ)) |
22 | 21 | 3impb 1116 |
. . . . 5
โข ((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โ (๐ด โ โ
โง (๐ +op
๐): โโถ
โ)) |
23 | | homval 30725 |
. . . . . 6
โข ((๐ด โ โ โง (๐ +op ๐): โโถ โ โง
๐ฅ โ โ) โ
((๐ด
ยทop (๐ +op ๐))โ๐ฅ) = (๐ด ยทโ ((๐ +op ๐)โ๐ฅ))) |
24 | 23 | 3expa 1119 |
. . . . 5
โข (((๐ด โ โ โง (๐ +op ๐): โโถ โ)
โง ๐ฅ โ โ)
โ ((๐ด
ยทop (๐ +op ๐))โ๐ฅ) = (๐ด ยทโ ((๐ +op ๐)โ๐ฅ))) |
25 | 22, 24 | sylan 581 |
. . . 4
โข (((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ ((๐ด
ยทop (๐ +op ๐))โ๐ฅ) = (๐ด ยทโ ((๐ +op ๐)โ๐ฅ))) |
26 | | homulcl 30743 |
. . . . . . 7
โข ((๐ด โ โ โง ๐: โโถ โ)
โ (๐ด
ยทop ๐): โโถ โ) |
27 | | homulcl 30743 |
. . . . . . 7
โข ((๐ด โ โ โง ๐: โโถ โ)
โ (๐ด
ยทop ๐): โโถ โ) |
28 | 26, 27 | anim12i 614 |
. . . . . 6
โข (((๐ด โ โ โง ๐: โโถ โ) โง
(๐ด โ โ โง
๐: โโถ
โ)) โ ((๐ด
ยทop ๐): โโถ โ โง (๐ด ยทop
๐): โโถ
โ)) |
29 | 28 | 3impdi 1351 |
. . . . 5
โข ((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โ ((๐ด
ยทop ๐): โโถ โ โง (๐ด ยทop
๐): โโถ
โ)) |
30 | | hosval 30724 |
. . . . . 6
โข (((๐ด ยทop
๐): โโถ โ
โง (๐ด
ยทop ๐): โโถ โ โง ๐ฅ โ โ) โ (((๐ด ยทop
๐) +op (๐ด ยทop
๐))โ๐ฅ) = (((๐ด ยทop ๐)โ๐ฅ) +โ ((๐ด ยทop ๐)โ๐ฅ))) |
31 | 30 | 3expa 1119 |
. . . . 5
โข ((((๐ด ยทop
๐): โโถ โ
โง (๐ด
ยทop ๐): โโถ โ) โง ๐ฅ โ โ) โ (((๐ด ยทop
๐) +op (๐ด ยทop
๐))โ๐ฅ) = (((๐ด ยทop ๐)โ๐ฅ) +โ ((๐ด ยทop ๐)โ๐ฅ))) |
32 | 29, 31 | sylan 581 |
. . . 4
โข (((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ (((๐ด
ยทop ๐) +op (๐ด ยทop ๐))โ๐ฅ) = (((๐ด ยทop ๐)โ๐ฅ) +โ ((๐ด ยทop ๐)โ๐ฅ))) |
33 | 19, 25, 32 | 3eqtr4d 2783 |
. . 3
โข (((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ ((๐ด
ยทop (๐ +op ๐))โ๐ฅ) = (((๐ด ยทop ๐) +op (๐ด ยทop
๐))โ๐ฅ)) |
34 | 33 | ralrimiva 3140 |
. 2
โข ((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โ โ๐ฅ โ
โ ((๐ด
ยทop (๐ +op ๐))โ๐ฅ) = (((๐ด ยทop ๐) +op (๐ด ยทop
๐))โ๐ฅ)) |
35 | | homulcl 30743 |
. . . . 5
โข ((๐ด โ โ โง (๐ +op ๐): โโถ โ)
โ (๐ด
ยทop (๐ +op ๐)): โโถ
โ) |
36 | 20, 35 | sylan2 594 |
. . . 4
โข ((๐ด โ โ โง (๐: โโถ โ โง
๐: โโถ
โ)) โ (๐ด
ยทop (๐ +op ๐)): โโถ
โ) |
37 | 36 | 3impb 1116 |
. . 3
โข ((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โ (๐ด
ยทop (๐ +op ๐)): โโถ
โ) |
38 | | hoaddcl 30742 |
. . . . 5
โข (((๐ด ยทop
๐): โโถ โ
โง (๐ด
ยทop ๐): โโถ โ) โ ((๐ด ยทop
๐) +op (๐ด ยทop
๐)): โโถ
โ) |
39 | 26, 27, 38 | syl2an 597 |
. . . 4
โข (((๐ด โ โ โง ๐: โโถ โ) โง
(๐ด โ โ โง
๐: โโถ
โ)) โ ((๐ด
ยทop ๐) +op (๐ด ยทop ๐)): โโถ
โ) |
40 | 39 | 3impdi 1351 |
. . 3
โข ((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โ ((๐ด
ยทop ๐) +op (๐ด ยทop ๐)): โโถ
โ) |
41 | | hoeq 30744 |
. . 3
โข (((๐ด ยทop
(๐ +op ๐)): โโถ โ
โง ((๐ด
ยทop ๐) +op (๐ด ยทop ๐)): โโถ โ)
โ (โ๐ฅ โ
โ ((๐ด
ยทop (๐ +op ๐))โ๐ฅ) = (((๐ด ยทop ๐) +op (๐ด ยทop
๐))โ๐ฅ) โ (๐ด ยทop (๐ +op ๐)) = ((๐ด ยทop ๐) +op (๐ด ยทop
๐)))) |
42 | 37, 40, 41 | syl2anc 585 |
. 2
โข ((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โ (โ๐ฅ โ
โ ((๐ด
ยทop (๐ +op ๐))โ๐ฅ) = (((๐ด ยทop ๐) +op (๐ด ยทop
๐))โ๐ฅ) โ (๐ด ยทop (๐ +op ๐)) = ((๐ด ยทop ๐) +op (๐ด ยทop
๐)))) |
43 | 34, 42 | mpbid 231 |
1
โข ((๐ด โ โ โง ๐: โโถ โ โง
๐: โโถ โ)
โ (๐ด
ยทop (๐ +op ๐)) = ((๐ด ยทop ๐) +op (๐ด ยทop
๐))) |