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

Metamath Proof Explorer

Theorem psmet0

Description: The distance function of a pseudometric space is zero if its arguments are equal. (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Assertion psmet0 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X → A D A = 0

Proof

Step Hyp Ref Expression
1 elfvex ⊢ D ∈ PsMet ⁡ X → X ∈ V
2 ispsmet ⊢ X ∈ V → D ∈ PsMet ⁡ X ↔ D : X × X ⟶ ℝ * ∧ ∀ a ∈ X a D a = 0 ∧ ∀ b ∈ X ∀ c ∈ X a D b ≤ c D a + 𝑒 c D b
3 1 2 syl ⊢ D ∈ PsMet ⁡ X → D ∈ PsMet ⁡ X ↔ D : X × X ⟶ ℝ * ∧ ∀ a ∈ X a D a = 0 ∧ ∀ b ∈ X ∀ c ∈ X a D b ≤ c D a + 𝑒 c D b
4 3 ibi ⊢ D ∈ PsMet ⁡ X → D : X × X ⟶ ℝ * ∧ ∀ a ∈ X a D a = 0 ∧ ∀ b ∈ X ∀ c ∈ X a D b ≤ c D a + 𝑒 c D b
5 4 simprd ⊢ D ∈ PsMet ⁡ X → ∀ a ∈ X a D a = 0 ∧ ∀ b ∈ X ∀ c ∈ X a D b ≤ c D a + 𝑒 c D b
6 5 r19.21bi ⊢ D ∈ PsMet ⁡ X ∧ a ∈ X → a D a = 0 ∧ ∀ b ∈ X ∀ c ∈ X a D b ≤ c D a + 𝑒 c D b
7 6 simpld ⊢ D ∈ PsMet ⁡ X ∧ a ∈ X → a D a = 0
8 7 ralrimiva ⊢ D ∈ PsMet ⁡ X → ∀ a ∈ X a D a = 0
9 id ⊢ a = A → a = A
10 9 9 oveq12d ⊢ a = A → a D a = A D A
11 10 eqeq1d ⊢ a = A → a D a = 0 ↔ A D A = 0
12 11 rspcv ⊢ A ∈ X → ∀ a ∈ X a D a = 0 → A D A = 0
13 8 12 mpan9 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X → A D A = 0