Metamath Proof Explorer

Theorem tmsms

Description: The constructed metric space is a metric space given a metric. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypothesis tmsbas.k 
|- K = ( toMetSp ` D )
Assertion tmsms 
|- ( D e. ( Met ` X ) -> K e. MetSp )

Proof

Step Hyp Ref Expression
1 tmsbas.k 
 |-  K = ( toMetSp ` D )
2 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
3 1 tmsxms 
 |-  ( D e. ( *Met ` X ) -> K e. *MetSp )
4 2 3 syl 
 |-  ( D e. ( Met ` X ) -> K e. *MetSp )
5 1 tmsds 
 |-  ( D e. ( *Met ` X ) -> D = ( dist ` K ) )
6 2 5 syl 
 |-  ( D e. ( Met ` X ) -> D = ( dist ` K ) )
7 1 tmsbas 
 |-  ( D e. ( *Met ` X ) -> X = ( Base ` K ) )
8 2 7 syl 
 |-  ( D e. ( Met ` X ) -> X = ( Base ` K ) )
9 8 fveq2d 
 |-  ( D e. ( Met ` X ) -> ( Met ` X ) = ( Met ` ( Base ` K ) ) )
10 6 9 eleq12d 
 |-  ( D e. ( Met ` X ) -> ( D e. ( Met ` X ) <-> ( dist ` K ) e. ( Met ` ( Base ` K ) ) ) )
11 10 ibi 
 |-  ( D e. ( Met ` X ) -> ( dist ` K ) e. ( Met ` ( Base ` K ) ) )
12 ssid 
 |-  ( Base ` K ) C_ ( Base ` K )
13 metres2 
 |-  ( ( ( dist ` K ) e. ( Met ` ( Base ` K ) ) /\ ( Base ` K ) C_ ( Base ` K ) ) -> ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( Met ` ( Base ` K ) ) )
14 11 12 13 sylancl 
 |-  ( D e. ( Met ` X ) -> ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( Met ` ( Base ` K ) ) )
15 eqid 
 |-  ( TopOpen ` K ) = ( TopOpen ` K )
16 eqid 
 |-  ( Base ` K ) = ( Base ` K )
17 eqid 
 |-  ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) )
18 15 16 17 isms 
 |-  ( K e. MetSp <-> ( K e. *MetSp /\ ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( Met ` ( Base ` K ) ) ) )
19 4 14 18 sylanbrc 
 |-  ( D e. ( Met ` X ) -> K e. MetSp )