MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dscmet Structured version   Visualization version   GIF version

Theorem dscmet 23174
Description: The discrete metric on any set 𝑋. Definition 1.1-8 of [Kreyszig] p. 8. (Contributed by FL, 12-Oct-2006.)
Hypothesis
Ref Expression
dscmet.1 𝐷 = (𝑥𝑋, 𝑦𝑋 ↦ if(𝑥 = 𝑦, 0, 1))
Assertion
Ref Expression
dscmet (𝑋𝑉𝐷 ∈ (Met‘𝑋))
Distinct variable group:   𝑥,𝑦,𝑋
Allowed substitution hints:   𝐷(𝑥,𝑦)   𝑉(𝑥,𝑦)

Proof of Theorem dscmet
Dummy variables 𝑣 𝑢 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0re 10635 . . . . . 6 0 ∈ ℝ
2 1re 10633 . . . . . 6 1 ∈ ℝ
31, 2ifcli 4511 . . . . 5 if(𝑥 = 𝑦, 0, 1) ∈ ℝ
43rgen2w 3149 . . . 4 𝑥𝑋𝑦𝑋 if(𝑥 = 𝑦, 0, 1) ∈ ℝ
5 dscmet.1 . . . . 5 𝐷 = (𝑥𝑋, 𝑦𝑋 ↦ if(𝑥 = 𝑦, 0, 1))
65fmpo 7758 . . . 4 (∀𝑥𝑋𝑦𝑋 if(𝑥 = 𝑦, 0, 1) ∈ ℝ ↔ 𝐷:(𝑋 × 𝑋)⟶ℝ)
74, 6mpbi 232 . . 3 𝐷:(𝑋 × 𝑋)⟶ℝ
8 equequ1 2025 . . . . . . . . 9 (𝑥 = 𝑤 → (𝑥 = 𝑦𝑤 = 𝑦))
98ifbid 4487 . . . . . . . 8 (𝑥 = 𝑤 → if(𝑥 = 𝑦, 0, 1) = if(𝑤 = 𝑦, 0, 1))
10 equequ2 2026 . . . . . . . . 9 (𝑦 = 𝑣 → (𝑤 = 𝑦𝑤 = 𝑣))
1110ifbid 4487 . . . . . . . 8 (𝑦 = 𝑣 → if(𝑤 = 𝑦, 0, 1) = if(𝑤 = 𝑣, 0, 1))
12 0nn0 11904 . . . . . . . . . 10 0 ∈ ℕ0
13 1nn0 11905 . . . . . . . . . 10 1 ∈ ℕ0
1412, 13ifcli 4511 . . . . . . . . 9 if(𝑤 = 𝑣, 0, 1) ∈ ℕ0
1514elexi 3512 . . . . . . . 8 if(𝑤 = 𝑣, 0, 1) ∈ V
169, 11, 5, 15ovmpo 7302 . . . . . . 7 ((𝑤𝑋𝑣𝑋) → (𝑤𝐷𝑣) = if(𝑤 = 𝑣, 0, 1))
1716eqeq1d 2821 . . . . . 6 ((𝑤𝑋𝑣𝑋) → ((𝑤𝐷𝑣) = 0 ↔ if(𝑤 = 𝑣, 0, 1) = 0))
18 iffalse 4474 . . . . . . . . . 10 𝑤 = 𝑣 → if(𝑤 = 𝑣, 0, 1) = 1)
19 ax-1ne0 10598 . . . . . . . . . . 11 1 ≠ 0
2019a1i 11 . . . . . . . . . 10 𝑤 = 𝑣 → 1 ≠ 0)
2118, 20eqnetrd 3081 . . . . . . . . 9 𝑤 = 𝑣 → if(𝑤 = 𝑣, 0, 1) ≠ 0)
2221neneqd 3019 . . . . . . . 8 𝑤 = 𝑣 → ¬ if(𝑤 = 𝑣, 0, 1) = 0)
2322con4i 114 . . . . . . 7 (if(𝑤 = 𝑣, 0, 1) = 0 → 𝑤 = 𝑣)
24 iftrue 4471 . . . . . . 7 (𝑤 = 𝑣 → if(𝑤 = 𝑣, 0, 1) = 0)
2523, 24impbii 211 . . . . . 6 (if(𝑤 = 𝑣, 0, 1) = 0 ↔ 𝑤 = 𝑣)
2617, 25syl6bb 289 . . . . 5 ((𝑤𝑋𝑣𝑋) → ((𝑤𝐷𝑣) = 0 ↔ 𝑤 = 𝑣))
2712, 13ifcli 4511 . . . . . . . . . . 11 if(𝑢 = 𝑤, 0, 1) ∈ ℕ0
2812, 13ifcli 4511 . . . . . . . . . . 11 if(𝑢 = 𝑣, 0, 1) ∈ ℕ0
2927, 28nn0addcli 11926 . . . . . . . . . 10 (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) ∈ ℕ0
30 elnn0 11891 . . . . . . . . . 10 ((if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) ∈ ℕ0 ↔ ((if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) ∈ ℕ ∨ (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) = 0))
3129, 30mpbi 232 . . . . . . . . 9 ((if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) ∈ ℕ ∨ (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) = 0)
32 breq1 5060 . . . . . . . . . . . 12 (0 = if(𝑤 = 𝑣, 0, 1) → (0 ≤ 1 ↔ if(𝑤 = 𝑣, 0, 1) ≤ 1))
33 breq1 5060 . . . . . . . . . . . 12 (1 = if(𝑤 = 𝑣, 0, 1) → (1 ≤ 1 ↔ if(𝑤 = 𝑣, 0, 1) ≤ 1))
34 0le1 11155 . . . . . . . . . . . 12 0 ≤ 1
352leidi 11166 . . . . . . . . . . . 12 1 ≤ 1
3632, 33, 34, 35keephyp 4534 . . . . . . . . . . 11 if(𝑤 = 𝑣, 0, 1) ≤ 1
37 nnge1 11657 . . . . . . . . . . 11 ((if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) ∈ ℕ → 1 ≤ (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)))
3814nn0rei 11900 . . . . . . . . . . . 12 if(𝑤 = 𝑣, 0, 1) ∈ ℝ
3929nn0rei 11900 . . . . . . . . . . . 12 (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) ∈ ℝ
4038, 2, 39letri 10761 . . . . . . . . . . 11 ((if(𝑤 = 𝑣, 0, 1) ≤ 1 ∧ 1 ≤ (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1))) → if(𝑤 = 𝑣, 0, 1) ≤ (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)))
4136, 37, 40sylancr 589 . . . . . . . . . 10 ((if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) ∈ ℕ → if(𝑤 = 𝑣, 0, 1) ≤ (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)))
4227nn0ge0i 11916 . . . . . . . . . . . . 13 0 ≤ if(𝑢 = 𝑤, 0, 1)
4328nn0ge0i 11916 . . . . . . . . . . . . 13 0 ≤ if(𝑢 = 𝑣, 0, 1)
4427nn0rei 11900 . . . . . . . . . . . . . 14 if(𝑢 = 𝑤, 0, 1) ∈ ℝ
4528nn0rei 11900 . . . . . . . . . . . . . 14 if(𝑢 = 𝑣, 0, 1) ∈ ℝ
4644, 45add20i 11175 . . . . . . . . . . . . 13 ((0 ≤ if(𝑢 = 𝑤, 0, 1) ∧ 0 ≤ if(𝑢 = 𝑣, 0, 1)) → ((if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) = 0 ↔ (if(𝑢 = 𝑤, 0, 1) = 0 ∧ if(𝑢 = 𝑣, 0, 1) = 0)))
4742, 43, 46mp2an 690 . . . . . . . . . . . 12 ((if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) = 0 ↔ (if(𝑢 = 𝑤, 0, 1) = 0 ∧ if(𝑢 = 𝑣, 0, 1) = 0))
48 equequ2 2026 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑤 → (𝑢 = 𝑣𝑢 = 𝑤))
4948ifbid 4487 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑤 → if(𝑢 = 𝑣, 0, 1) = if(𝑢 = 𝑤, 0, 1))
5049eqeq1d 2821 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑤 → (if(𝑢 = 𝑣, 0, 1) = 0 ↔ if(𝑢 = 𝑤, 0, 1) = 0))
5150, 48bibi12d 348 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑤 → ((if(𝑢 = 𝑣, 0, 1) = 0 ↔ 𝑢 = 𝑣) ↔ (if(𝑢 = 𝑤, 0, 1) = 0 ↔ 𝑢 = 𝑤)))
52 equequ1 2025 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑢 → (𝑤 = 𝑣𝑢 = 𝑣))
5352ifbid 4487 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑢 → if(𝑤 = 𝑣, 0, 1) = if(𝑢 = 𝑣, 0, 1))
5453eqeq1d 2821 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑢 → (if(𝑤 = 𝑣, 0, 1) = 0 ↔ if(𝑢 = 𝑣, 0, 1) = 0))
5554, 52bibi12d 348 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑢 → ((if(𝑤 = 𝑣, 0, 1) = 0 ↔ 𝑤 = 𝑣) ↔ (if(𝑢 = 𝑣, 0, 1) = 0 ↔ 𝑢 = 𝑣)))
5655, 25chvarvv 1998 . . . . . . . . . . . . . . . 16 (if(𝑢 = 𝑣, 0, 1) = 0 ↔ 𝑢 = 𝑣)
5751, 56chvarvv 1998 . . . . . . . . . . . . . . 15 (if(𝑢 = 𝑤, 0, 1) = 0 ↔ 𝑢 = 𝑤)
58 eqtr2 2840 . . . . . . . . . . . . . . 15 ((𝑢 = 𝑤𝑢 = 𝑣) → 𝑤 = 𝑣)
5957, 56, 58syl2anb 599 . . . . . . . . . . . . . 14 ((if(𝑢 = 𝑤, 0, 1) = 0 ∧ if(𝑢 = 𝑣, 0, 1) = 0) → 𝑤 = 𝑣)
6059iftrued 4473 . . . . . . . . . . . . 13 ((if(𝑢 = 𝑤, 0, 1) = 0 ∧ if(𝑢 = 𝑣, 0, 1) = 0) → if(𝑤 = 𝑣, 0, 1) = 0)
611leidi 11166 . . . . . . . . . . . . 13 0 ≤ 0
6260, 61eqbrtrdi 5096 . . . . . . . . . . . 12 ((if(𝑢 = 𝑤, 0, 1) = 0 ∧ if(𝑢 = 𝑣, 0, 1) = 0) → if(𝑤 = 𝑣, 0, 1) ≤ 0)
6347, 62sylbi 219 . . . . . . . . . . 11 ((if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) = 0 → if(𝑤 = 𝑣, 0, 1) ≤ 0)
64 id 22 . . . . . . . . . . 11 ((if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) = 0 → (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) = 0)
6563, 64breqtrrd 5085 . . . . . . . . . 10 ((if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) = 0 → if(𝑤 = 𝑣, 0, 1) ≤ (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)))
6641, 65jaoi 853 . . . . . . . . 9 (((if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) ∈ ℕ ∨ (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) = 0) → if(𝑤 = 𝑣, 0, 1) ≤ (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)))
6731, 66mp1i 13 . . . . . . . 8 ((𝑢𝑋 ∧ (𝑤𝑋𝑣𝑋)) → if(𝑤 = 𝑣, 0, 1) ≤ (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)))
6816adantl 484 . . . . . . . 8 ((𝑢𝑋 ∧ (𝑤𝑋𝑣𝑋)) → (𝑤𝐷𝑣) = if(𝑤 = 𝑣, 0, 1))
69 eqeq12 2833 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑤) → (𝑥 = 𝑦𝑢 = 𝑤))
7069ifbid 4487 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑤) → if(𝑥 = 𝑦, 0, 1) = if(𝑢 = 𝑤, 0, 1))
7127elexi 3512 . . . . . . . . . . 11 if(𝑢 = 𝑤, 0, 1) ∈ V
7270, 5, 71ovmpoa 7297 . . . . . . . . . 10 ((𝑢𝑋𝑤𝑋) → (𝑢𝐷𝑤) = if(𝑢 = 𝑤, 0, 1))
7372adantrr 715 . . . . . . . . 9 ((𝑢𝑋 ∧ (𝑤𝑋𝑣𝑋)) → (𝑢𝐷𝑤) = if(𝑢 = 𝑤, 0, 1))
74 eqeq12 2833 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑥 = 𝑦𝑢 = 𝑣))
7574ifbid 4487 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑣) → if(𝑥 = 𝑦, 0, 1) = if(𝑢 = 𝑣, 0, 1))
7628elexi 3512 . . . . . . . . . . 11 if(𝑢 = 𝑣, 0, 1) ∈ V
7775, 5, 76ovmpoa 7297 . . . . . . . . . 10 ((𝑢𝑋𝑣𝑋) → (𝑢𝐷𝑣) = if(𝑢 = 𝑣, 0, 1))
7877adantrl 714 . . . . . . . . 9 ((𝑢𝑋 ∧ (𝑤𝑋𝑣𝑋)) → (𝑢𝐷𝑣) = if(𝑢 = 𝑣, 0, 1))
7973, 78oveq12d 7166 . . . . . . . 8 ((𝑢𝑋 ∧ (𝑤𝑋𝑣𝑋)) → ((𝑢𝐷𝑤) + (𝑢𝐷𝑣)) = (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)))
8067, 68, 793brtr4d 5089 . . . . . . 7 ((𝑢𝑋 ∧ (𝑤𝑋𝑣𝑋)) → (𝑤𝐷𝑣) ≤ ((𝑢𝐷𝑤) + (𝑢𝐷𝑣)))
8180expcom 416 . . . . . 6 ((𝑤𝑋𝑣𝑋) → (𝑢𝑋 → (𝑤𝐷𝑣) ≤ ((𝑢𝐷𝑤) + (𝑢𝐷𝑣))))
8281ralrimiv 3179 . . . . 5 ((𝑤𝑋𝑣𝑋) → ∀𝑢𝑋 (𝑤𝐷𝑣) ≤ ((𝑢𝐷𝑤) + (𝑢𝐷𝑣)))
8326, 82jca 514 . . . 4 ((𝑤𝑋𝑣𝑋) → (((𝑤𝐷𝑣) = 0 ↔ 𝑤 = 𝑣) ∧ ∀𝑢𝑋 (𝑤𝐷𝑣) ≤ ((𝑢𝐷𝑤) + (𝑢𝐷𝑣))))
8483rgen2 3201 . . 3 𝑤𝑋𝑣𝑋 (((𝑤𝐷𝑣) = 0 ↔ 𝑤 = 𝑣) ∧ ∀𝑢𝑋 (𝑤𝐷𝑣) ≤ ((𝑢𝐷𝑤) + (𝑢𝐷𝑣)))
857, 84pm3.2i 473 . 2 (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑤𝑋𝑣𝑋 (((𝑤𝐷𝑣) = 0 ↔ 𝑤 = 𝑣) ∧ ∀𝑢𝑋 (𝑤𝐷𝑣) ≤ ((𝑢𝐷𝑤) + (𝑢𝐷𝑣))))
86 ismet 22925 . 2 (𝑋𝑉 → (𝐷 ∈ (Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑤𝑋𝑣𝑋 (((𝑤𝐷𝑣) = 0 ↔ 𝑤 = 𝑣) ∧ ∀𝑢𝑋 (𝑤𝐷𝑣) ≤ ((𝑢𝐷𝑤) + (𝑢𝐷𝑣))))))
8785, 86mpbiri 260 1 (𝑋𝑉𝐷 ∈ (Met‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wo 843   = wceq 1530  wcel 2107  wne 3014  wral 3136  ifcif 4465   class class class wbr 5057   × cxp 5546  wf 6344  cfv 6348  (class class class)co 7148  cmpo 7150  cr 10528  0cc0 10529  1c1 10530   + caddc 10532  cle 10668  cn 11630  0cn0 11889  Metcmet 20523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7573  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-er 8281  df-map 8400  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-nn 11631  df-n0 11890  df-met 20531
This theorem is referenced by:  dscopn  23175
  Copyright terms: Public domain W3C validator