Theorem remet

Description: The absolute value metric determines a metric space on the reals. (Contributed by NM, 10-Feb-2007)

	Ref	Expression
Hypothesis	remet.1	|- D = ( ( abs o. - ) |` ( RR X. RR ) )
Assertion	remet	|- D e. ( Met ` RR )

Proof

Step	Hyp	Ref	Expression
1		remet.1	|- D = ( ( abs o. - ) |` ( RR X. RR ) )
2		cnmet	|- ( abs o. - ) e. ( Met ` CC )
3		ax-resscn	|- RR C_ CC
4		metres2	|- ( ( ( abs o. - ) e. ( Met ` CC ) /\ RR C_ CC ) -> ( ( abs o. - ) |` ( RR X. RR ) ) e. ( Met ` RR ) )
5	2 3 4	mp2an	|- ( ( abs o. - ) |` ( RR X. RR ) ) e. ( Met ` RR )
6	1 5	eqeltri	|- D e. ( Met ` RR )