Metamath Proof Explorer


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=BaseM
mscl.d D=distM
Assertion msmet2 MMetSpDX×XMetX

Proof

Step Hyp Ref Expression
1 mscl.x X=BaseM
2 mscl.d D=distM
3 2 reseq1i DX×X=distMX×X
4 1 3 msmet MMetSpDX×XMetX