Metamath Proof Explorer

Theorem psmettri2

Description: Triangle inequality for the distance function of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Assertion psmettri2 ⊢ D ∈ PsMet ⁡ X ∧ C ∈ X ∧ A ∈ X ∧ B ∈ X → A D B ≤ C D A + 𝑒 C D B

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 simprd ⊢ D ∈ PsMet ⁡ X ∧ a ∈ X → ∀ b ∈ X ∀ c ∈ X a D b ≤ c D a + 𝑒 c D b
8 7 ralrimiva ⊢ D ∈ PsMet ⁡ X → ∀ a ∈ X ∀ b ∈ X ∀ c ∈ X a D b ≤ c D a + 𝑒 c D b
9 oveq1 ⊢ a = A → a D b = A D b
10 oveq2 ⊢ a = A → c D a = c D A
11 10 oveq1d ⊢ a = A → c D a + 𝑒 c D b = c D A + 𝑒 c D b
12 9 11 breq12d ⊢ a = A → a D b ≤ c D a + 𝑒 c D b ↔ A D b ≤ c D A + 𝑒 c D b
13 oveq2 ⊢ b = B → A D b = A D B
14 oveq2 ⊢ b = B → c D b = c D B
15 14 oveq2d ⊢ b = B → c D A + 𝑒 c D b = c D A + 𝑒 c D B
16 13 15 breq12d ⊢ b = B → A D b ≤ c D A + 𝑒 c D b ↔ A D B ≤ c D A + 𝑒 c D B
17 oveq1 ⊢ c = C → c D A = C D A
18 oveq1 ⊢ c = C → c D B = C D B
19 17 18 oveq12d ⊢ c = C → c D A + 𝑒 c D B = C D A + 𝑒 C D B
20 19 breq2d ⊢ c = C → A D B ≤ c D A + 𝑒 c D B ↔ A D B ≤ C D A + 𝑒 C D B
21 12 16 20 rspc3v ⊢ A ∈ X ∧ B ∈ X ∧ C ∈ X → ∀ a ∈ X ∀ b ∈ X ∀ c ∈ X a D b ≤ c D a + 𝑒 c D b → A D B ≤ C D A + 𝑒 C D B
22 21 3comr ⊢ C ∈ X ∧ A ∈ X ∧ B ∈ X → ∀ a ∈ X ∀ b ∈ X ∀ c ∈ X a D b ≤ c D a + 𝑒 c D b → A D B ≤ C D A + 𝑒 C D B
23 8 22 mpan9 ⊢ D ∈ PsMet ⁡ X ∧ C ∈ X ∧ A ∈ X ∧ B ∈ X → A D B ≤ C D A + 𝑒 C D B