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	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
	abvf.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	abvf	⊢ ( 𝐹 ∈ 𝐴 → 𝐹 : 𝐵 ⟶ ℝ )

Proof

Step	Hyp	Ref	Expression
1		abvf.a	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
2		abvf.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3	1 2	abvfge0	⊢ ( 𝐹 ∈ 𝐴 → 𝐹 : 𝐵 ⟶ ( 0 [,) +∞ ) )
4		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
5		fss	⊢ ( ( 𝐹 : 𝐵 ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ ) → 𝐹 : 𝐵 ⟶ ℝ )
6	3 4 5	sylancl	⊢ ( 𝐹 ∈ 𝐴 → 𝐹 : 𝐵 ⟶ ℝ )