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 ⊢ 𝐷 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ if ( 𝑥 = 𝑦 , 0 , 1 ) )
Assertion dscmet ( 𝑋 ∈ 𝑉 → 𝐷 ∈ ( Met ‘ 𝑋 ) )

Proof

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