Metamath Proof Explorer

Theorem psmetsym

Description: The distance function of a pseudometric is symmetrical. (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Assertion psmetsym ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B = B D A

Proof

Step Hyp Ref Expression
1 psmetcl ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B ∈ ℝ *
2 psmetcl ⊢ D ∈ PsMet ⁡ X ∧ B ∈ X ∧ A ∈ X → B D A ∈ ℝ *
3 2 3com23 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → B D A ∈ ℝ *
4 simp1 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → D ∈ PsMet ⁡ X
5 simp3 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → B ∈ X
6 simp2 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → A ∈ X
7 psmettri2 ⊢ D ∈ PsMet ⁡ X ∧ B ∈ X ∧ A ∈ X ∧ B ∈ X → A D B ≤ B D A + 𝑒 B D B
8 4 5 6 5 7 syl13anc ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B ≤ B D A + 𝑒 B D B
9 psmet0 ⊢ D ∈ PsMet ⁡ X ∧ B ∈ X → B D B = 0
10 9 3adant2 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → B D B = 0
11 10 oveq2d ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → B D A + 𝑒 B D B = B D A + 𝑒 0
12 2 xaddid1d ⊢ D ∈ PsMet ⁡ X ∧ B ∈ X ∧ A ∈ X → B D A + 𝑒 0 = B D A
13 12 3com23 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → B D A + 𝑒 0 = B D A
14 11 13 eqtrd ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → B D A + 𝑒 B D B = B D A
15 8 14 breqtrd ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B ≤ B D A
16 psmettri2 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ A ∈ X → B D A ≤ A D B + 𝑒 A D A
17 4 6 5 6 16 syl13anc ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → B D A ≤ A D B + 𝑒 A D A
18 psmet0 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X → A D A = 0
19 18 3adant3 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → A D A = 0
20 19 oveq2d ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B + 𝑒 A D A = A D B + 𝑒 0
21 1 xaddid1d ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B + 𝑒 0 = A D B
22 20 21 eqtrd ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B + 𝑒 A D A = A D B
23 17 22 breqtrd ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → B D A ≤ A D B
24 1 3 15 23 xrletrid ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B = B D A