Theorem remetdval

Description: Value of the distance function of the metric space of real numbers. (Contributed by NM, 16-May-2007)

	Ref	Expression
Hypothesis	remet.1	|- D = ( ( abs o. - ) |` ( RR X. RR ) )
Assertion	remetdval	|- ( ( A e. RR /\ B e. RR ) -> ( A D B ) = ( abs ` ( A - B ) ) )

Proof

Step	Hyp	Ref	Expression
1		remet.1	|- D = ( ( abs o. - ) |` ( RR X. RR ) )
2		df-ov	|- ( A D B ) = ( D ` <. A , B >. )
3	1	fveq1i	|- ( D ` <. A , B >. ) = ( ( ( abs o. - ) |` ( RR X. RR ) ) ` <. A , B >. )
4	2 3	eqtri	|- ( A D B ) = ( ( ( abs o. - ) |` ( RR X. RR ) ) ` <. A , B >. )
5		opelxpi	|- ( ( A e. RR /\ B e. RR ) -> <. A , B >. e. ( RR X. RR ) )
6	5	fvresd	|- ( ( A e. RR /\ B e. RR ) -> ( ( ( abs o. - ) |` ( RR X. RR ) ) ` <. A , B >. ) = ( ( abs o. - ) ` <. A , B >. ) )
7		df-ov	|- ( A ( abs o. - ) B ) = ( ( abs o. - ) ` <. A , B >. )
8		recn	|- ( A e. RR -> A e. CC )
9		recn	|- ( B e. RR -> B e. CC )
10		eqid	|- ( abs o. - ) = ( abs o. - )
11	10	cnmetdval	|- ( ( A e. CC /\ B e. CC ) -> ( A ( abs o. - ) B ) = ( abs ` ( A - B ) ) )
12	8 9 11	syl2an	|- ( ( A e. RR /\ B e. RR ) -> ( A ( abs o. - ) B ) = ( abs ` ( A - B ) ) )
13	7 12	eqtr3id	|- ( ( A e. RR /\ B e. RR ) -> ( ( abs o. - ) ` <. A , B >. ) = ( abs ` ( A - B ) ) )
14	6 13	eqtrd	|- ( ( A e. RR /\ B e. RR ) -> ( ( ( abs o. - ) |` ( RR X. RR ) ) ` <. A , B >. ) = ( abs ` ( A - B ) ) )
15	4 14	syl5eq	|- ( ( A e. RR /\ B e. RR ) -> ( A D B ) = ( abs ` ( A - B ) ) )