Metamath Proof Explorer

Theorem xrsdsreval

Description: The metric of the extended real number structure coincides with the real number metric on the reals. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypothesis xrsds.d 
|- D = ( dist ` RR*s )
Assertion xrsdsreval 
|- ( ( A e. RR /\ B e. RR ) -> ( A D B ) = ( abs ` ( A - B ) ) )

Proof

Step Hyp Ref Expression
1 xrsds.d 
 |-  D = ( dist ` RR*s )
2 rexr 
 |-  ( A e. RR -> A e. RR* )
3 rexr 
 |-  ( B e. RR -> B e. RR* )
4 1 xrsdsval 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A D B ) = if ( A <_ B , ( B +e -e A ) , ( A +e -e B ) ) )
5 2 3 4 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A D B ) = if ( A <_ B , ( B +e -e A ) , ( A +e -e B ) ) )
6 rexsub 
 |-  ( ( B e. RR /\ A e. RR ) -> ( B +e -e A ) = ( B - A ) )
7 6 ancoms 
 |-  ( ( A e. RR /\ B e. RR ) -> ( B +e -e A ) = ( B - A ) )
8 7 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( B +e -e A ) = ( B - A ) )
9 abssuble0 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( abs ` ( A - B ) ) = ( B - A ) )
10 9 3expa 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( abs ` ( A - B ) ) = ( B - A ) )
11 8 10 eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( B +e -e A ) = ( abs ` ( A - B ) ) )
12 rexsub 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A +e -e B ) = ( A - B ) )
13 12 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A <_ B ) -> ( A +e -e B ) = ( A - B ) )
14 letric 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A <_ B \/ B <_ A ) )
15 14 orcanai 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A <_ B ) -> B <_ A )
16 abssubge0 
 |-  ( ( B e. RR /\ A e. RR /\ B <_ A ) -> ( abs ` ( A - B ) ) = ( A - B ) )
17 16 3com12 
 |-  ( ( A e. RR /\ B e. RR /\ B <_ A ) -> ( abs ` ( A - B ) ) = ( A - B ) )
18 17 3expa 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B <_ A ) -> ( abs ` ( A - B ) ) = ( A - B ) )
19 15 18 syldan 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A <_ B ) -> ( abs ` ( A - B ) ) = ( A - B ) )
20 13 19 eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. A <_ B ) -> ( A +e -e B ) = ( abs ` ( A - B ) ) )
21 11 20 ifeqda 
 |-  ( ( A e. RR /\ B e. RR ) -> if ( A <_ B , ( B +e -e A ) , ( A +e -e B ) ) = ( abs ` ( A - B ) ) )
22 5 21 eqtrd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A D B ) = ( abs ` ( A - B ) ) )