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	$$⊢\mathrm{AbsVal}=\left(r\in \mathrm{Ring}⟼\left\{f\in \left({\left[0,\mathrm{+\infty }\right)}^{{\mathrm{Base}}_r}\right)|\forall x\in {\mathrm{Base}}_r\left(\left(f\left(x\right)=0\leftrightarrow x=0_r\right)\wedge \forall y\in {\mathrm{Base}}_r\left(f\left(x{\cdot }_{r}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{r}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cabv	$$class\mathrm{AbsVal}$$
1		vr	$$setvarr$$
2		crg	$$class\mathrm{Ring}$$
3		vf	$$setvarf$$
4		cc0	$$class0$$
5		cico	$$class\left[.\right)$$
6		cpnf	$$class\mathrm{+\infty }$$
7	4 6 5	co	$$class\left[0,\mathrm{+\infty }\right)$$
8		cmap	$$class{\uparrow }_{𝑚}$$
9		cbs	$$class\mathrm{Base}$$
10	1	cv	$$setvarr$$
11	10 9	cfv	$$class{\mathrm{Base}}_r$$
12	7 11 8	co	$$class\left({\left[0,\mathrm{+\infty }\right)}^{{\mathrm{Base}}_r}\right)$$
13		vx	$$setvarx$$
14	3	cv	$$setvarf$$
15	13	cv	$$setvarx$$
16	15 14	cfv	$$classf\left(x\right)$$
17	16 4	wceq	$$wfff\left(x\right)=0$$
18		c0g	$$class{0}_{𝑔}$$
19	10 18	cfv	$$class{0}_r$$
20	15 19	wceq	$$wffx=0_r$$
21	17 20	wb	$$wff\left(f\left(x\right)=0\leftrightarrow x=0_r\right)$$
22		vy	$$setvary$$
23		cmulr	$$class{\cdot }_{𝑟}$$
24	10 23	cfv	$$class{\cdot }_r$$
25	22	cv	$$setvary$$
26	15 25 24	co	$$class\left(x{\cdot }_{r}y\right)$$
27	26 14	cfv	$$classf\left(x{\cdot }_{r}y\right)$$
28		cmul	$$class\times$$
29	25 14	cfv	$$classf\left(y\right)$$
30	16 29 28	co	$$classf\left(x\right)f\left(y\right)$$
31	27 30	wceq	$$wfff\left(x{\cdot }_{r}y\right)=f\left(x\right)f\left(y\right)$$
32		cplusg	$$class{+}_{𝑔}$$
33	10 32	cfv	$$class{+}_r$$
34	15 25 33	co	$$class\left(x{+}_{r}y\right)$$
35	34 14	cfv	$$classf\left(x{+}_{r}y\right)$$
36		cle	$$class\le$$
37		caddc	$$class+$$
38	16 29 37	co	$$class\left(f\left(x\right)+f\left(y\right)\right)$$
39	35 38 36	wbr	$$wfff\left(x{+}_{r}y\right)\le f\left(x\right)+f\left(y\right)$$
40	31 39	wa	$$wff\left(f\left(x{\cdot }_{r}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{r}y\right)\le f\left(x\right)+f\left(y\right)\right)$$
41	40 22 11	wral	$$wff\forall y\in {\mathrm{Base}}_r\left(f\left(x{\cdot }_{r}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{r}y\right)\le f\left(x\right)+f\left(y\right)\right)$$
42	21 41	wa	$$wff\left(\left(f\left(x\right)=0\leftrightarrow x=0_r\right)\wedge \forall y\in {\mathrm{Base}}_r\left(f\left(x{\cdot }_{r}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{r}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)$$
43	42 13 11	wral	$$wff\forall x\in {\mathrm{Base}}_r\left(\left(f\left(x\right)=0\leftrightarrow x=0_r\right)\wedge \forall y\in {\mathrm{Base}}_r\left(f\left(x{\cdot }_{r}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{r}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)$$
44	43 3 12	crab	$$class\left\{f\in \left({\left[0,\mathrm{+\infty }\right)}^{{\mathrm{Base}}_r}\right)|\forall x\in {\mathrm{Base}}_r\left(\left(f\left(x\right)=0\leftrightarrow x=0_r\right)\wedge \forall y\in {\mathrm{Base}}_r\left(f\left(x{\cdot }_{r}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{r}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right\}$$
45	1 2 44	cmpt	$$class\left(r\in \mathrm{Ring}⟼\left\{f\in \left({\left[0,\mathrm{+\infty }\right)}^{{\mathrm{Base}}_r}\right)|\forall x\in {\mathrm{Base}}_r\left(\left(f\left(x\right)=0\leftrightarrow x=0_r\right)\wedge \forall y\in {\mathrm{Base}}_r\left(f\left(x{\cdot }_{r}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{r}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right\}\right)$$
46	0 45	wceq	$$wff\mathrm{AbsVal}=\left(r\in \mathrm{Ring}⟼\left\{f\in \left({\left[0,\mathrm{+\infty }\right)}^{{\mathrm{Base}}_r}\right)|\forall x\in {\mathrm{Base}}_r\left(\left(f\left(x\right)=0\leftrightarrow x=0_r\right)\wedge \forall y\in {\mathrm{Base}}_r\left(f\left(x{\cdot }_{r}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x{+}_{r}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right\}\right)$$