Step | Hyp | Ref
| Expression |
1 | | hvass.1 |
. . . . 5
โข ๐ด โ โ |
2 | | neg1cn 12275 |
. . . . . 6
โข -1 โ
โ |
3 | | hvass.2 |
. . . . . 6
โข ๐ต โ โ |
4 | 2, 3 | hvmulcli 30005 |
. . . . 5
โข (-1
ยทโ ๐ต) โ โ |
5 | | hvass.3 |
. . . . . 6
โข ๐ถ โ โ |
6 | 2, 5 | hvmulcli 30005 |
. . . . 5
โข (-1
ยทโ ๐ถ) โ โ |
7 | | hvadd4.4 |
. . . . . . 7
โข ๐ท โ โ |
8 | 2, 7 | hvmulcli 30005 |
. . . . . 6
โข (-1
ยทโ ๐ท) โ โ |
9 | 2, 8 | hvmulcli 30005 |
. . . . 5
โข (-1
ยทโ (-1 ยทโ ๐ท)) โ
โ |
10 | 1, 4, 6, 9 | hvadd4i 30049 |
. . . 4
โข ((๐ด +โ (-1
ยทโ ๐ต)) +โ ((-1
ยทโ ๐ถ) +โ (-1
ยทโ (-1 ยทโ ๐ท)))) = ((๐ด +โ (-1
ยทโ ๐ถ)) +โ ((-1
ยทโ ๐ต) +โ (-1
ยทโ (-1 ยทโ ๐ท)))) |
11 | 2, 5, 8 | hvdistr1i 30042 |
. . . . 5
โข (-1
ยทโ (๐ถ +โ (-1
ยทโ ๐ท))) = ((-1
ยทโ ๐ถ) +โ (-1
ยทโ (-1 ยทโ ๐ท))) |
12 | 11 | oveq2i 7372 |
. . . 4
โข ((๐ด +โ (-1
ยทโ ๐ต)) +โ (-1
ยทโ (๐ถ +โ (-1
ยทโ ๐ท)))) = ((๐ด +โ (-1
ยทโ ๐ต)) +โ ((-1
ยทโ ๐ถ) +โ (-1
ยทโ (-1 ยทโ ๐ท)))) |
13 | 2, 3, 8 | hvdistr1i 30042 |
. . . . 5
โข (-1
ยทโ (๐ต +โ (-1
ยทโ ๐ท))) = ((-1
ยทโ ๐ต) +โ (-1
ยทโ (-1 ยทโ ๐ท))) |
14 | 13 | oveq2i 7372 |
. . . 4
โข ((๐ด +โ (-1
ยทโ ๐ถ)) +โ (-1
ยทโ (๐ต +โ (-1
ยทโ ๐ท)))) = ((๐ด +โ (-1
ยทโ ๐ถ)) +โ ((-1
ยทโ ๐ต) +โ (-1
ยทโ (-1 ยทโ ๐ท)))) |
15 | 10, 12, 14 | 3eqtr4i 2771 |
. . 3
โข ((๐ด +โ (-1
ยทโ ๐ต)) +โ (-1
ยทโ (๐ถ +โ (-1
ยทโ ๐ท)))) = ((๐ด +โ (-1
ยทโ ๐ถ)) +โ (-1
ยทโ (๐ต +โ (-1
ยทโ ๐ท)))) |
16 | 1, 4 | hvaddcli 30009 |
. . . 4
โข (๐ด +โ (-1
ยทโ ๐ต)) โ โ |
17 | 5, 8 | hvaddcli 30009 |
. . . 4
โข (๐ถ +โ (-1
ยทโ ๐ท)) โ โ |
18 | 16, 17 | hvsubvali 30011 |
. . 3
โข ((๐ด +โ (-1
ยทโ ๐ต)) โโ (๐ถ +โ (-1
ยทโ ๐ท))) = ((๐ด +โ (-1
ยทโ ๐ต)) +โ (-1
ยทโ (๐ถ +โ (-1
ยทโ ๐ท)))) |
19 | 1, 6 | hvaddcli 30009 |
. . . 4
โข (๐ด +โ (-1
ยทโ ๐ถ)) โ โ |
20 | 3, 8 | hvaddcli 30009 |
. . . 4
โข (๐ต +โ (-1
ยทโ ๐ท)) โ โ |
21 | 19, 20 | hvsubvali 30011 |
. . 3
โข ((๐ด +โ (-1
ยทโ ๐ถ)) โโ (๐ต +โ (-1
ยทโ ๐ท))) = ((๐ด +โ (-1
ยทโ ๐ถ)) +โ (-1
ยทโ (๐ต +โ (-1
ยทโ ๐ท)))) |
22 | 15, 18, 21 | 3eqtr4i 2771 |
. 2
โข ((๐ด +โ (-1
ยทโ ๐ต)) โโ (๐ถ +โ (-1
ยทโ ๐ท))) = ((๐ด +โ (-1
ยทโ ๐ถ)) โโ (๐ต +โ (-1
ยทโ ๐ท))) |
23 | 1, 3 | hvsubvali 30011 |
. . 3
โข (๐ด โโ
๐ต) = (๐ด +โ (-1
ยทโ ๐ต)) |
24 | 5, 7 | hvsubvali 30011 |
. . 3
โข (๐ถ โโ
๐ท) = (๐ถ +โ (-1
ยทโ ๐ท)) |
25 | 23, 24 | oveq12i 7373 |
. 2
โข ((๐ด โโ
๐ต)
โโ (๐ถ โโ ๐ท)) = ((๐ด +โ (-1
ยทโ ๐ต)) โโ (๐ถ +โ (-1
ยทโ ๐ท))) |
26 | 1, 5 | hvsubvali 30011 |
. . 3
โข (๐ด โโ
๐ถ) = (๐ด +โ (-1
ยทโ ๐ถ)) |
27 | 3, 7 | hvsubvali 30011 |
. . 3
โข (๐ต โโ
๐ท) = (๐ต +โ (-1
ยทโ ๐ท)) |
28 | 26, 27 | oveq12i 7373 |
. 2
โข ((๐ด โโ
๐ถ)
โโ (๐ต โโ ๐ท)) = ((๐ด +โ (-1
ยทโ ๐ถ)) โโ (๐ต +โ (-1
ยทโ ๐ท))) |
29 | 22, 25, 28 | 3eqtr4i 2771 |
1
โข ((๐ด โโ
๐ต)
โโ (๐ถ โโ ๐ท)) = ((๐ด โโ ๐ถ) โโ
(๐ต
โโ ๐ท)) |