Metamath Proof Explorer

Theorem xmetpsmet

Description: An extended metric is a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Assertion xmetpsmet ⊢ D ∈ ∞Met ⁡ X → D ∈ PsMet ⁡ X

Proof

Step Hyp Ref Expression
1 xmetf ⊢ D ∈ ∞Met ⁡ X → D : X × X ⟶ ℝ *
2 xmet0 ⊢ D ∈ ∞Met ⁡ X ∧ x ∈ X → x D x = 0
3 3anrot ⊢ z ∈ X ∧ x ∈ X ∧ y ∈ X ↔ x ∈ X ∧ y ∈ X ∧ z ∈ X
4 xmettri2 ⊢ D ∈ ∞Met ⁡ X ∧ z ∈ X ∧ x ∈ X ∧ y ∈ X → x D y ≤ z D x + 𝑒 z D y
5 3 4 sylan2br ⊢ D ∈ ∞Met ⁡ X ∧ x ∈ X ∧ y ∈ X ∧ z ∈ X → x D y ≤ z D x + 𝑒 z D y
6 5 3anassrs ⊢ D ∈ ∞Met ⁡ X ∧ x ∈ X ∧ y ∈ X ∧ z ∈ X → x D y ≤ z D x + 𝑒 z D y
7 6 ralrimiva ⊢ D ∈ ∞Met ⁡ X ∧ x ∈ X ∧ y ∈ X → ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
8 7 ralrimiva ⊢ D ∈ ∞Met ⁡ X ∧ x ∈ X → ∀ y ∈ X ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
9 2 8 jca ⊢ D ∈ ∞Met ⁡ X ∧ x ∈ X → x D x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
10 9 ralrimiva ⊢ D ∈ ∞Met ⁡ X → ∀ x ∈ X x D x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
11 elfvex ⊢ D ∈ ∞Met ⁡ X → X ∈ V
12 ispsmet ⊢ X ∈ V → D ∈ PsMet ⁡ X ↔ D : X × X ⟶ ℝ * ∧ ∀ x ∈ X x D x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
13 11 12 syl ⊢ D ∈ ∞Met ⁡ X → D ∈ PsMet ⁡ X ↔ D : X × X ⟶ ℝ * ∧ ∀ x ∈ X x D x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
14 1 10 13 mpbir2and ⊢ D ∈ ∞Met ⁡ X → D ∈ PsMet ⁡ X