Metamath Proof Explorer

Theorem psmettri

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

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

Proof

Step Hyp Ref Expression
1 simpl ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → D ∈ PsMet ⁡ X
2 simpr3 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → C ∈ X
3 simpr1 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A ∈ X
4 simpr2 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B ∈ X
5 psmettri2 ⊢ D ∈ PsMet ⁡ X ∧ C ∈ X ∧ A ∈ X ∧ B ∈ X → A D B ≤ C D A + 𝑒 C D B
6 1 2 3 4 5 syl13anc ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B ≤ C D A + 𝑒 C D B
7 psmetsym ⊢ D ∈ PsMet ⁡ X ∧ C ∈ X ∧ A ∈ X → C D A = A D C
8 1 2 3 7 syl3anc ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → C D A = A D C
9 8 oveq1d ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → C D A + 𝑒 C D B = A D C + 𝑒 C D B
10 6 9 breqtrd ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B ≤ A D C + 𝑒 C D B