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\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)$$
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}$$