Step | Hyp | Ref
| Expression |
1 | | neg1cn 12275 |
. . . 4
โข -1 โ
โ |
2 | | hvmulcl 30004 |
. . . 4
โข ((-1
โ โ โง ๐ต
โ โ) โ (-1 ยทโ ๐ต) โ โ) |
3 | 1, 2 | mpan 689 |
. . 3
โข (๐ต โ โ โ (-1
ยทโ ๐ต) โ โ) |
4 | | hvaddsubass 30032 |
. . 3
โข ((๐ด โ โ โง (-1
ยทโ ๐ต) โ โ โง ๐ถ โ โ) โ ((๐ด +โ (-1
ยทโ ๐ต)) โโ ๐ถ) = (๐ด +โ ((-1
ยทโ ๐ต) โโ ๐ถ))) |
5 | 3, 4 | syl3an2 1165 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด +โ (-1
ยทโ ๐ต)) โโ ๐ถ) = (๐ด +โ ((-1
ยทโ ๐ต) โโ ๐ถ))) |
6 | | hvsubval 30007 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โโ
๐ต) = (๐ด +โ (-1
ยทโ ๐ต))) |
7 | 6 | 3adant3 1133 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด โโ
๐ต) = (๐ด +โ (-1
ยทโ ๐ต))) |
8 | 7 | oveq1d 7376 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โโ
๐ต)
โโ ๐ถ) = ((๐ด +โ (-1
ยทโ ๐ต)) โโ ๐ถ)) |
9 | | simp1 1137 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ด โ
โ) |
10 | | hvaddcl 30003 |
. . . . 5
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต +โ ๐ถ) โ
โ) |
11 | 10 | 3adant1 1131 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ต +โ ๐ถ) โ
โ) |
12 | | hvsubval 30007 |
. . . 4
โข ((๐ด โ โ โง (๐ต +โ ๐ถ) โ โ) โ (๐ด โโ
(๐ต +โ
๐ถ)) = (๐ด +โ (-1
ยทโ (๐ต +โ ๐ถ)))) |
13 | 9, 11, 12 | syl2anc 585 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด โโ
(๐ต +โ
๐ถ)) = (๐ด +โ (-1
ยทโ (๐ต +โ ๐ถ)))) |
14 | | hvsubval 30007 |
. . . . . . 7
โข (((-1
ยทโ ๐ต) โ โ โง ๐ถ โ โ) โ ((-1
ยทโ ๐ต) โโ ๐ถ) = ((-1
ยทโ ๐ต) +โ (-1
ยทโ ๐ถ))) |
15 | 3, 14 | sylan 581 |
. . . . . 6
โข ((๐ต โ โ โง ๐ถ โ โ) โ ((-1
ยทโ ๐ต) โโ ๐ถ) = ((-1
ยทโ ๐ต) +โ (-1
ยทโ ๐ถ))) |
16 | 15 | 3adant1 1131 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((-1
ยทโ ๐ต) โโ ๐ถ) = ((-1
ยทโ ๐ต) +โ (-1
ยทโ ๐ถ))) |
17 | | ax-hvdistr1 29999 |
. . . . . . 7
โข ((-1
โ โ โง ๐ต
โ โ โง ๐ถ
โ โ) โ (-1 ยทโ (๐ต +โ ๐ถ)) = ((-1
ยทโ ๐ต) +โ (-1
ยทโ ๐ถ))) |
18 | 1, 17 | mp3an1 1449 |
. . . . . 6
โข ((๐ต โ โ โง ๐ถ โ โ) โ (-1
ยทโ (๐ต +โ ๐ถ)) = ((-1 ยทโ
๐ต) +โ (-1
ยทโ ๐ถ))) |
19 | 18 | 3adant1 1131 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (-1
ยทโ (๐ต +โ ๐ถ)) = ((-1 ยทโ
๐ต) +โ (-1
ยทโ ๐ถ))) |
20 | 16, 19 | eqtr4d 2776 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((-1
ยทโ ๐ต) โโ ๐ถ) = (-1
ยทโ (๐ต +โ ๐ถ))) |
21 | 20 | oveq2d 7377 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด +โ ((-1
ยทโ ๐ต) โโ ๐ถ)) = (๐ด +โ (-1
ยทโ (๐ต +โ ๐ถ)))) |
22 | 13, 21 | eqtr4d 2776 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด โโ
(๐ต +โ
๐ถ)) = (๐ด +โ ((-1
ยทโ ๐ต) โโ ๐ถ))) |
23 | 5, 8, 22 | 3eqtr4d 2783 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โโ
๐ต)
โโ ๐ถ) = (๐ด โโ (๐ต +โ ๐ถ))) |