Metamath Proof Explorer
Description: An absolute value is a function from the ring to the real numbers.
(Contributed by Mario Carneiro, 8Sep2014)


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