This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xmseq0

Description: The distance between two points in an extended metric space is zero iff the two points are identical. (Contributed by Mario Carneiro, 2-Oct-2015)

		Ref	Expression
	Hypotheses	mscl.x	$⊢ X = {Base}_{M}$
		mscl.d	$⊢ D = dist (M)$
	Assertion	xmseq0	$⊢ (M \in ∞MetSp \land A \in X \land B \in X) \to (A D B = 0 \leftrightarrow A = B)$

Proof

Step	Hyp	Ref	Expression
1		mscl.x	$⊢ X = {Base}_{M}$
2		mscl.d	$⊢ D = dist (M)$
3		ovres	$⊢ (A \in X \land B \in X) \to A ({D ↾}_{(X \times X)}) B = A D B$
4	3	3adant1	$⊢ (M \in ∞MetSp \land A \in X \land B \in X) \to A ({D ↾}_{(X \times X)}) B = A D B$
5	4	eqeq1d	$⊢ (M \in ∞MetSp \land A \in X \land B \in X) \to (A ({D ↾}_{(X \times X)}) B = 0 \leftrightarrow A D B = 0)$
6	1 2	xmsxmet2	$⊢ M \in ∞MetSp \to {D ↾}_{(X \times X)} \in ∞Met (X)$
7		xmeteq0	$⊢ ({D ↾}_{(X \times X)} \in ∞Met (X) \land A \in X \land B \in X) \to (A ({D ↾}_{(X \times X)}) B = 0 \leftrightarrow A = B)$
8	6 7	syl3an1	$⊢ (M \in ∞MetSp \land A \in X \land B \in X) \to (A ({D ↾}_{(X \times X)}) B = 0 \leftrightarrow A = B)$
9	5 8	bitr3d	$⊢ (M \in ∞MetSp \land A \in X \land B \in X) \to (A D B = 0 \leftrightarrow A = B)$