Theorem msmet2

Description: The distance function, suitably truncated, is a metric on X . (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	mscl.x	$$⊢X={\mathrm{Base}}_M$$
	mscl.d	$$⊢D=\mathrm{dist}\left(M\right)$$
Assertion	msmet2	$$⊢M\in \mathrm{MetSp}\to {D\upharpoonright }_{\left(X\times X\right)}\in \mathrm{Met}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		mscl.x	$$⊢X={\mathrm{Base}}_M$$
2		mscl.d	$$⊢D=\mathrm{dist}\left(M\right)$$
3	2	reseq1i	$$⊢{D\upharpoonright }_{\left(X\times X\right)}={\mathrm{dist}\left(M\right)\upharpoonright }_{\left(X\times X\right)}$$
4	1 3	msmet	$$⊢M\in \mathrm{MetSp}\to {D\upharpoonright }_{\left(X\times X\right)}\in \mathrm{Met}\left(X\right)$$