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 = x ∈ X , y ∈ X ⟼ if x = y 0 1
Assertion dscmet ⊢ X ∈ V → D ∈ Met ⁡ X

Proof

Step Hyp Ref Expression
1 dscmet.1 ⊢ D = x ∈ X , y ∈ X ⟼ if x = y 0 1
2 0re ⊢ 0 ∈ ℝ
3 1re ⊢ 1 ∈ ℝ
4 2 3 ifcli ⊢ if x = y 0 1 ∈ ℝ
5 4 rgen2w ⊢ ∀ x ∈ X ∀ y ∈ X if x = y 0 1 ∈ ℝ
6 1 fmpo ⊢ ∀ x ∈ X ∀ y ∈ X if x = y 0 1 ∈ ℝ ↔ D : X × X ⟶ ℝ
7 5 6 mpbi ⊢ D : X × X ⟶ ℝ
8 equequ1 ⊢ x = w → x = y ↔ w = y
9 8 ifbid ⊢ x = w → if x = y 0 1 = if w = y 0 1
10 equequ2 ⊢ y = v → w = y ↔ w = v
11 10 ifbid ⊢ y = v → if w = y 0 1 = if w = v 0 1
12 0nn0 ⊢ 0 ∈ ℕ 0
13 1nn0 ⊢ 1 ∈ ℕ 0
14 12 13 ifcli ⊢ if w = v 0 1 ∈ ℕ 0
15 14 elexi ⊢ if w = v 0 1 ∈ V
16 9 11 1 15 ovmpo ⊢ w ∈ X ∧ v ∈ X → w D v = if w = v 0 1
17 16 eqeq1d ⊢ w ∈ X ∧ v ∈ X → w D v = 0 ↔ if w = v 0 1 = 0
18 iffalse ⊢ ¬ w = v → if w = v 0 1 = 1
19 ax-1ne0 ⊢ 1 ≠ 0
20 19 a1i ⊢ ¬ w = v → 1 ≠ 0
21 18 20 eqnetrd ⊢ ¬ w = v → if w = v 0 1 ≠ 0
22 21 neneqd ⊢ ¬ w = v → ¬ if w = v 0 1 = 0
23 22 con4i ⊢ if w = v 0 1 = 0 → w = v
24 iftrue ⊢ w = v → if w = v 0 1 = 0
25 23 24 impbii ⊢ if w = v 0 1 = 0 ↔ w = v
26 17 25 bitrdi ⊢ w ∈ X ∧ v ∈ X → w D v = 0 ↔ w = v
27 12 13 ifcli ⊢ if u = w 0 1 ∈ ℕ 0
28 12 13 ifcli ⊢ if u = v 0 1 ∈ ℕ 0
29 27 28 nn0addcli ⊢ if u = w 0 1 + if u = v 0 1 ∈ ℕ 0
30 elnn0 ⊢ if u = w 0 1 + if u = v 0 1 ∈ ℕ 0 ↔ if u = w 0 1 + if u = v 0 1 ∈ ℕ ∨ if u = w 0 1 + if u = v 0 1 = 0
31 29 30 mpbi ⊢ if u = w 0 1 + if u = v 0 1 ∈ ℕ ∨ if u = w 0 1 + if u = v 0 1 = 0
32 breq1 ⊢ 0 = if w = v 0 1 → 0 ≤ 1 ↔ if w = v 0 1 ≤ 1
33 breq1 ⊢ 1 = if w = v 0 1 → 1 ≤ 1 ↔ if w = v 0 1 ≤ 1
34 0le1 ⊢ 0 ≤ 1
35 3 leidi ⊢ 1 ≤ 1
36 32 33 34 35 keephyp ⊢ if w = v 0 1 ≤ 1
37 nnge1 ⊢ if u = w 0 1 + if u = v 0 1 ∈ ℕ → 1 ≤ if u = w 0 1 + if u = v 0 1
38 14 nn0rei ⊢ if w = v 0 1 ∈ ℝ
39 29 nn0rei ⊢ if u = w 0 1 + if u = v 0 1 ∈ ℝ
40 38 3 39 letri ⊢ if w = v 0 1 ≤ 1 ∧ 1 ≤ if u = w 0 1 + if u = v 0 1 → if w = v 0 1 ≤ if u = w 0 1 + if u = v 0 1
41 36 37 40 sylancr ⊢ if u = w 0 1 + if u = v 0 1 ∈ ℕ → if w = v 0 1 ≤ if u = w 0 1 + if u = v 0 1
42 27 nn0ge0i ⊢ 0 ≤ if u = w 0 1
43 28 nn0ge0i ⊢ 0 ≤ if u = v 0 1
44 27 nn0rei ⊢ if u = w 0 1 ∈ ℝ
45 28 nn0rei ⊢ if u = v 0 1 ∈ ℝ
46 44 45 add20i ⊢ 0 ≤ if u = w 0 1 ∧ 0 ≤ if u = v 0 1 → if u = w 0 1 + if u = v 0 1 = 0 ↔ if u = w 0 1 = 0 ∧ if u = v 0 1 = 0
47 42 43 46 mp2an ⊢ if u = w 0 1 + if u = v 0 1 = 0 ↔ if u = w 0 1 = 0 ∧ if u = v 0 1 = 0
48 equequ2 ⊢ v = w → u = v ↔ u = w
49 48 ifbid ⊢ v = w → if u = v 0 1 = if u = w 0 1
50 49 eqeq1d ⊢ v = w → if u = v 0 1 = 0 ↔ if u = w 0 1 = 0
51 50 48 bibi12d ⊢ v = w → if u = v 0 1 = 0 ↔ u = v ↔ if u = w 0 1 = 0 ↔ u = w
52 equequ1 ⊢ w = u → w = v ↔ u = v
53 52 ifbid ⊢ w = u → if w = v 0 1 = if u = v 0 1
54 53 eqeq1d ⊢ w = u → if w = v 0 1 = 0 ↔ if u = v 0 1 = 0
55 54 52 bibi12d ⊢ w = u → if w = v 0 1 = 0 ↔ w = v ↔ if u = v 0 1 = 0 ↔ u = v
56 55 25 chvarvv ⊢ if u = v 0 1 = 0 ↔ u = v
57 51 56 chvarvv ⊢ if u = w 0 1 = 0 ↔ u = w
58 eqtr2 ⊢ u = w ∧ u = v → w = v
59 57 56 58 syl2anb ⊢ if u = w 0 1 = 0 ∧ if u = v 0 1 = 0 → w = v
60 59 iftrued ⊢ if u = w 0 1 = 0 ∧ if u = v 0 1 = 0 → if w = v 0 1 = 0
61 2 leidi ⊢ 0 ≤ 0
62 60 61 eqbrtrdi ⊢ if u = w 0 1 = 0 ∧ if u = v 0 1 = 0 → if w = v 0 1 ≤ 0
63 47 62 sylbi ⊢ if u = w 0 1 + if u = v 0 1 = 0 → if w = v 0 1 ≤ 0
64 id ⊢ if u = w 0 1 + if u = v 0 1 = 0 → if u = w 0 1 + if u = v 0 1 = 0
65 63 64 breqtrrd ⊢ if u = w 0 1 + if u = v 0 1 = 0 → if w = v 0 1 ≤ if u = w 0 1 + if u = v 0 1
66 41 65 jaoi ⊢ if u = w 0 1 + if u = v 0 1 ∈ ℕ ∨ if u = w 0 1 + if u = v 0 1 = 0 → if w = v 0 1 ≤ if u = w 0 1 + if u = v 0 1
67 31 66 mp1i ⊢ u ∈ X ∧ w ∈ X ∧ v ∈ X → if w = v 0 1 ≤ if u = w 0 1 + if u = v 0 1
68 16 adantl ⊢ u ∈ X ∧ w ∈ X ∧ v ∈ X → w D v = if w = v 0 1
69 eqeq12 ⊢ x = u ∧ y = w → x = y ↔ u = w
70 69 ifbid ⊢ x = u ∧ y = w → if x = y 0 1 = if u = w 0 1
71 27 elexi ⊢ if u = w 0 1 ∈ V
72 70 1 71 ovmpoa ⊢ u ∈ X ∧ w ∈ X → u D w = if u = w 0 1
73 72 adantrr ⊢ u ∈ X ∧ w ∈ X ∧ v ∈ X → u D w = if u = w 0 1
74 eqeq12 ⊢ x = u ∧ y = v → x = y ↔ u = v
75 74 ifbid ⊢ x = u ∧ y = v → if x = y 0 1 = if u = v 0 1
76 28 elexi ⊢ if u = v 0 1 ∈ V
77 75 1 76 ovmpoa ⊢ u ∈ X ∧ v ∈ X → u D v = if u = v 0 1
78 77 adantrl ⊢ u ∈ X ∧ w ∈ X ∧ v ∈ X → u D v = if u = v 0 1
79 73 78 oveq12d ⊢ u ∈ X ∧ w ∈ X ∧ v ∈ X → u D w + u D v = if u = w 0 1 + if u = v 0 1
80 67 68 79 3brtr4d ⊢ u ∈ X ∧ w ∈ X ∧ v ∈ X → w D v ≤ u D w + u D v
81 80 expcom ⊢ w ∈ X ∧ v ∈ X → u ∈ X → w D v ≤ u D w + u D v
82 81 ralrimiv ⊢ w ∈ X ∧ v ∈ X → ∀ u ∈ X w D v ≤ u D w + u D v
83 26 82 jca ⊢ w ∈ X ∧ v ∈ X → w D v = 0 ↔ w = v ∧ ∀ u ∈ X w D v ≤ u D w + u D v
84 83 rgen2 ⊢ ∀ w ∈ X ∀ v ∈ X w D v = 0 ↔ w = v ∧ ∀ u ∈ X w D v ≤ u D w + u D v
85 7 84 pm3.2i ⊢ D : X × X ⟶ ℝ ∧ ∀ w ∈ X ∀ v ∈ X w D v = 0 ↔ w = v ∧ ∀ u ∈ X w D v ≤ u D w + u D v
86 ismet ⊢ X ∈ V → D ∈ Met ⁡ X ↔ D : X × X ⟶ ℝ ∧ ∀ w ∈ X ∀ v ∈ X w D v = 0 ↔ w = v ∧ ∀ u ∈ X w D v ≤ u D w + u D v
87 85 86 mpbiri ⊢ X ∈ V → D ∈ Met ⁡ X