Step | Hyp | Ref
| Expression |
1 | | cabv 20291 |
. 2
class
AbsVal |
2 | | vr |
. . 3
setvar ๐ |
3 | | crg 19971 |
. . 3
class
Ring |
4 | | vx |
. . . . . . . . . 10
setvar ๐ฅ |
5 | 4 | cv 1541 |
. . . . . . . . 9
class ๐ฅ |
6 | | vf |
. . . . . . . . . 10
setvar ๐ |
7 | 6 | cv 1541 |
. . . . . . . . 9
class ๐ |
8 | 5, 7 | cfv 6501 |
. . . . . . . 8
class (๐โ๐ฅ) |
9 | | cc0 11058 |
. . . . . . . 8
class
0 |
10 | 8, 9 | wceq 1542 |
. . . . . . 7
wff (๐โ๐ฅ) = 0 |
11 | 2 | cv 1541 |
. . . . . . . . 9
class ๐ |
12 | | c0g 17328 |
. . . . . . . . 9
class
0g |
13 | 11, 12 | cfv 6501 |
. . . . . . . 8
class
(0gโ๐) |
14 | 5, 13 | wceq 1542 |
. . . . . . 7
wff ๐ฅ = (0gโ๐) |
15 | 10, 14 | wb 205 |
. . . . . 6
wff ((๐โ๐ฅ) = 0 โ ๐ฅ = (0gโ๐)) |
16 | | vy |
. . . . . . . . . . . 12
setvar ๐ฆ |
17 | 16 | cv 1541 |
. . . . . . . . . . 11
class ๐ฆ |
18 | | cmulr 17141 |
. . . . . . . . . . . 12
class
.r |
19 | 11, 18 | cfv 6501 |
. . . . . . . . . . 11
class
(.rโ๐) |
20 | 5, 17, 19 | co 7362 |
. . . . . . . . . 10
class (๐ฅ(.rโ๐)๐ฆ) |
21 | 20, 7 | cfv 6501 |
. . . . . . . . 9
class (๐โ(๐ฅ(.rโ๐)๐ฆ)) |
22 | 17, 7 | cfv 6501 |
. . . . . . . . . 10
class (๐โ๐ฆ) |
23 | | cmul 11063 |
. . . . . . . . . 10
class
ยท |
24 | 8, 22, 23 | co 7362 |
. . . . . . . . 9
class ((๐โ๐ฅ) ยท (๐โ๐ฆ)) |
25 | 21, 24 | wceq 1542 |
. . . . . . . 8
wff (๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ) ยท (๐โ๐ฆ)) |
26 | | cplusg 17140 |
. . . . . . . . . . . 12
class
+g |
27 | 11, 26 | cfv 6501 |
. . . . . . . . . . 11
class
(+gโ๐) |
28 | 5, 17, 27 | co 7362 |
. . . . . . . . . 10
class (๐ฅ(+gโ๐)๐ฆ) |
29 | 28, 7 | cfv 6501 |
. . . . . . . . 9
class (๐โ(๐ฅ(+gโ๐)๐ฆ)) |
30 | | caddc 11061 |
. . . . . . . . . 10
class
+ |
31 | 8, 22, 30 | co 7362 |
. . . . . . . . 9
class ((๐โ๐ฅ) + (๐โ๐ฆ)) |
32 | | cle 11197 |
. . . . . . . . 9
class
โค |
33 | 29, 31, 32 | wbr 5110 |
. . . . . . . 8
wff (๐โ(๐ฅ(+gโ๐)๐ฆ)) โค ((๐โ๐ฅ) + (๐โ๐ฆ)) |
34 | 25, 33 | wa 397 |
. . . . . . 7
wff ((๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ) ยท (๐โ๐ฆ)) โง (๐โ(๐ฅ(+gโ๐)๐ฆ)) โค ((๐โ๐ฅ) + (๐โ๐ฆ))) |
35 | | cbs 17090 |
. . . . . . . 8
class
Base |
36 | 11, 35 | cfv 6501 |
. . . . . . 7
class
(Baseโ๐) |
37 | 34, 16, 36 | wral 3065 |
. . . . . 6
wff
โ๐ฆ โ
(Baseโ๐)((๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ) ยท (๐โ๐ฆ)) โง (๐โ(๐ฅ(+gโ๐)๐ฆ)) โค ((๐โ๐ฅ) + (๐โ๐ฆ))) |
38 | 15, 37 | wa 397 |
. . . . 5
wff (((๐โ๐ฅ) = 0 โ ๐ฅ = (0gโ๐)) โง โ๐ฆ โ (Baseโ๐)((๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ) ยท (๐โ๐ฆ)) โง (๐โ(๐ฅ(+gโ๐)๐ฆ)) โค ((๐โ๐ฅ) + (๐โ๐ฆ)))) |
39 | 38, 4, 36 | wral 3065 |
. . . 4
wff
โ๐ฅ โ
(Baseโ๐)(((๐โ๐ฅ) = 0 โ ๐ฅ = (0gโ๐)) โง โ๐ฆ โ (Baseโ๐)((๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ) ยท (๐โ๐ฆ)) โง (๐โ(๐ฅ(+gโ๐)๐ฆ)) โค ((๐โ๐ฅ) + (๐โ๐ฆ)))) |
40 | | cpnf 11193 |
. . . . . 6
class
+โ |
41 | | cico 13273 |
. . . . . 6
class
[,) |
42 | 9, 40, 41 | co 7362 |
. . . . 5
class
(0[,)+โ) |
43 | | cmap 8772 |
. . . . 5
class
โm |
44 | 42, 36, 43 | co 7362 |
. . . 4
class
((0[,)+โ) โm (Baseโ๐)) |
45 | 39, 6, 44 | crab 3410 |
. . 3
class {๐ โ ((0[,)+โ)
โm (Baseโ๐)) โฃ โ๐ฅ โ (Baseโ๐)(((๐โ๐ฅ) = 0 โ ๐ฅ = (0gโ๐)) โง โ๐ฆ โ (Baseโ๐)((๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ) ยท (๐โ๐ฆ)) โง (๐โ(๐ฅ(+gโ๐)๐ฆ)) โค ((๐โ๐ฅ) + (๐โ๐ฆ))))} |
46 | 2, 3, 45 | cmpt 5193 |
. 2
class (๐ โ Ring โฆ {๐ โ ((0[,)+โ)
โm (Baseโ๐)) โฃ โ๐ฅ โ (Baseโ๐)(((๐โ๐ฅ) = 0 โ ๐ฅ = (0gโ๐)) โง โ๐ฆ โ (Baseโ๐)((๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ) ยท (๐โ๐ฆ)) โง (๐โ(๐ฅ(+gโ๐)๐ฆ)) โค ((๐โ๐ฅ) + (๐โ๐ฆ))))}) |
47 | 1, 46 | wceq 1542 |
1
wff AbsVal =
(๐ โ Ring โฆ
{๐ โ ((0[,)+โ)
โm (Baseโ๐)) โฃ โ๐ฅ โ (Baseโ๐)(((๐โ๐ฅ) = 0 โ ๐ฅ = (0gโ๐)) โง โ๐ฆ โ (Baseโ๐)((๐โ(๐ฅ(.rโ๐)๐ฆ)) = ((๐โ๐ฅ) ยท (๐โ๐ฆ)) โง (๐โ(๐ฅ(+gโ๐)๐ฆ)) โค ((๐โ๐ฅ) + (๐โ๐ฆ))))}) |