# Metamath Proof Explorer

## Theorem abvfge0

Description: An absolute value is a function from the ring to the nonnegative real numbers. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Hypotheses abvf.a ${⊢}{A}=\mathrm{AbsVal}\left({R}\right)$
abvf.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
Assertion abvfge0 ${⊢}{F}\in {A}\to {F}:{B}⟶\left[0,\mathrm{+\infty }\right)$

### Proof

Step Hyp Ref Expression
1 abvf.a ${⊢}{A}=\mathrm{AbsVal}\left({R}\right)$
2 abvf.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
3 1 abvrcl ${⊢}{F}\in {A}\to {R}\in \mathrm{Ring}$
4 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
5 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
6 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
7 1 2 4 5 6 isabv ${⊢}{R}\in \mathrm{Ring}\to \left({F}\in {A}↔\left({F}:{B}⟶\left[0,\mathrm{+\infty }\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({x}\right)=0↔{x}={0}_{{R}}\right)\wedge \forall {y}\in {B}\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)$
8 3 7 syl ${⊢}{F}\in {A}\to \left({F}\in {A}↔\left({F}:{B}⟶\left[0,\mathrm{+\infty }\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({x}\right)=0↔{x}={0}_{{R}}\right)\wedge \forall {y}\in {B}\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)$
9 8 ibi ${⊢}{F}\in {A}\to \left({F}:{B}⟶\left[0,\mathrm{+\infty }\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({x}\right)=0↔{x}={0}_{{R}}\right)\wedge \forall {y}\in {B}\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)$
10 9 simpld ${⊢}{F}\in {A}\to {F}:{B}⟶\left[0,\mathrm{+\infty }\right)$