Theorem abvcl

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	abvcl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		abvf.a	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
2		abvf.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3	1 2	abvf	⊢ ( 𝐹 ∈ 𝐴 → 𝐹 : 𝐵 ⟶ ℝ )
4	3	ffvelrnda	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ∈ ℝ )