# 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 ${⊢}\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}}\phantom{\rule{.4em}{0ex}}\left(\left({f}\left({x}\right)=0↔{x}={0}_{{r}}\right)\wedge \forall {y}\in {\mathrm{Base}}_{{r}}\phantom{\rule{.4em}{0ex}}\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 ${setvar}{r}$
2 crg ${class}\mathrm{Ring}$
3 vf ${setvar}{f}$
4 cc0 ${class}0$
5 cico ${class}\left[.\right)$
6 cpnf ${class}\mathrm{+\infty }$
7 4 6 5 co ${class}\left[0,\mathrm{+\infty }\right)$
8 cmap ${class}{↑}_{𝑚}$
9 cbs ${class}\mathrm{Base}$
10 1 cv ${setvar}{r}$
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 ${setvar}{x}$
14 3 cv ${setvar}{f}$
15 13 cv ${setvar}{x}$
16 15 14 cfv ${class}{f}\left({x}\right)$
17 16 4 wceq ${wff}{f}\left({x}\right)=0$
18 c0g ${class}{0}_{𝑔}$
19 10 18 cfv ${class}{0}_{{r}}$
20 15 19 wceq ${wff}{x}={0}_{{r}}$
21 17 20 wb ${wff}\left({f}\left({x}\right)=0↔{x}={0}_{{r}}\right)$
22 vy ${setvar}{y}$
23 cmulr ${class}{\cdot }_{𝑟}$
24 10 23 cfv ${class}{\cdot }_{{r}}$
25 22 cv ${setvar}{y}$
26 15 25 24 co ${class}\left({x}{\cdot }_{{r}}{y}\right)$
27 26 14 cfv ${class}{f}\left({x}{\cdot }_{{r}}{y}\right)$
28 cmul ${class}×$
29 25 14 cfv ${class}{f}\left({y}\right)$
30 16 29 28 co ${class}{f}\left({x}\right){f}\left({y}\right)$
31 27 30 wceq ${wff}{f}\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 ${class}{f}\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 ${wff}{f}\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}}\phantom{\rule{.4em}{0ex}}\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↔{x}={0}_{{r}}\right)\wedge \forall {y}\in {\mathrm{Base}}_{{r}}\phantom{\rule{.4em}{0ex}}\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}}\phantom{\rule{.4em}{0ex}}\left(\left({f}\left({x}\right)=0↔{x}={0}_{{r}}\right)\wedge \forall {y}\in {\mathrm{Base}}_{{r}}\phantom{\rule{.4em}{0ex}}\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}}\phantom{\rule{.4em}{0ex}}\left(\left({f}\left({x}\right)=0↔{x}={0}_{{r}}\right)\wedge \forall {y}\in {\mathrm{Base}}_{{r}}\phantom{\rule{.4em}{0ex}}\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}}\phantom{\rule{.4em}{0ex}}\left(\left({f}\left({x}\right)=0↔{x}={0}_{{r}}\right)\wedge \forall {y}\in {\mathrm{Base}}_{{r}}\phantom{\rule{.4em}{0ex}}\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}}\phantom{\rule{.4em}{0ex}}\left(\left({f}\left({x}\right)=0↔{x}={0}_{{r}}\right)\wedge \forall {y}\in {\mathrm{Base}}_{{r}}\phantom{\rule{.4em}{0ex}}\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)$