# Metamath Proof Explorer

## Theorem abvrcl

Description: Reverse closure for the absolute value set. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Hypothesis abvf.a ${⊢}{A}=\mathrm{AbsVal}\left({R}\right)$
Assertion abvrcl ${⊢}{F}\in {A}\to {R}\in \mathrm{Ring}$

### Proof

Step Hyp Ref Expression
1 abvf.a ${⊢}{A}=\mathrm{AbsVal}\left({R}\right)$
2 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)$
3 2 mptrcl ${⊢}{F}\in \mathrm{AbsVal}\left({R}\right)\to {R}\in \mathrm{Ring}$
4 3 1 eleq2s ${⊢}{F}\in {A}\to {R}\in \mathrm{Ring}$