Theorem abvfval

Description: Value of the set of absolute values. (Contributed by Mario Carneiro, 8-Sep-2014)

	Ref	Expression
Hypotheses	abvfval.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
	abvfval.b	$$⊢B={\mathrm{Base}}_R$$
	abvfval.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	abvfval.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	abvfval.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	abvfval	$$⊢R\in \mathrm{Ring}\to A=\left\{f\in \left({\left[0,\mathrm{+\infty }\right)}^B\right)|\forall x\in B\left(\left(f\left(x\right)=0\leftrightarrow x=\underset{\dot{}}{0}\right)\wedge \forall y\in B\left(f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x\underset{\dot{}}{+}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		abvfval.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
2		abvfval.b	$$⊢B={\mathrm{Base}}_R$$
3		abvfval.p	$$⊢\underset{\dot{}}{+}={+}_R$$
4		abvfval.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
5		abvfval.z	$$⊢\underset{\dot{}}{0}=0_R$$
6		fveq2	$$⊢r=R\to {\mathrm{Base}}_r={\mathrm{Base}}_R$$
7	6 2	syl6eqr	$$⊢r=R\to {\mathrm{Base}}_r=B$$
8	7	oveq2d	$$⊢r=R\to {\left[0,\mathrm{+\infty }\right)}^{{\mathrm{Base}}_r}={\left[0,\mathrm{+\infty }\right)}^B$$
9		fveq2	$$⊢r=R\to 0_r=0_R$$
10	9 5	syl6eqr	$$⊢r=R\to 0_r=\underset{\dot{}}{0}$$
11	10	eqeq2d	$$⊢r=R\to \left(x=0_r\leftrightarrow x=\underset{\dot{}}{0}\right)$$
12	11	bibi2d	$$⊢r=R\to \left(\left(f\left(x\right)=0\leftrightarrow x=0_r\right)\leftrightarrow \left(f\left(x\right)=0\leftrightarrow x=\underset{\dot{}}{0}\right)\right)$$
13		fveq2	$$⊢r=R\to {\cdot }_r={\cdot }_R$$
14	13 4	syl6eqr	$$⊢r=R\to {\cdot }_r=\underset{\dot{}}{·}$$
15	14	oveqd	$$⊢r=R\to x{\cdot }_{r}y=x\underset{\dot{}}{·}y$$
16	15	fveqeq2d	$$⊢r=R\to \left(f\left(x{\cdot }_{r}y\right)=f\left(x\right)f\left(y\right)\leftrightarrow f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)f\left(y\right)\right)$$
17		fveq2	$$⊢r=R\to {+}_r={+}_R$$
18	17 3	syl6eqr	$$⊢r=R\to {+}_r=\underset{\dot{}}{+}$$
19	18	oveqd	$$⊢r=R\to x{+}_{r}y=x\underset{\dot{}}{+}y$$
20	19	fveq2d	$$⊢r=R\to f\left(x{+}_{r}y\right)=f\left(x\underset{\dot{}}{+}y\right)$$
21	20	breq1d	$$⊢r=R\to \left(f\left(x{+}_{r}y\right)\le f\left(x\right)+f\left(y\right)\leftrightarrow f\left(x\underset{\dot{}}{+}y\right)\le f\left(x\right)+f\left(y\right)\right)$$
22	16 21	anbi12d	$$⊢r=R\to \left(\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)\leftrightarrow \left(f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x\underset{\dot{}}{+}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)$$
23	7 22	raleqbidv	$$⊢r=R\to \left(\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)\leftrightarrow \forall y\in B\left(f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x\underset{\dot{}}{+}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)$$
24	12 23	anbi12d	$$⊢r=R\to \left(\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)\leftrightarrow \left(\left(f\left(x\right)=0\leftrightarrow x=\underset{\dot{}}{0}\right)\wedge \forall y\in B\left(f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x\underset{\dot{}}{+}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right)$$
25	7 24	raleqbidv	$$⊢r=R\to \left(\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)\leftrightarrow \forall x\in B\left(\left(f\left(x\right)=0\leftrightarrow x=\underset{\dot{}}{0}\right)\wedge \forall y\in B\left(f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x\underset{\dot{}}{+}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right)$$
26	8 25	rabeqbidv	$$⊢r=R\to \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\}=\left\{f\in \left({\left[0,\mathrm{+\infty }\right)}^B\right)|\forall x\in B\left(\left(f\left(x\right)=0\leftrightarrow x=\underset{\dot{}}{0}\right)\wedge \forall y\in B\left(f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x\underset{\dot{}}{+}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right\}$$
27		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)$$
28		ovex	$$⊢{\left[0,\mathrm{+\infty }\right)}^B\in \mathrm{V}$$
29	28	rabex	$$⊢\left\{f\in \left({\left[0,\mathrm{+\infty }\right)}^B\right)|\forall x\in B\left(\left(f\left(x\right)=0\leftrightarrow x=\underset{\dot{}}{0}\right)\wedge \forall y\in B\left(f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x\underset{\dot{}}{+}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right\}\in \mathrm{V}$$
30	26 27 29	fvmpt	$$⊢R\in \mathrm{Ring}\to \mathrm{AbsVal}\left(R\right)=\left\{f\in \left({\left[0,\mathrm{+\infty }\right)}^B\right)|\forall x\in B\left(\left(f\left(x\right)=0\leftrightarrow x=\underset{\dot{}}{0}\right)\wedge \forall y\in B\left(f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x\underset{\dot{}}{+}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right\}$$
31	1 30	syl5eq	$$⊢R\in \mathrm{Ring}\to A=\left\{f\in \left({\left[0,\mathrm{+\infty }\right)}^B\right)|\forall x\in B\left(\left(f\left(x\right)=0\leftrightarrow x=\underset{\dot{}}{0}\right)\wedge \forall y\in B\left(f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)f\left(y\right)\wedge f\left(x\underset{\dot{}}{+}y\right)\le f\left(x\right)+f\left(y\right)\right)\right)\right\}$$