Metamath Proof Explorer

Theorem met0

Description: The distance function of a metric space is zero if its arguments are equal. Definition 14-1.1(a) of Gleason p. 223. (Contributed by NM, 30-Aug-2006)

		Ref	Expression
	Assertion	met0	$⊢ (D \in Met (X) \land A \in X) \to A D A = 0$

Proof

Step	Hyp	Ref	Expression
1		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
2		xmet0	$⊢ (D \in ∞Met (X) \land A \in X) \to A D A = 0$
3	1 2	sylan	$⊢ (D \in Met (X) \land A \in X) \to A D A = 0$