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 ) ) |
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 ) ) |