Theorem isabv

Description: Elementhood in 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	isabv	$$⊢R\in \mathrm{Ring}\to \left(F\in A\leftrightarrow \left(F:B⟶\left[0,\mathrm{+\infty }\right)\wedge \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)\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	1 2 3 4 5	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\}$$
7	6	eleq2d	$$⊢R\in \mathrm{Ring}\to \left(F\in A\leftrightarrow F\in \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\}\right)$$
8		fveq1	$$⊢f=F\to f\left(x\right)=F\left(x\right)$$
9	8	eqeq1d	$$⊢f=F\to \left(f\left(x\right)=0\leftrightarrow F\left(x\right)=0\right)$$
10	9	bibi1d	$$⊢f=F\to \left(\left(f\left(x\right)=0\leftrightarrow x=\underset{\dot{}}{0}\right)\leftrightarrow \left(F\left(x\right)=0\leftrightarrow x=\underset{\dot{}}{0}\right)\right)$$
11		fveq1	$$⊢f=F\to f\left(x\underset{\dot{}}{·}y\right)=F\left(x\underset{\dot{}}{·}y\right)$$
12		fveq1	$$⊢f=F\to f\left(y\right)=F\left(y\right)$$
13	8 12	oveq12d	$$⊢f=F\to f\left(x\right)f\left(y\right)=F\left(x\right)F\left(y\right)$$
14	11 13	eqeq12d	$$⊢f=F\to \left(f\left(x\underset{\dot{}}{·}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)$$
15		fveq1	$$⊢f=F\to f\left(x\underset{\dot{}}{+}y\right)=F\left(x\underset{\dot{}}{+}y\right)$$
16	8 12	oveq12d	$$⊢f=F\to f\left(x\right)+f\left(y\right)=F\left(x\right)+F\left(y\right)$$
17	15 16	breq12d	$$⊢f=F\to \left(f\left(x\underset{\dot{}}{+}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)$$
18	14 17	anbi12d	$$⊢f=F\to \left(\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)\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)$$
19	18	ralbidv	$$⊢f=F\to \left(\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)\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)$$
20	10 19	anbi12d	$$⊢f=F\to \left(\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)\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)$$
21	20	ralbidv	$$⊢f=F\to \left(\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)\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)$$
22	21	elrab	$$⊢F\in \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\}\leftrightarrow \left(F\in \left({\left[0,\mathrm{+\infty }\right)}^B\right)\wedge \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)$$
23		ovex	$$⊢\left[0,\mathrm{+\infty }\right)\in \mathrm{V}$$
24	2	fvexi	$$⊢B\in \mathrm{V}$$
25	23 24	elmap	$$⊢F\in \left({\left[0,\mathrm{+\infty }\right)}^B\right)\leftrightarrow F:B⟶\left[0,\mathrm{+\infty }\right)$$
26	25	anbi1i	$$⊢\left(F\in \left({\left[0,\mathrm{+\infty }\right)}^B\right)\wedge \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)\leftrightarrow \left(F:B⟶\left[0,\mathrm{+\infty }\right)\wedge \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	22 26	bitri	$$⊢F\in \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\}\leftrightarrow \left(F:B⟶\left[0,\mathrm{+\infty }\right)\wedge \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)$$
28	7 27	bitrdi	$$⊢R\in \mathrm{Ring}\to \left(F\in A\leftrightarrow \left(F:B⟶\left[0,\mathrm{+\infty }\right)\wedge \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)\right)$$