xmetsym

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

		Ref	Expression
	Assertion	xmetsym	$⊢ (D \in ∞Met (X) \land A \in X \land B \in X) \to A D B = B D A$

Proof

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

Metamath Proof Explorer

Theorem xmetsym

Proof