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 \in ∞MetSp \land A \in X \land B \in X) \to A D B = B D A$

Step	Hyp	Ref	Expression
1		mscl.x	$⊢ X = {Base}_{M}$
2		mscl.d	$⊢ D = dist (M)$
3	1 2	xmsxmet2	$⊢ M \in ∞MetSp \to {D ↾}_{(X \times X)} \in ∞Met (X)$
4		xmetsym	$⊢ ({D ↾}_{(X \times X)} \in ∞Met (X) \land A \in X \land B \in X) \to A ({D ↾}_{(X \times X)}) B = B ({D ↾}_{(X \times X)}) A$
5	3 4	syl3an1	$⊢ (M \in ∞MetSp \land A \in X \land B \in X) \to A ({D ↾}_{(X \times X)}) B = B ({D ↾}_{(X \times X)}) A$
6		simp2	$⊢ (M \in ∞MetSp \land A \in X \land B \in X) \to A \in X$
7		simp3	$⊢ (M \in ∞MetSp \land A \in X \land B \in X) \to B \in X$
8	6 7	ovresd	$⊢ (M \in ∞MetSp \land A \in X \land B \in X) \to A ({D ↾}_{(X \times X)}) B = A D B$
9	7 6	ovresd	$⊢ (M \in ∞MetSp \land A \in X \land B \in X) \to B ({D ↾}_{(X \times X)}) A = B D A$
10	5 8 9	3eqtr3d	$⊢ (M \in ∞MetSp \land A \in X \land B \in X) \to A D B = B D A$

Metamath Proof Explorer