Metamath Proof Explorer

Theorem xrsdsre

Description: The metric on the extended reals coincides with the usual metric on the reals. (Contributed by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypothesis xrsxmet.1 
|- D = ( dist ` RR*s )
Assertion xrsdsre 
|- ( D |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )

Proof

Step Hyp Ref Expression
1 xrsxmet.1 
 |-  D = ( dist ` RR*s )
2 1 xrsdsreval 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x D y ) = ( abs ` ( x - y ) ) )
3 ovres 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x ( D |` ( RR X. RR ) ) y ) = ( x D y ) )
4 eqid 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
5 4 remetdval 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x ( ( abs o. - ) |` ( RR X. RR ) ) y ) = ( abs ` ( x - y ) ) )
6 2 3 5 3eqtr4d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x ( D |` ( RR X. RR ) ) y ) = ( x ( ( abs o. - ) |` ( RR X. RR ) ) y ) )
7 6 rgen2 
 |-  A. x e. RR A. y e. RR ( x ( D |` ( RR X. RR ) ) y ) = ( x ( ( abs o. - ) |` ( RR X. RR ) ) y )
8 1 xrsxmet 
 |-  D e. ( *Met ` RR* )
9 xmetf 
 |-  ( D e. ( *Met ` RR* ) -> D : ( RR* X. RR* ) --> RR* )
10 ffn 
 |-  ( D : ( RR* X. RR* ) --> RR* -> D Fn ( RR* X. RR* ) )
11 8 9 10 mp2b 
 |-  D Fn ( RR* X. RR* )
12 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
13 fnssres 
 |-  ( ( D Fn ( RR* X. RR* ) /\ ( RR X. RR ) C_ ( RR* X. RR* ) ) -> ( D |` ( RR X. RR ) ) Fn ( RR X. RR ) )
14 11 12 13 mp2an 
 |-  ( D |` ( RR X. RR ) ) Fn ( RR X. RR )
15 cnmet 
 |-  ( abs o. - ) e. ( Met ` CC )
16 metf 
 |-  ( ( abs o. - ) e. ( Met ` CC ) -> ( abs o. - ) : ( CC X. CC ) --> RR )
17 ffn 
 |-  ( ( abs o. - ) : ( CC X. CC ) --> RR -> ( abs o. - ) Fn ( CC X. CC ) )
18 15 16 17 mp2b 
 |-  ( abs o. - ) Fn ( CC X. CC )
19 ax-resscn 
 |-  RR C_ CC
20 xpss12 
 |-  ( ( RR C_ CC /\ RR C_ CC ) -> ( RR X. RR ) C_ ( CC X. CC ) )
21 19 19 20 mp2an 
 |-  ( RR X. RR ) C_ ( CC X. CC )
22 fnssres 
 |-  ( ( ( abs o. - ) Fn ( CC X. CC ) /\ ( RR X. RR ) C_ ( CC X. CC ) ) -> ( ( abs o. - ) |` ( RR X. RR ) ) Fn ( RR X. RR ) )
23 18 21 22 mp2an 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) Fn ( RR X. RR )
24 eqfnov2 
 |-  ( ( ( D |` ( RR X. RR ) ) Fn ( RR X. RR ) /\ ( ( abs o. - ) |` ( RR X. RR ) ) Fn ( RR X. RR ) ) -> ( ( D |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) ) <-> A. x e. RR A. y e. RR ( x ( D |` ( RR X. RR ) ) y ) = ( x ( ( abs o. - ) |` ( RR X. RR ) ) y ) ) )
25 14 23 24 mp2an 
 |-  ( ( D |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) ) <-> A. x e. RR A. y e. RR ( x ( D |` ( RR X. RR ) ) y ) = ( x ( ( abs o. - ) |` ( RR X. RR ) ) y ) )
26 7 25 mpbir 
 |-  ( D |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )