This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xmeteq0

Description: The value of an extended metric is zero iff its arguments are equal. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmeteq0 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B = 0 ↔ A = B

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ D ∈ ∞Met ⁡ X → X ∈ dom ⁡ ∞Met
2 isxmet ⊢ X ∈ dom ⁡ ∞Met → D ∈ ∞Met ⁡ X ↔ D : X × X ⟶ ℝ * ∧ ∀ x ∈ X ∀ y ∈ X x D y = 0 ↔ x = y ∧ ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
3 1 2 syl ⊢ D ∈ ∞Met ⁡ X → D ∈ ∞Met ⁡ X ↔ D : X × X ⟶ ℝ * ∧ ∀ x ∈ X ∀ y ∈ X x D y = 0 ↔ x = y ∧ ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
4 3 ibi ⊢ D ∈ ∞Met ⁡ X → D : X × X ⟶ ℝ * ∧ ∀ x ∈ X ∀ y ∈ X x D y = 0 ↔ x = y ∧ ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
5 simpl ⊢ x D y = 0 ↔ x = y ∧ ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y → x D y = 0 ↔ x = y
6 5 2ralimi ⊢ ∀ x ∈ X ∀ y ∈ X x D y = 0 ↔ x = y ∧ ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y → ∀ x ∈ X ∀ y ∈ X x D y = 0 ↔ x = y
7 4 6 simpl2im ⊢ D ∈ ∞Met ⁡ X → ∀ x ∈ X ∀ y ∈ X x D y = 0 ↔ x = y
8 oveq1 ⊢ x = A → x D y = A D y
9 8 eqeq1d ⊢ x = A → x D y = 0 ↔ A D y = 0
10 eqeq1 ⊢ x = A → x = y ↔ A = y
11 9 10 bibi12d ⊢ x = A → x D y = 0 ↔ x = y ↔ A D y = 0 ↔ A = y
12 oveq2 ⊢ y = B → A D y = A D B
13 12 eqeq1d ⊢ y = B → A D y = 0 ↔ A D B = 0
14 eqeq2 ⊢ y = B → A = y ↔ A = B
15 13 14 bibi12d ⊢ y = B → A D y = 0 ↔ A = y ↔ A D B = 0 ↔ A = B
16 11 15 rspc2v ⊢ A ∈ X ∧ B ∈ X → ∀ x ∈ X ∀ y ∈ X x D y = 0 ↔ x = y → A D B = 0 ↔ A = B
17 7 16 syl5com ⊢ D ∈ ∞Met ⁡ X → A ∈ X ∧ B ∈ X → A D B = 0 ↔ A = B
18 17 3impib ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B = 0 ↔ A = B