Description: Define the set of absolute values on a ring. An absolute value is a generalization of the usual absolute value function df-abs to arbitrary rings. (Contributed by Mario Carneiro, 8-Sep-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | df-abv | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cabv | |
|
1 | vr | |
|
2 | crg | |
|
3 | vf | |
|
4 | cc0 | |
|
5 | cico | |
|
6 | cpnf | |
|
7 | 4 6 5 | co | |
8 | cmap | |
|
9 | cbs | |
|
10 | 1 | cv | |
11 | 10 9 | cfv | |
12 | 7 11 8 | co | |
13 | vx | |
|
14 | 3 | cv | |
15 | 13 | cv | |
16 | 15 14 | cfv | |
17 | 16 4 | wceq | |
18 | c0g | |
|
19 | 10 18 | cfv | |
20 | 15 19 | wceq | |
21 | 17 20 | wb | |
22 | vy | |
|
23 | cmulr | |
|
24 | 10 23 | cfv | |
25 | 22 | cv | |
26 | 15 25 24 | co | |
27 | 26 14 | cfv | |
28 | cmul | |
|
29 | 25 14 | cfv | |
30 | 16 29 28 | co | |
31 | 27 30 | wceq | |
32 | cplusg | |
|
33 | 10 32 | cfv | |
34 | 15 25 33 | co | |
35 | 34 14 | cfv | |
36 | cle | |
|
37 | caddc | |
|
38 | 16 29 37 | co | |
39 | 35 38 36 | wbr | |
40 | 31 39 | wa | |
41 | 40 22 11 | wral | |
42 | 21 41 | wa | |
43 | 42 13 11 | wral | |
44 | 43 3 12 | crab | |
45 | 1 2 44 | cmpt | |
46 | 0 45 | wceq | |