# 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 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{D}{B}={B}{D}{A}$

### Proof

Step Hyp Ref Expression
1 xmetcl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{D}{B}\in {ℝ}^{*}$
2 xmetcl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {B}\in {X}\wedge {A}\in {X}\right)\to {B}{D}{A}\in {ℝ}^{*}$
3 2 3com23 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {B}{D}{A}\in {ℝ}^{*}$
4 simp1 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
5 simp3 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {B}\in {X}$
6 simp2 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}\in {X}$
7 xmettri2 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({B}\in {X}\wedge {A}\in {X}\wedge {B}\in {X}\right)\right)\to {A}{D}{B}\le \left({B}{D}{A}\right){+}_{𝑒}\left({B}{D}{B}\right)$
8 4 5 6 5 7 syl13anc ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{D}{B}\le \left({B}{D}{A}\right){+}_{𝑒}\left({B}{D}{B}\right)$
9 xmet0 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {B}\in {X}\right)\to {B}{D}{B}=0$
10 9 3adant2 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {B}{D}{B}=0$
11 10 oveq2d ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \left({B}{D}{A}\right){+}_{𝑒}\left({B}{D}{B}\right)=\left({B}{D}{A}\right){+}_{𝑒}0$
12 2 xaddid1d ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {B}\in {X}\wedge {A}\in {X}\right)\to \left({B}{D}{A}\right){+}_{𝑒}0={B}{D}{A}$
13 12 3com23 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \left({B}{D}{A}\right){+}_{𝑒}0={B}{D}{A}$
14 11 13 eqtrd ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \left({B}{D}{A}\right){+}_{𝑒}\left({B}{D}{B}\right)={B}{D}{A}$
15 8 14 breqtrd ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{D}{B}\le {B}{D}{A}$
16 xmettri2 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {A}\in {X}\right)\right)\to {B}{D}{A}\le \left({A}{D}{B}\right){+}_{𝑒}\left({A}{D}{A}\right)$
17 4 6 5 6 16 syl13anc ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {B}{D}{A}\le \left({A}{D}{B}\right){+}_{𝑒}\left({A}{D}{A}\right)$
18 xmet0 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\right)\to {A}{D}{A}=0$
19 18 3adant3 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{D}{A}=0$
20 19 oveq2d ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \left({A}{D}{B}\right){+}_{𝑒}\left({A}{D}{A}\right)=\left({A}{D}{B}\right){+}_{𝑒}0$
21 1 xaddid1d ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \left({A}{D}{B}\right){+}_{𝑒}0={A}{D}{B}$
22 20 21 eqtrd ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \left({A}{D}{B}\right){+}_{𝑒}\left({A}{D}{A}\right)={A}{D}{B}$
23 17 22 breqtrd ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {B}{D}{A}\le {A}{D}{B}$
24 1 3 15 23 xrletrid ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{D}{B}={B}{D}{A}$