This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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