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

Metamath Proof Explorer

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 eqtrid 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A D B ) = ( abs ` ( A - B ) ) )