Step | Hyp | Ref
| Expression |
1 | | hvsubval 30536 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โโ
๐ต) = (๐ด +โ (-1
ยทโ ๐ต))) |
2 | 1 | oveq1d 7426 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด โโ
๐ต)
ยทih ๐ถ) = ((๐ด +โ (-1
ยทโ ๐ต)) ยทih ๐ถ)) |
3 | 2 | 3adant3 1130 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โโ
๐ต)
ยทih ๐ถ) = ((๐ด +โ (-1
ยทโ ๐ต)) ยทih ๐ถ)) |
4 | | neg1cn 12330 |
. . . . 5
โข -1 โ
โ |
5 | | hvmulcl 30533 |
. . . . 5
โข ((-1
โ โ โง ๐ต
โ โ) โ (-1 ยทโ ๐ต) โ โ) |
6 | 4, 5 | mpan 686 |
. . . 4
โข (๐ต โ โ โ (-1
ยทโ ๐ต) โ โ) |
7 | | ax-his2 30603 |
. . . 4
โข ((๐ด โ โ โง (-1
ยทโ ๐ต) โ โ โง ๐ถ โ โ) โ ((๐ด +โ (-1
ยทโ ๐ต)) ยทih ๐ถ) = ((๐ด ยทih ๐ถ) + ((-1
ยทโ ๐ต) ยทih ๐ถ))) |
8 | 6, 7 | syl3an2 1162 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด +โ (-1
ยทโ ๐ต)) ยทih ๐ถ) = ((๐ด ยทih ๐ถ) + ((-1
ยทโ ๐ต) ยทih ๐ถ))) |
9 | | ax-his3 30604 |
. . . . . . 7
โข ((-1
โ โ โง ๐ต
โ โ โง ๐ถ
โ โ) โ ((-1 ยทโ ๐ต)
ยทih ๐ถ) = (-1 ยท (๐ต ยทih ๐ถ))) |
10 | 4, 9 | mp3an1 1446 |
. . . . . 6
โข ((๐ต โ โ โง ๐ถ โ โ) โ ((-1
ยทโ ๐ต) ยทih ๐ถ) = (-1 ยท (๐ต
ยทih ๐ถ))) |
11 | | hicl 30600 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต
ยทih ๐ถ) โ โ) |
12 | 11 | mulm1d 11670 |
. . . . . 6
โข ((๐ต โ โ โง ๐ถ โ โ) โ (-1
ยท (๐ต
ยทih ๐ถ)) = -(๐ต ยทih ๐ถ)) |
13 | 10, 12 | eqtrd 2770 |
. . . . 5
โข ((๐ต โ โ โง ๐ถ โ โ) โ ((-1
ยทโ ๐ต) ยทih ๐ถ) = -(๐ต ยทih ๐ถ)) |
14 | 13 | oveq2d 7427 |
. . . 4
โข ((๐ต โ โ โง ๐ถ โ โ) โ ((๐ด
ยทih ๐ถ) + ((-1 ยทโ
๐ต)
ยทih ๐ถ)) = ((๐ด ยทih ๐ถ) + -(๐ต ยทih ๐ถ))) |
15 | 14 | 3adant1 1128 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด
ยทih ๐ถ) + ((-1 ยทโ
๐ต)
ยทih ๐ถ)) = ((๐ด ยทih ๐ถ) + -(๐ต ยทih ๐ถ))) |
16 | 8, 15 | eqtrd 2770 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด +โ (-1
ยทโ ๐ต)) ยทih ๐ถ) = ((๐ด ยทih ๐ถ) + -(๐ต ยทih ๐ถ))) |
17 | | hicl 30600 |
. . . 4
โข ((๐ด โ โ โง ๐ถ โ โ) โ (๐ด
ยทih ๐ถ) โ โ) |
18 | 17 | 3adant2 1129 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด
ยทih ๐ถ) โ โ) |
19 | 11 | 3adant1 1128 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ต
ยทih ๐ถ) โ โ) |
20 | 18, 19 | negsubd 11581 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด
ยทih ๐ถ) + -(๐ต ยทih ๐ถ)) = ((๐ด ยทih ๐ถ) โ (๐ต ยทih ๐ถ))) |
21 | 3, 16, 20 | 3eqtrd 2774 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โโ
๐ต)
ยทih ๐ถ) = ((๐ด ยทih ๐ถ) โ (๐ต ยทih ๐ถ))) |