Step | Hyp | Ref
| Expression |
1 | | hvmulcl 29997 |
. . . 4
โข ((๐ด โ โ โง ๐ถ โ โ) โ (๐ด
ยทโ ๐ถ) โ โ) |
2 | 1 | 3adant2 1132 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด
ยทโ ๐ถ) โ โ) |
3 | | hvmulcl 29997 |
. . . 4
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต
ยทโ ๐ถ) โ โ) |
4 | 3 | 3adant1 1131 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ต
ยทโ ๐ถ) โ โ) |
5 | | hvsubval 30000 |
. . 3
โข (((๐ด
ยทโ ๐ถ) โ โ โง (๐ต ยทโ ๐ถ) โ โ) โ ((๐ด
ยทโ ๐ถ) โโ (๐ต
ยทโ ๐ถ)) = ((๐ด ยทโ ๐ถ) +โ (-1
ยทโ (๐ต ยทโ ๐ถ)))) |
6 | 2, 4, 5 | syl2anc 585 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด
ยทโ ๐ถ) โโ (๐ต
ยทโ ๐ถ)) = ((๐ด ยทโ ๐ถ) +โ (-1
ยทโ (๐ต ยทโ ๐ถ)))) |
7 | | mulm1 11601 |
. . . . . . 7
โข (๐ต โ โ โ (-1
ยท ๐ต) = -๐ต) |
8 | 7 | oveq1d 7373 |
. . . . . 6
โข (๐ต โ โ โ ((-1
ยท ๐ต)
ยทโ ๐ถ) = (-๐ต ยทโ ๐ถ)) |
9 | 8 | adantr 482 |
. . . . 5
โข ((๐ต โ โ โง ๐ถ โ โ) โ ((-1
ยท ๐ต)
ยทโ ๐ถ) = (-๐ต ยทโ ๐ถ)) |
10 | | neg1cn 12272 |
. . . . . 6
โข -1 โ
โ |
11 | | ax-hvmulass 29991 |
. . . . . 6
โข ((-1
โ โ โง ๐ต
โ โ โง ๐ถ
โ โ) โ ((-1 ยท ๐ต) ยทโ ๐ถ) = (-1
ยทโ (๐ต ยทโ ๐ถ))) |
12 | 10, 11 | mp3an1 1449 |
. . . . 5
โข ((๐ต โ โ โง ๐ถ โ โ) โ ((-1
ยท ๐ต)
ยทโ ๐ถ) = (-1 ยทโ
(๐ต
ยทโ ๐ถ))) |
13 | 9, 12 | eqtr3d 2775 |
. . . 4
โข ((๐ต โ โ โง ๐ถ โ โ) โ (-๐ต
ยทโ ๐ถ) = (-1 ยทโ
(๐ต
ยทโ ๐ถ))) |
14 | 13 | 3adant1 1131 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (-๐ต
ยทโ ๐ถ) = (-1 ยทโ
(๐ต
ยทโ ๐ถ))) |
15 | 14 | oveq2d 7374 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด
ยทโ ๐ถ) +โ (-๐ต ยทโ ๐ถ)) = ((๐ด ยทโ ๐ถ) +โ (-1
ยทโ (๐ต ยทโ ๐ถ)))) |
16 | | negcl 11406 |
. . . 4
โข (๐ต โ โ โ -๐ต โ
โ) |
17 | | ax-hvdistr2 29993 |
. . . 4
โข ((๐ด โ โ โง -๐ต โ โ โง ๐ถ โ โ) โ ((๐ด + -๐ต) ยทโ ๐ถ) = ((๐ด ยทโ ๐ถ) +โ (-๐ต
ยทโ ๐ถ))) |
18 | 16, 17 | syl3an2 1165 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด + -๐ต) ยทโ ๐ถ) = ((๐ด ยทโ ๐ถ) +โ (-๐ต
ยทโ ๐ถ))) |
19 | | negsub 11454 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + -๐ต) = (๐ด โ ๐ต)) |
20 | 19 | 3adant3 1133 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด + -๐ต) = (๐ด โ ๐ต)) |
21 | 20 | oveq1d 7373 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด + -๐ต) ยทโ ๐ถ) = ((๐ด โ ๐ต) ยทโ ๐ถ)) |
22 | 18, 21 | eqtr3d 2775 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด
ยทโ ๐ถ) +โ (-๐ต ยทโ ๐ถ)) = ((๐ด โ ๐ต) ยทโ ๐ถ)) |
23 | 6, 15, 22 | 3eqtr2rd 2780 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โ ๐ต) ยทโ ๐ถ) = ((๐ด ยทโ ๐ถ) โโ
(๐ต
ยทโ ๐ถ))) |