Metamath Proof Explorer


Theorem dscmet

Description: The discrete metric on any set X . Definition 1.1-8 of Kreyszig p. 8. (Contributed by FL, 12-Oct-2006)

Ref Expression
Hypothesis dscmet.1 D=xX,yXifx=y01
Assertion dscmet XVDMetX

Proof

Step Hyp Ref Expression
1 dscmet.1 D=xX,yXifx=y01
2 0re 0
3 1re 1
4 2 3 ifcli ifx=y01
5 4 rgen2w xXyXifx=y01
6 1 fmpo xXyXifx=y01D:X×X
7 5 6 mpbi D:X×X
8 equequ1 x=wx=yw=y
9 8 ifbid x=wifx=y01=ifw=y01
10 equequ2 y=vw=yw=v
11 10 ifbid y=vifw=y01=ifw=v01
12 0nn0 00
13 1nn0 10
14 12 13 ifcli ifw=v010
15 14 elexi ifw=v01V
16 9 11 1 15 ovmpo wXvXwDv=ifw=v01
17 16 eqeq1d wXvXwDv=0ifw=v01=0
18 iffalse ¬w=vifw=v01=1
19 ax-1ne0 10
20 19 a1i ¬w=v10
21 18 20 eqnetrd ¬w=vifw=v010
22 21 neneqd ¬w=v¬ifw=v01=0
23 22 con4i ifw=v01=0w=v
24 iftrue w=vifw=v01=0
25 23 24 impbii ifw=v01=0w=v
26 17 25 bitrdi wXvXwDv=0w=v
27 12 13 ifcli ifu=w010
28 12 13 ifcli ifu=v010
29 27 28 nn0addcli ifu=w01+ifu=v010
30 elnn0 ifu=w01+ifu=v010ifu=w01+ifu=v01ifu=w01+ifu=v01=0
31 29 30 mpbi ifu=w01+ifu=v01ifu=w01+ifu=v01=0
32 breq1 0=ifw=v0101ifw=v011
33 breq1 1=ifw=v0111ifw=v011
34 0le1 01
35 3 leidi 11
36 32 33 34 35 keephyp ifw=v011
37 nnge1 ifu=w01+ifu=v011ifu=w01+ifu=v01
38 14 nn0rei ifw=v01
39 29 nn0rei ifu=w01+ifu=v01
40 38 3 39 letri ifw=v0111ifu=w01+ifu=v01ifw=v01ifu=w01+ifu=v01
41 36 37 40 sylancr ifu=w01+ifu=v01ifw=v01ifu=w01+ifu=v01
42 27 nn0ge0i 0ifu=w01
43 28 nn0ge0i 0ifu=v01
44 27 nn0rei ifu=w01
45 28 nn0rei ifu=v01
46 44 45 add20i 0ifu=w010ifu=v01ifu=w01+ifu=v01=0ifu=w01=0ifu=v01=0
47 42 43 46 mp2an ifu=w01+ifu=v01=0ifu=w01=0ifu=v01=0
48 equequ2 v=wu=vu=w
49 48 ifbid v=wifu=v01=ifu=w01
50 49 eqeq1d v=wifu=v01=0ifu=w01=0
51 50 48 bibi12d v=wifu=v01=0u=vifu=w01=0u=w
52 equequ1 w=uw=vu=v
53 52 ifbid w=uifw=v01=ifu=v01
54 53 eqeq1d w=uifw=v01=0ifu=v01=0
55 54 52 bibi12d w=uifw=v01=0w=vifu=v01=0u=v
56 55 25 chvarvv ifu=v01=0u=v
57 51 56 chvarvv ifu=w01=0u=w
58 eqtr2 u=wu=vw=v
59 57 56 58 syl2anb ifu=w01=0ifu=v01=0w=v
60 59 iftrued ifu=w01=0ifu=v01=0ifw=v01=0
61 2 leidi 00
62 60 61 eqbrtrdi ifu=w01=0ifu=v01=0ifw=v010
63 47 62 sylbi ifu=w01+ifu=v01=0ifw=v010
64 id ifu=w01+ifu=v01=0ifu=w01+ifu=v01=0
65 63 64 breqtrrd ifu=w01+ifu=v01=0ifw=v01ifu=w01+ifu=v01
66 41 65 jaoi ifu=w01+ifu=v01ifu=w01+ifu=v01=0ifw=v01ifu=w01+ifu=v01
67 31 66 mp1i uXwXvXifw=v01ifu=w01+ifu=v01
68 16 adantl uXwXvXwDv=ifw=v01
69 eqeq12 x=uy=wx=yu=w
70 69 ifbid x=uy=wifx=y01=ifu=w01
71 27 elexi ifu=w01V
72 70 1 71 ovmpoa uXwXuDw=ifu=w01
73 72 adantrr uXwXvXuDw=ifu=w01
74 eqeq12 x=uy=vx=yu=v
75 74 ifbid x=uy=vifx=y01=ifu=v01
76 28 elexi ifu=v01V
77 75 1 76 ovmpoa uXvXuDv=ifu=v01
78 77 adantrl uXwXvXuDv=ifu=v01
79 73 78 oveq12d uXwXvXuDw+uDv=ifu=w01+ifu=v01
80 67 68 79 3brtr4d uXwXvXwDvuDw+uDv
81 80 expcom wXvXuXwDvuDw+uDv
82 81 ralrimiv wXvXuXwDvuDw+uDv
83 26 82 jca wXvXwDv=0w=vuXwDvuDw+uDv
84 83 rgen2 wXvXwDv=0w=vuXwDvuDw+uDv
85 7 84 pm3.2i D:X×XwXvXwDv=0w=vuXwDvuDw+uDv
86 ismet XVDMetXD:X×XwXvXwDv=0w=vuXwDvuDw+uDv
87 85 86 mpbiri XVDMetX