Metamath Proof Explorer

Theorem xmettri2

Description: Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmettri2 ⊢ D ∈ ∞Met ⁡ X ∧ C ∈ X ∧ A ∈ X ∧ B ∈ X → A D B ≤ C D A + 𝑒 C D 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 simpr ⊢ x D y = 0 ↔ x = y ∧ ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y → ∀ z ∈ X x D y ≤ z D x + 𝑒 z D 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 ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
7 4 6 simpl2im ⊢ D ∈ ∞Met ⁡ X → ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
8 oveq1 ⊢ x = A → x D y = A D y
9 oveq2 ⊢ x = A → z D x = z D A
10 9 oveq1d ⊢ x = A → z D x + 𝑒 z D y = z D A + 𝑒 z D y
11 8 10 breq12d ⊢ x = A → x D y ≤ z D x + 𝑒 z D y ↔ A D y ≤ z D A + 𝑒 z D y
12 oveq2 ⊢ y = B → A D y = A D B
13 oveq2 ⊢ y = B → z D y = z D B
14 13 oveq2d ⊢ y = B → z D A + 𝑒 z D y = z D A + 𝑒 z D B
15 12 14 breq12d ⊢ y = B → A D y ≤ z D A + 𝑒 z D y ↔ A D B ≤ z D A + 𝑒 z D B
16 oveq1 ⊢ z = C → z D A = C D A
17 oveq1 ⊢ z = C → z D B = C D B
18 16 17 oveq12d ⊢ z = C → z D A + 𝑒 z D B = C D A + 𝑒 C D B
19 18 breq2d ⊢ z = C → A D B ≤ z D A + 𝑒 z D B ↔ A D B ≤ C D A + 𝑒 C D B
20 11 15 19 rspc3v ⊢ A ∈ X ∧ B ∈ X ∧ C ∈ X → ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y → A D B ≤ C D A + 𝑒 C D B
21 7 20 syl5 ⊢ A ∈ X ∧ B ∈ X ∧ C ∈ X → D ∈ ∞Met ⁡ X → A D B ≤ C D A + 𝑒 C D B
22 21 3comr ⊢ C ∈ X ∧ A ∈ X ∧ B ∈ X → D ∈ ∞Met ⁡ X → A D B ≤ C D A + 𝑒 C D B
23 22 impcom ⊢ D ∈ ∞Met ⁡ X ∧ C ∈ X ∧ A ∈ X ∧ B ∈ X → A D B ≤ C D A + 𝑒 C D B