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

Metamath Proof Explorer

Theorem isxmetd

Description: Properties that determine an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015) (Revised by AV, 9-Apr-2024)

Ref Expression
Hypotheses isxmetd.0 ⊢ φ → X ∈ V
isxmetd.1 ⊢ φ → D : X × X ⟶ ℝ *
isxmetd.2 ⊢ φ ∧ x ∈ X ∧ y ∈ X → x D y = 0 ↔ x = y
isxmetd.3 ⊢ φ ∧ x ∈ X ∧ y ∈ X ∧ z ∈ X → x D y ≤ z D x + 𝑒 z D y
Assertion isxmetd ⊢ φ → D ∈ ∞Met ⁡ X

Proof

Step Hyp Ref Expression
1 isxmetd.0 ⊢ φ → X ∈ V
2 isxmetd.1 ⊢ φ → D : X × X ⟶ ℝ *
3 isxmetd.2 ⊢ φ ∧ x ∈ X ∧ y ∈ X → x D y = 0 ↔ x = y
4 isxmetd.3 ⊢ φ ∧ x ∈ X ∧ y ∈ X ∧ z ∈ X → x D y ≤ z D x + 𝑒 z D y
5 4 3exp2 ⊢ φ → x ∈ X → y ∈ X → z ∈ X → x D y ≤ z D x + 𝑒 z D y
6 5 imp32 ⊢ φ ∧ x ∈ X ∧ y ∈ X → z ∈ X → x D y ≤ z D x + 𝑒 z D y
7 6 ralrimiv ⊢ φ ∧ x ∈ X ∧ y ∈ X → ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
8 3 7 jca ⊢ φ ∧ x ∈ X ∧ y ∈ X → x D y = 0 ↔ x = y ∧ ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
9 8 ralrimivva ⊢ φ → ∀ x ∈ X ∀ y ∈ X x D y = 0 ↔ x = y ∧ ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
10 isxmet ⊢ X ∈ V → 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
11 1 10 syl ⊢ φ → 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
12 2 9 11 mpbir2and ⊢ φ → D ∈ ∞Met ⁡ X