Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-abv Structured version   Unicode version

Definition df-abv 16826
 Description: Define the set of absolute values on a ring. An absolute value is a generalization of the usual absolute value function df-abs 12709 to arbitrary rings. (Contributed by Mario Carneiro, 8-Sep-2014.)
Assertion
Ref Expression
df-abv AbsVal
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-abv
StepHypRef Expression
1 cabv 16825 . 2 AbsVal
2 vr . . 3
3 crg 16577 . . 3
4 vx . . . . . . . . . 10
54cv 1361 . . . . . . . . 9
6 vf . . . . . . . . . 10
76cv 1361 . . . . . . . . 9
85, 7cfv 5406 . . . . . . . 8
9 cc0 9270 . . . . . . . 8
108, 9wceq 1362 . . . . . . 7
112cv 1361 . . . . . . . . 9
12 c0g 14361 . . . . . . . . 9
1311, 12cfv 5406 . . . . . . . 8
145, 13wceq 1362 . . . . . . 7
1510, 14wb 184 . . . . . 6
16 vy . . . . . . . . . . . 12
1716cv 1361 . . . . . . . . . . 11
18 cmulr 14222 . . . . . . . . . . . 12
1911, 18cfv 5406 . . . . . . . . . . 11
205, 17, 19co 6080 . . . . . . . . . 10
2120, 7cfv 5406 . . . . . . . . 9
2217, 7cfv 5406 . . . . . . . . . 10
23 cmul 9275 . . . . . . . . . 10
248, 22, 23co 6080 . . . . . . . . 9
2521, 24wceq 1362 . . . . . . . 8
26 cplusg 14221 . . . . . . . . . . . 12
2711, 26cfv 5406 . . . . . . . . . . 11
285, 17, 27co 6080 . . . . . . . . . 10
2928, 7cfv 5406 . . . . . . . . 9
30 caddc 9273 . . . . . . . . . 10
318, 22, 30co 6080 . . . . . . . . 9
32 cle 9407 . . . . . . . . 9
3329, 31, 32wbr 4280 . . . . . . . 8
3425, 33wa 369 . . . . . . 7
35 cbs 14157 . . . . . . . 8
3611, 35cfv 5406 . . . . . . 7
3734, 16, 36wral 2705 . . . . . 6
3815, 37wa 369 . . . . 5
3938, 4, 36wral 2705 . . . 4
40 cpnf 9403 . . . . . 6
41 cico 11290 . . . . . 6
429, 40, 41co 6080 . . . . 5
43 cmap 7202 . . . . 5
4442, 36, 43co 6080 . . . 4
4539, 6, 44crab 2709 . . 3
462, 3, 45cmpt 4338 . 2
471, 46wceq 1362 1 AbsVal
 Colors of variables: wff setvar class This definition is referenced by:  abvfval  16827  abvrcl  16830
 Copyright terms: Public domain W3C validator