Metamath Proof Explorer

Theorem xmseq0

Description: The distance between two points in an extended metric space is zero iff the two points are identical. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses mscl.x ⊢ X = Base M
mscl.d ⊢ D = dist ⁡ M
Assertion xmseq0 ⊢ M ∈ ∞MetSp ∧ A ∈ X ∧ B ∈ X → A D B = 0 ↔ A = B

Proof

Step Hyp Ref Expression
1 mscl.x ⊢ X = Base M
2 mscl.d ⊢ D = dist ⁡ M
3 ovres ⊢ A ∈ X ∧ B ∈ X → A D ↾ X × X B = A D B
4 3 3adant1 ⊢ M ∈ ∞MetSp ∧ A ∈ X ∧ B ∈ X → A D ↾ X × X B = A D B
5 4 eqeq1d ⊢ M ∈ ∞MetSp ∧ A ∈ X ∧ B ∈ X → A D ↾ X × X B = 0 ↔ A D B = 0
6 1 2 xmsxmet2 ⊢ M ∈ ∞MetSp → D ↾ X × X ∈ ∞Met ⁡ X
7 xmeteq0 ⊢ D ↾ X × X ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → A D ↾ X × X B = 0 ↔ A = B
8 6 7 syl3an1 ⊢ M ∈ ∞MetSp ∧ A ∈ X ∧ B ∈ X → A D ↾ X × X B = 0 ↔ A = B
9 5 8 bitr3d ⊢ M ∈ ∞MetSp ∧ A ∈ X ∧ B ∈ X → A D B = 0 ↔ A = B