Theorem abvf

Description: An absolute value is a function from the ring to the 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	abvf	$$⊢F\in A\to F:B⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		abvf.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
2		abvf.b	$$⊢B={\mathrm{Base}}_R$$
3	1 2	abvfge0	$$⊢F\in A\to F:B⟶\left[0,\mathrm{+\infty }\right)$$
4		rge0ssre	$$⊢\left[0,\mathrm{+\infty }\right)\subseteq ℝ$$
5		fss	$$⊢\left(F:B⟶\left[0,\mathrm{+\infty }\right)\wedge \left[0,\mathrm{+\infty }\right)\subseteq ℝ\right)\to F:B⟶ℝ$$
6	3 4 5	sylancl	$$⊢F\in A\to F:B⟶ℝ$$