Step | Hyp | Ref
| Expression |
1 | | neg1cn 12272 |
. . . . 5
โข -1 โ
โ |
2 | | hvmulcl 29997 |
. . . . 5
โข ((-1
โ โ โง ๐ถ
โ โ) โ (-1 ยทโ ๐ถ) โ โ) |
3 | 1, 2 | mpan 689 |
. . . 4
โข (๐ถ โ โ โ (-1
ยทโ ๐ถ) โ โ) |
4 | | ax-hvdistr1 29992 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง (-1
ยทโ ๐ถ) โ โ) โ (๐ด ยทโ (๐ต +โ (-1
ยทโ ๐ถ))) = ((๐ด ยทโ ๐ต) +โ (๐ด
ยทโ (-1 ยทโ ๐ถ)))) |
5 | 3, 4 | syl3an3 1166 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด
ยทโ (๐ต +โ (-1
ยทโ ๐ถ))) = ((๐ด ยทโ ๐ต) +โ (๐ด
ยทโ (-1 ยทโ ๐ถ)))) |
6 | | hvmulcom 30027 |
. . . . . 6
โข ((๐ด โ โ โง -1 โ
โ โง ๐ถ โ
โ) โ (๐ด
ยทโ (-1 ยทโ ๐ถ)) = (-1
ยทโ (๐ด ยทโ ๐ถ))) |
7 | 1, 6 | mp3an2 1450 |
. . . . 5
โข ((๐ด โ โ โง ๐ถ โ โ) โ (๐ด
ยทโ (-1 ยทโ ๐ถ)) = (-1
ยทโ (๐ด ยทโ ๐ถ))) |
8 | 7 | oveq2d 7374 |
. . . 4
โข ((๐ด โ โ โง ๐ถ โ โ) โ ((๐ด
ยทโ ๐ต) +โ (๐ด ยทโ (-1
ยทโ ๐ถ))) = ((๐ด ยทโ ๐ต) +โ (-1
ยทโ (๐ด ยทโ ๐ถ)))) |
9 | 8 | 3adant2 1132 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด
ยทโ ๐ต) +โ (๐ด ยทโ (-1
ยทโ ๐ถ))) = ((๐ด ยทโ ๐ต) +โ (-1
ยทโ (๐ด ยทโ ๐ถ)))) |
10 | 5, 9 | eqtrd 2773 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด
ยทโ (๐ต +โ (-1
ยทโ ๐ถ))) = ((๐ด ยทโ ๐ต) +โ (-1
ยทโ (๐ด ยทโ ๐ถ)))) |
11 | | hvsubval 30000 |
. . . 4
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต โโ
๐ถ) = (๐ต +โ (-1
ยทโ ๐ถ))) |
12 | 11 | 3adant1 1131 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ต โโ
๐ถ) = (๐ต +โ (-1
ยทโ ๐ถ))) |
13 | 12 | oveq2d 7374 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด
ยทโ (๐ต โโ ๐ถ)) = (๐ด ยทโ (๐ต +โ (-1
ยทโ ๐ถ)))) |
14 | | hvmulcl 29997 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด
ยทโ ๐ต) โ โ) |
15 | 14 | 3adant3 1133 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด
ยทโ ๐ต) โ โ) |
16 | | hvmulcl 29997 |
. . . 4
โข ((๐ด โ โ โง ๐ถ โ โ) โ (๐ด
ยทโ ๐ถ) โ โ) |
17 | 16 | 3adant2 1132 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด
ยทโ ๐ถ) โ โ) |
18 | | hvsubval 30000 |
. . 3
โข (((๐ด
ยทโ ๐ต) โ โ โง (๐ด ยทโ ๐ถ) โ โ) โ ((๐ด
ยทโ ๐ต) โโ (๐ด
ยทโ ๐ถ)) = ((๐ด ยทโ ๐ต) +โ (-1
ยทโ (๐ด ยทโ ๐ถ)))) |
19 | 15, 17, 18 | syl2anc 585 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด
ยทโ ๐ต) โโ (๐ด
ยทโ ๐ถ)) = ((๐ด ยทโ ๐ต) +โ (-1
ยทโ (๐ด ยทโ ๐ถ)))) |
20 | 10, 13, 19 | 3eqtr4d 2783 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด
ยทโ (๐ต โโ ๐ถ)) = ((๐ด ยทโ ๐ต) โโ
(๐ด
ยทโ ๐ถ))) |