Metamath Proof Explorer

Theorem xmssym

Description: The distance function in an extended metric space is symmetric. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses mscl.x ⊢ X = Base M
mscl.d ⊢ D = dist ⁡ M
Assertion xmssym ⊢ M ∈ ∞MetSp ∧ A ∈ X ∧ B ∈ X → A D B = B D A

Proof

Step Hyp Ref Expression
1 mscl.x ⊢ X = Base M
2 mscl.d ⊢ D = dist ⁡ M
3 1 2 xmsxmet2 ⊢ M ∈ ∞MetSp → D ↾ X × X ∈ ∞Met ⁡ X
4 xmetsym ⊢ D ↾ X × X ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → A D ↾ X × X B = B D ↾ X × X A
5 3 4 syl3an1 ⊢ M ∈ ∞MetSp ∧ A ∈ X ∧ B ∈ X → A D ↾ X × X B = B D ↾ X × X A
6 simp2 ⊢ M ∈ ∞MetSp ∧ A ∈ X ∧ B ∈ X → A ∈ X
7 simp3 ⊢ M ∈ ∞MetSp ∧ A ∈ X ∧ B ∈ X → B ∈ X
8 6 7 ovresd ⊢ M ∈ ∞MetSp ∧ A ∈ X ∧ B ∈ X → A D ↾ X × X B = A D B
9 7 6 ovresd ⊢ M ∈ ∞MetSp ∧ A ∈ X ∧ B ∈ X → B D ↾ X × X A = B D A
10 5 8 9 3eqtr3d ⊢ M ∈ ∞MetSp ∧ A ∈ X ∧ B ∈ X → A D B = B D A