Theorem xmsxmet2

Description: The distance function, suitably truncated, is an extended 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	xmsxmet2	$$⊢M\in \mathrm{\infty MetSp}\to {D\upharpoonright }_{\left(X\times X\right)}\in \mathrm{\infty 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	xmsxmet	$$⊢M\in \mathrm{\infty MetSp}\to {D\upharpoonright }_{\left(X\times X\right)}\in \mathrm{\infty Met}\left(X\right)$$