Metamath Proof Explorer


Definition df-abv

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 AbsVal=rRingf0+∞Baser|xBaserfx=0x=0ryBaserfxry=fxfyfx+ryfx+fy

Detailed syntax breakdown

Step Hyp Ref Expression
0 cabv classAbsVal
1 vr setvarr
2 crg classRing
3 vf setvarf
4 cc0 class0
5 cico class.
6 cpnf class+∞
7 4 6 5 co class0+∞
8 cmap class𝑚
9 cbs classBase
10 1 cv setvarr
11 10 9 cfv classBaser
12 7 11 8 co class0+∞Baser
13 vx setvarx
14 3 cv setvarf
15 13 cv setvarx
16 15 14 cfv classfx
17 16 4 wceq wfffx=0
18 c0g class0𝑔
19 10 18 cfv class0r
20 15 19 wceq wffx=0r
21 17 20 wb wfffx=0x=0r
22 vy setvary
23 cmulr class𝑟
24 10 23 cfv classr
25 22 cv setvary
26 15 25 24 co classxry
27 26 14 cfv classfxry
28 cmul class×
29 25 14 cfv classfy
30 16 29 28 co classfxfy
31 27 30 wceq wfffxry=fxfy
32 cplusg class+𝑔
33 10 32 cfv class+r
34 15 25 33 co classx+ry
35 34 14 cfv classfx+ry
36 cle class
37 caddc class+
38 16 29 37 co classfx+fy
39 35 38 36 wbr wfffx+ryfx+fy
40 31 39 wa wfffxry=fxfyfx+ryfx+fy
41 40 22 11 wral wffyBaserfxry=fxfyfx+ryfx+fy
42 21 41 wa wfffx=0x=0ryBaserfxry=fxfyfx+ryfx+fy
43 42 13 11 wral wffxBaserfx=0x=0ryBaserfxry=fxfyfx+ryfx+fy
44 43 3 12 crab classf0+∞Baser|xBaserfx=0x=0ryBaserfxry=fxfyfx+ryfx+fy
45 1 2 44 cmpt classrRingf0+∞Baser|xBaserfx=0x=0ryBaserfxry=fxfyfx+ryfx+fy
46 0 45 wceq wffAbsVal=rRingf0+∞Baser|xBaserfx=0x=0ryBaserfxry=fxfyfx+ryfx+fy