Theorem 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={\mathrm{Base}}_M$$
	mscl.d	$$⊢D=\mathrm{dist}\left(M\right)$$
Assertion	mscl	$$⊢\left(M\in \mathrm{MetSp}\wedge A\in X\wedge B\in X\right)\to ADB\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		mscl.x	$$⊢X={\mathrm{Base}}_M$$
2		mscl.d	$$⊢D=\mathrm{dist}\left(M\right)$$
3		ovres	$$⊢\left(A\in X\wedge B\in X\right)\to A\left({D\upharpoonright }_{\left(X\times X\right)}\right)B=ADB$$
4	3	3adant1	$$⊢\left(M\in \mathrm{MetSp}\wedge A\in X\wedge B\in X\right)\to A\left({D\upharpoonright }_{\left(X\times X\right)}\right)B=ADB$$
5	1 2	msmet2	$$⊢M\in \mathrm{MetSp}\to {D\upharpoonright }_{\left(X\times X\right)}\in \mathrm{Met}\left(X\right)$$
6		metcl	$$⊢\left({D\upharpoonright }_{\left(X\times X\right)}\in \mathrm{Met}\left(X\right)\wedge A\in X\wedge B\in X\right)\to A\left({D\upharpoonright }_{\left(X\times X\right)}\right)B\in ℝ$$
7	5 6	syl3an1	$$⊢\left(M\in \mathrm{MetSp}\wedge A\in X\wedge B\in X\right)\to A\left({D\upharpoonright }_{\left(X\times X\right)}\right)B\in ℝ$$
8	4 7	eqeltrrd	$$⊢\left(M\in \mathrm{MetSp}\wedge A\in X\wedge B\in X\right)\to ADB\in ℝ$$