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 = ( Base ` M )
mscl.d
|- D = ( dist ` M )
Assertion msmet2
|- ( M e. MetSp -> ( D |` ( X X. X ) ) e. ( Met ` X ) )

Proof

Step Hyp Ref Expression
1 mscl.x
 |-  X = ( Base ` M )
2 mscl.d
 |-  D = ( dist ` M )
3 2 reseq1i
 |-  ( D |` ( X X. X ) ) = ( ( dist ` M ) |` ( X X. X ) )
4 1 3 msmet
 |-  ( M e. MetSp -> ( D |` ( X X. X ) ) e. ( Met ` X ) )