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	|- A = ( AbsVal ` R )
	abvf.b	|- B = ( Base ` R )
Assertion	abvcl	|- ( ( F e. A /\ X e. B ) -> ( F ` X ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		abvf.a	|- A = ( AbsVal ` R )
2		abvf.b	|- B = ( Base ` R )
3	1 2	abvf	|- ( F e. A -> F : B --> RR )
4	3	ffvelcdmda	|- ( ( F e. A /\ X e. B ) -> ( F ` X ) e. RR )