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\leftrightarrow \left(F:B⟶\left[0,\mathrm{+\infty }\right)\wedge \forall x\in B\left(\left(F\left(x\right)=0\leftrightarrow x=0_R\right)\wedge \forall y\in B\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\leftrightarrow \left(F:B⟶\left[0,\mathrm{+\infty }\right)\wedge \forall x\in B\left(\left(F\left(x\right)=0\leftrightarrow x=0_R\right)\wedge \forall y\in B\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\left(\left(F\left(x\right)=0\leftrightarrow x=0_R\right)\wedge \forall y\in B\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)$$