Step | Hyp | Ref
| Expression |
1 | | hodseq.2 |
. . . . . 6
โข ๐: โโถ
โ |
2 | | neg1cn 12272 |
. . . . . . 7
โข -1 โ
โ |
3 | | hodseq.3 |
. . . . . . 7
โข ๐: โโถ
โ |
4 | | homulcl 30743 |
. . . . . . 7
โข ((-1
โ โ โง ๐:
โโถ โ) โ (-1 ยทop ๐): โโถ
โ) |
5 | 2, 3, 4 | mp2an 691 |
. . . . . 6
โข (-1
ยทop ๐): โโถ โ |
6 | | hosval 30724 |
. . . . . 6
โข ((๐: โโถ โ โง
(-1 ยทop ๐): โโถ โ โง ๐ฅ โ โ) โ ((๐ +op (-1
ยทop ๐))โ๐ฅ) = ((๐โ๐ฅ) +โ ((-1
ยทop ๐)โ๐ฅ))) |
7 | 1, 5, 6 | mp3an12 1452 |
. . . . 5
โข (๐ฅ โ โ โ ((๐ +op (-1
ยทop ๐))โ๐ฅ) = ((๐โ๐ฅ) +โ ((-1
ยทop ๐)โ๐ฅ))) |
8 | 1 | ffvelcdmi 7035 |
. . . . . . 7
โข (๐ฅ โ โ โ (๐โ๐ฅ) โ โ) |
9 | 3 | ffvelcdmi 7035 |
. . . . . . 7
โข (๐ฅ โ โ โ (๐โ๐ฅ) โ โ) |
10 | | hvsubval 30000 |
. . . . . . 7
โข (((๐โ๐ฅ) โ โ โง (๐โ๐ฅ) โ โ) โ ((๐โ๐ฅ) โโ (๐โ๐ฅ)) = ((๐โ๐ฅ) +โ (-1
ยทโ (๐โ๐ฅ)))) |
11 | 8, 9, 10 | syl2anc 585 |
. . . . . 6
โข (๐ฅ โ โ โ ((๐โ๐ฅ) โโ (๐โ๐ฅ)) = ((๐โ๐ฅ) +โ (-1
ยทโ (๐โ๐ฅ)))) |
12 | | homval 30725 |
. . . . . . . 8
โข ((-1
โ โ โง ๐:
โโถ โ โง ๐ฅ โ โ) โ ((-1
ยทop ๐)โ๐ฅ) = (-1 ยทโ
(๐โ๐ฅ))) |
13 | 2, 3, 12 | mp3an12 1452 |
. . . . . . 7
โข (๐ฅ โ โ โ ((-1
ยทop ๐)โ๐ฅ) = (-1 ยทโ
(๐โ๐ฅ))) |
14 | 13 | oveq2d 7374 |
. . . . . 6
โข (๐ฅ โ โ โ ((๐โ๐ฅ) +โ ((-1
ยทop ๐)โ๐ฅ)) = ((๐โ๐ฅ) +โ (-1
ยทโ (๐โ๐ฅ)))) |
15 | 11, 14 | eqtr4d 2776 |
. . . . 5
โข (๐ฅ โ โ โ ((๐โ๐ฅ) โโ (๐โ๐ฅ)) = ((๐โ๐ฅ) +โ ((-1
ยทop ๐)โ๐ฅ))) |
16 | 7, 15 | eqtr4d 2776 |
. . . 4
โข (๐ฅ โ โ โ ((๐ +op (-1
ยทop ๐))โ๐ฅ) = ((๐โ๐ฅ) โโ (๐โ๐ฅ))) |
17 | | hodval 30726 |
. . . . 5
โข ((๐: โโถ โ โง
๐: โโถ โ
โง ๐ฅ โ โ)
โ ((๐
โop ๐)โ๐ฅ) = ((๐โ๐ฅ) โโ (๐โ๐ฅ))) |
18 | 1, 3, 17 | mp3an12 1452 |
. . . 4
โข (๐ฅ โ โ โ ((๐ โop ๐)โ๐ฅ) = ((๐โ๐ฅ) โโ (๐โ๐ฅ))) |
19 | 16, 18 | eqtr4d 2776 |
. . 3
โข (๐ฅ โ โ โ ((๐ +op (-1
ยทop ๐))โ๐ฅ) = ((๐ โop ๐)โ๐ฅ)) |
20 | 19 | rgen 3063 |
. 2
โข
โ๐ฅ โ
โ ((๐ +op
(-1 ยทop ๐))โ๐ฅ) = ((๐ โop ๐)โ๐ฅ) |
21 | 1, 5 | hoaddcli 30752 |
. . 3
โข (๐ +op (-1
ยทop ๐)): โโถ โ |
22 | 1, 3 | hosubcli 30753 |
. . 3
โข (๐ โop ๐): โโถ
โ |
23 | 21, 22 | hoeqi 30745 |
. 2
โข
(โ๐ฅ โ
โ ((๐ +op
(-1 ยทop ๐))โ๐ฅ) = ((๐ โop ๐)โ๐ฅ) โ (๐ +op (-1
ยทop ๐)) = (๐ โop ๐)) |
24 | 20, 23 | mpbi 229 |
1
โข (๐ +op (-1
ยทop ๐)) = (๐ โop ๐) |