Metamath Proof Explorer

Theorem xrsds

Description: The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypothesis xrsds.d 
|- D = ( dist ` RR*s )
Assertion xrsds 
|- D = ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) )

Proof

Step Hyp Ref Expression
1 xrsds.d 
 |-  D = ( dist ` RR*s )
2 id 
 |-  ( y e. RR* -> y e. RR* )
3 xnegcl 
 |-  ( x e. RR* -> -e x e. RR* )
4 xaddcl 
 |-  ( ( y e. RR* /\ -e x e. RR* ) -> ( y +e -e x ) e. RR* )
5 2 3 4 syl2anr 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( y +e -e x ) e. RR* )
6 xnegcl 
 |-  ( y e. RR* -> -e y e. RR* )
7 xaddcl 
 |-  ( ( x e. RR* /\ -e y e. RR* ) -> ( x +e -e y ) e. RR* )
8 6 7 sylan2 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x +e -e y ) e. RR* )
9 5 8 ifcld 
 |-  ( ( x e. RR* /\ y e. RR* ) -> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) e. RR* )
10 9 rgen2 
 |-  A. x e. RR* A. y e. RR* if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) e. RR*
11 eqid 
 |-  ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) = ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) )
12 11 fmpo 
 |-  ( A. x e. RR* A. y e. RR* if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) e. RR* <-> ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) : ( RR* X. RR* ) --> RR* )
13 10 12 mpbi 
 |-  ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) : ( RR* X. RR* ) --> RR*
14 xrex 
 |-  RR* e. _V
15 14 14 xpex 
 |-  ( RR* X. RR* ) e. _V
16 fex2 
 |-  ( ( ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) : ( RR* X. RR* ) --> RR* /\ ( RR* X. RR* ) e. _V /\ RR* e. _V ) -> ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) e. _V )
17 13 15 14 16 mp3an 
 |-  ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) e. _V
18 df-xrs 
 |-  RR*s = ( { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , +e >. , <. ( .r ` ndx ) , *e >. } u. { <. ( TopSet ` ndx ) , ( ordTop ` <_ ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) >. } )
19 18 odrngds 
 |-  ( ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) e. _V -> ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) = ( dist ` RR*s ) )
20 17 19 ax-mp 
 |-  ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) = ( dist ` RR*s )
21 1 20 eqtr4i 
 |-  D = ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) )