Metamath Proof Explorer

Theorem tmsxms

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

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

Proof

Step Hyp Ref Expression
1 tmsbas.k 
 |-  K = ( toMetSp ` D )
2 1 tmsds 
 |-  ( D e. ( *Met ` X ) -> D = ( dist ` K ) )
3 1 tmsbas 
 |-  ( D e. ( *Met ` X ) -> X = ( Base ` K ) )
4 3 fveq2d 
 |-  ( D e. ( *Met ` X ) -> ( *Met ` X ) = ( *Met ` ( Base ` K ) ) )
5 2 4 eleq12d 
 |-  ( D e. ( *Met ` X ) -> ( D e. ( *Met ` X ) <-> ( dist ` K ) e. ( *Met ` ( Base ` K ) ) ) )
6 5 ibi 
 |-  ( D e. ( *Met ` X ) -> ( dist ` K ) e. ( *Met ` ( Base ` K ) ) )
7 ssid 
 |-  ( Base ` K ) C_ ( Base ` K )
8 xmetres2 
 |-  ( ( ( dist ` K ) e. ( *Met ` ( Base ` K ) ) /\ ( Base ` K ) C_ ( Base ` K ) ) -> ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( *Met ` ( Base ` K ) ) )
9 6 7 8 sylancl 
 |-  ( D e. ( *Met ` X ) -> ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( *Met ` ( Base ` K ) ) )
10 xmetf 
 |-  ( ( dist ` K ) e. ( *Met ` ( Base ` K ) ) -> ( dist ` K ) : ( ( Base ` K ) X. ( Base ` K ) ) --> RR* )
11 ffn 
 |-  ( ( dist ` K ) : ( ( Base ` K ) X. ( Base ` K ) ) --> RR* -> ( dist ` K ) Fn ( ( Base ` K ) X. ( Base ` K ) ) )
12 fnresdm 
 |-  ( ( dist ` K ) Fn ( ( Base ` K ) X. ( Base ` K ) ) -> ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) = ( dist ` K ) )
13 6 10 11 12 4syl 
 |-  ( D e. ( *Met ` X ) -> ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) = ( dist ` K ) )
14 13 2 eqtr4d 
 |-  ( D e. ( *Met ` X ) -> ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) = D )
15 14 fveq2d 
 |-  ( D e. ( *Met ` X ) -> ( MetOpen ` ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) = ( MetOpen ` D ) )
16 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
17 1 16 tmstopn 
 |-  ( D e. ( *Met ` X ) -> ( MetOpen ` D ) = ( TopOpen ` K ) )
18 15 17 eqtr2d 
 |-  ( D e. ( *Met ` X ) -> ( TopOpen ` K ) = ( MetOpen ` ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) )
19 eqid 
 |-  ( TopOpen ` K ) = ( TopOpen ` K )
20 eqid 
 |-  ( Base ` K ) = ( Base ` K )
21 eqid 
 |-  ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) )
22 19 20 21 isxms2 
 |-  ( K e. *MetSp <-> ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( *Met ` ( Base ` K ) ) /\ ( TopOpen ` K ) = ( MetOpen ` ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ) ) )
23 9 18 22 sylanbrc 
 |-  ( D e. ( *Met ` X ) -> K e. *MetSp )