Metamath Proof Explorer


Theorem xmsxmet

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

Ref Expression
Hypotheses msf.x
|- X = ( Base ` M )
msf.d
|- D = ( ( dist ` M ) |` ( X X. X ) )
Assertion xmsxmet
|- ( M e. *MetSp -> D e. ( *Met ` X ) )

Proof

Step Hyp Ref Expression
1 msf.x
 |-  X = ( Base ` M )
2 msf.d
 |-  D = ( ( dist ` M ) |` ( X X. X ) )
3 eqid
 |-  ( TopOpen ` M ) = ( TopOpen ` M )
4 3 1 2 isxms2
 |-  ( M e. *MetSp <-> ( D e. ( *Met ` X ) /\ ( TopOpen ` M ) = ( MetOpen ` D ) ) )
5 4 simplbi
 |-  ( M e. *MetSp -> D e. ( *Met ` X ) )