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 2
Assertion remetdval A B A D B = A B

Proof

Step Hyp Ref Expression
1 remet.1 D = abs 2
2 df-ov A D B = D A B
3 1 fveq1i D A B = abs 2 A B
4 2 3 eqtri A D B = abs 2 A B
5 opelxpi A B A B 2
6 5 fvresd A B abs 2 A B = abs A B
7 df-ov A abs B = abs A B
8 recn A A
9 recn B B
10 eqid abs = abs
11 10 cnmetdval A B A abs B = A B
12 8 9 11 syl2an A B A abs B = A B
13 7 12 syl5eqr A B abs A B = A B
14 6 13 eqtrd A B abs 2 A B = A B
15 4 14 syl5eq A B A D B = A B