Step | Hyp | Ref
| Expression |
1 | | neg1cn 12325 |
. . . 4
โข -1 โ
โ |
2 | | hvmulcl 30261 |
. . . 4
โข ((-1
โ โ โง ๐ต
โ โ) โ (-1 ยทโ ๐ต) โ โ) |
3 | 1, 2 | mpan 688 |
. . 3
โข (๐ต โ โ โ (-1
ยทโ ๐ต) โ โ) |
4 | | hvaddsubass 30289 |
. . 3
โข ((๐ด โ โ โง (-1
ยทโ ๐ต) โ โ โง ๐ถ โ โ) โ ((๐ด +โ (-1
ยทโ ๐ต)) โโ ๐ถ) = (๐ด +โ ((-1
ยทโ ๐ต) โโ ๐ถ))) |
5 | 3, 4 | syl3an2 1164 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด +โ (-1
ยทโ ๐ต)) โโ ๐ถ) = (๐ด +โ ((-1
ยทโ ๐ต) โโ ๐ถ))) |
6 | | hvsubval 30264 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โโ
๐ต) = (๐ด +โ (-1
ยทโ ๐ต))) |
7 | 6 | 3adant3 1132 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด โโ
๐ต) = (๐ด +โ (-1
ยทโ ๐ต))) |
8 | 7 | oveq1d 7423 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โโ
๐ต)
โโ ๐ถ) = ((๐ด +โ (-1
ยทโ ๐ต)) โโ ๐ถ)) |
9 | | simp1 1136 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ด โ
โ) |
10 | | hvaddcl 30260 |
. . . . 5
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต +โ ๐ถ) โ
โ) |
11 | 10 | 3adant1 1130 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ต +โ ๐ถ) โ
โ) |
12 | | hvsubval 30264 |
. . . 4
โข ((๐ด โ โ โง (๐ต +โ ๐ถ) โ โ) โ (๐ด โโ
(๐ต +โ
๐ถ)) = (๐ด +โ (-1
ยทโ (๐ต +โ ๐ถ)))) |
13 | 9, 11, 12 | syl2anc 584 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด โโ
(๐ต +โ
๐ถ)) = (๐ด +โ (-1
ยทโ (๐ต +โ ๐ถ)))) |
14 | | hvsubval 30264 |
. . . . . . 7
โข (((-1
ยทโ ๐ต) โ โ โง ๐ถ โ โ) โ ((-1
ยทโ ๐ต) โโ ๐ถ) = ((-1
ยทโ ๐ต) +โ (-1
ยทโ ๐ถ))) |
15 | 3, 14 | sylan 580 |
. . . . . 6
โข ((๐ต โ โ โง ๐ถ โ โ) โ ((-1
ยทโ ๐ต) โโ ๐ถ) = ((-1
ยทโ ๐ต) +โ (-1
ยทโ ๐ถ))) |
16 | 15 | 3adant1 1130 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((-1
ยทโ ๐ต) โโ ๐ถ) = ((-1
ยทโ ๐ต) +โ (-1
ยทโ ๐ถ))) |
17 | | ax-hvdistr1 30256 |
. . . . . . 7
โข ((-1
โ โ โง ๐ต
โ โ โง ๐ถ
โ โ) โ (-1 ยทโ (๐ต +โ ๐ถ)) = ((-1
ยทโ ๐ต) +โ (-1
ยทโ ๐ถ))) |
18 | 1, 17 | mp3an1 1448 |
. . . . . 6
โข ((๐ต โ โ โง ๐ถ โ โ) โ (-1
ยทโ (๐ต +โ ๐ถ)) = ((-1 ยทโ
๐ต) +โ (-1
ยทโ ๐ถ))) |
19 | 18 | 3adant1 1130 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (-1
ยทโ (๐ต +โ ๐ถ)) = ((-1 ยทโ
๐ต) +โ (-1
ยทโ ๐ถ))) |
20 | 16, 19 | eqtr4d 2775 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((-1
ยทโ ๐ต) โโ ๐ถ) = (-1
ยทโ (๐ต +โ ๐ถ))) |
21 | 20 | oveq2d 7424 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด +โ ((-1
ยทโ ๐ต) โโ ๐ถ)) = (๐ด +โ (-1
ยทโ (๐ต +โ ๐ถ)))) |
22 | 13, 21 | eqtr4d 2775 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด โโ
(๐ต +โ
๐ถ)) = (๐ด +โ ((-1
ยทโ ๐ต) โโ ๐ถ))) |
23 | 5, 8, 22 | 3eqtr4d 2782 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โโ
๐ต)
โโ ๐ถ) = (๐ด โโ (๐ต +โ ๐ถ))) |