xmscl

Description: Closure of the distance function of an extended metric space. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	mscl.x	$⊢ X = {Base}_{M}$
	mscl.d	$⊢ D = dist (M)$
Assertion	xmscl	$⊢ (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	xmsxmet2	$⊢ M \in ∞MetSp \to {D ↾}_{(X \times X)} \in ∞Met (X)$
6		xmetcl	$⊢ ({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