Metamath Proof Explorer

Theorem xrsdsval

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 xrsdsval 
|- ( ( A e. RR* /\ B e. RR* ) -> ( A D B ) = if ( A <_ B , ( B +e -e A ) , ( A +e -e B ) ) )

Proof

Step Hyp Ref Expression
1 xrsds.d 
 |-  D = ( dist ` RR*s )
2 breq12 
 |-  ( ( x = A /\ y = B ) -> ( x <_ y <-> A <_ B ) )
3 id 
 |-  ( y = B -> y = B )
4 xnegeq 
 |-  ( x = A -> -e x = -e A )
5 3 4 oveqan12rd 
 |-  ( ( x = A /\ y = B ) -> ( y +e -e x ) = ( B +e -e A ) )
6 id 
 |-  ( x = A -> x = A )
7 xnegeq 
 |-  ( y = B -> -e y = -e B )
8 6 7 oveqan12d 
 |-  ( ( x = A /\ y = B ) -> ( x +e -e y ) = ( A +e -e B ) )
9 2 5 8 ifbieq12d 
 |-  ( ( x = A /\ y = B ) -> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) = if ( A <_ B , ( B +e -e A ) , ( A +e -e B ) ) )
10 1 xrsds 
 |-  D = ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) )
11 ovex 
 |-  ( B +e -e A ) e. _V
12 ovex 
 |-  ( A +e -e B ) e. _V
13 11 12 ifex 
 |-  if ( A <_ B , ( B +e -e A ) , ( A +e -e B ) ) e. _V
14 9 10 13 ovmpoa 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A D B ) = if ( A <_ B , ( B +e -e A ) , ( A +e -e B ) ) )