Step | Hyp | Ref
| Expression |
1 | | hvmulcl 30797 |
. . . 4
โข ((๐ด โ โ โง ๐ถ โ โ) โ (๐ด
ยทโ ๐ถ) โ โ) |
2 | 1 | 3adant2 1129 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด
ยทโ ๐ถ) โ โ) |
3 | | hvmulcl 30797 |
. . . 4
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต
ยทโ ๐ถ) โ โ) |
4 | 3 | 3adant1 1128 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ต
ยทโ ๐ถ) โ โ) |
5 | | hvsubval 30800 |
. . 3
โข (((๐ด
ยทโ ๐ถ) โ โ โง (๐ต ยทโ ๐ถ) โ โ) โ ((๐ด
ยทโ ๐ถ) โโ (๐ต
ยทโ ๐ถ)) = ((๐ด ยทโ ๐ถ) +โ (-1
ยทโ (๐ต ยทโ ๐ถ)))) |
6 | 2, 4, 5 | syl2anc 583 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด
ยทโ ๐ถ) โโ (๐ต
ยทโ ๐ถ)) = ((๐ด ยทโ ๐ถ) +โ (-1
ยทโ (๐ต ยทโ ๐ถ)))) |
7 | | mulm1 11671 |
. . . . . . 7
โข (๐ต โ โ โ (-1
ยท ๐ต) = -๐ต) |
8 | 7 | oveq1d 7429 |
. . . . . 6
โข (๐ต โ โ โ ((-1
ยท ๐ต)
ยทโ ๐ถ) = (-๐ต ยทโ ๐ถ)) |
9 | 8 | adantr 480 |
. . . . 5
โข ((๐ต โ โ โง ๐ถ โ โ) โ ((-1
ยท ๐ต)
ยทโ ๐ถ) = (-๐ต ยทโ ๐ถ)) |
10 | | neg1cn 12342 |
. . . . . 6
โข -1 โ
โ |
11 | | ax-hvmulass 30791 |
. . . . . 6
โข ((-1
โ โ โง ๐ต
โ โ โง ๐ถ
โ โ) โ ((-1 ยท ๐ต) ยทโ ๐ถ) = (-1
ยทโ (๐ต ยทโ ๐ถ))) |
12 | 10, 11 | mp3an1 1445 |
. . . . 5
โข ((๐ต โ โ โง ๐ถ โ โ) โ ((-1
ยท ๐ต)
ยทโ ๐ถ) = (-1 ยทโ
(๐ต
ยทโ ๐ถ))) |
13 | 9, 12 | eqtr3d 2769 |
. . . 4
โข ((๐ต โ โ โง ๐ถ โ โ) โ (-๐ต
ยทโ ๐ถ) = (-1 ยทโ
(๐ต
ยทโ ๐ถ))) |
14 | 13 | 3adant1 1128 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (-๐ต
ยทโ ๐ถ) = (-1 ยทโ
(๐ต
ยทโ ๐ถ))) |
15 | 14 | oveq2d 7430 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด
ยทโ ๐ถ) +โ (-๐ต ยทโ ๐ถ)) = ((๐ด ยทโ ๐ถ) +โ (-1
ยทโ (๐ต ยทโ ๐ถ)))) |
16 | | negcl 11476 |
. . . 4
โข (๐ต โ โ โ -๐ต โ
โ) |
17 | | ax-hvdistr2 30793 |
. . . 4
โข ((๐ด โ โ โง -๐ต โ โ โง ๐ถ โ โ) โ ((๐ด + -๐ต) ยทโ ๐ถ) = ((๐ด ยทโ ๐ถ) +โ (-๐ต
ยทโ ๐ถ))) |
18 | 16, 17 | syl3an2 1162 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด + -๐ต) ยทโ ๐ถ) = ((๐ด ยทโ ๐ถ) +โ (-๐ต
ยทโ ๐ถ))) |
19 | | negsub 11524 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + -๐ต) = (๐ด โ ๐ต)) |
20 | 19 | 3adant3 1130 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด + -๐ต) = (๐ด โ ๐ต)) |
21 | 20 | oveq1d 7429 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด + -๐ต) ยทโ ๐ถ) = ((๐ด โ ๐ต) ยทโ ๐ถ)) |
22 | 18, 21 | eqtr3d 2769 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด
ยทโ ๐ถ) +โ (-๐ต ยทโ ๐ถ)) = ((๐ด โ ๐ต) ยทโ ๐ถ)) |
23 | 6, 15, 22 | 3eqtr2rd 2774 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โ ๐ต) ยทโ ๐ถ) = ((๐ด ยทโ ๐ถ) โโ
(๐ต
ยทโ ๐ถ))) |