Metamath Proof Explorer

Theorem xmetsym

Description: The distance function of an extended metric space is symmetric. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmetsym ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B = B D A

Proof

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