mscl

Description: Closure of the distance function of a metric space. (Contributed by NM, 30-Aug-2006) (Revised by Mario Carneiro, 2-Oct-2015)

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

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	1 2	msmet2	$⊢ M \in MetSp \to {D ↾}_{(X \times X)} \in Met (X)$
6		metcl	$⊢ ({D ↾}_{(X \times X)} \in Met (X) \land A \in X \land B \in X) \to A ({D ↾}_{(X \times X)}) B \in ℝ$
7	5 6	syl3an1	$⊢ (M \in MetSp \land A \in X \land B \in X) \to A ({D ↾}_{(X \times X)}) B \in ℝ$
8	4 7	eqeltrrd	$⊢ (M \in MetSp \land A \in X \land B \in X) \to A D B \in ℝ$

Metamath Proof Explorer