Metamath Proof Explorer

Theorem tmsval

Description: For any metric there is an associated metric space. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses tmsval.m 
|- M = { <. ( Base ` ndx ) , X >. , <. ( dist ` ndx ) , D >. }
tmsval.k 
|- K = ( toMetSp ` D )
Assertion tmsval 
|- ( D e. ( *Met ` X ) -> K = ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) )

Proof

Step Hyp Ref Expression
1 tmsval.m 
 |-  M = { <. ( Base ` ndx ) , X >. , <. ( dist ` ndx ) , D >. }
2 tmsval.k 
 |-  K = ( toMetSp ` D )
3 df-tms 
 |-  toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. ( TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
4 dmeq 
 |-  ( d = D -> dom d = dom D )
5 4 dmeqd 
 |-  ( d = D -> dom dom d = dom dom D )
6 xmetf 
 |-  ( D e. ( *Met ` X ) -> D : ( X X. X ) --> RR* )
7 6 fdmd 
 |-  ( D e. ( *Met ` X ) -> dom D = ( X X. X ) )
8 7 dmeqd 
 |-  ( D e. ( *Met ` X ) -> dom dom D = dom ( X X. X ) )
9 dmxpid 
 |-  dom ( X X. X ) = X
10 8 9 eqtrdi 
 |-  ( D e. ( *Met ` X ) -> dom dom D = X )
11 5 10 sylan9eqr 
 |-  ( ( D e. ( *Met ` X ) /\ d = D ) -> dom dom d = X )
12 11 opeq2d 
 |-  ( ( D e. ( *Met ` X ) /\ d = D ) -> <. ( Base ` ndx ) , dom dom d >. = <. ( Base ` ndx ) , X >. )
13 simpr 
 |-  ( ( D e. ( *Met ` X ) /\ d = D ) -> d = D )
14 13 opeq2d 
 |-  ( ( D e. ( *Met ` X ) /\ d = D ) -> <. ( dist ` ndx ) , d >. = <. ( dist ` ndx ) , D >. )
15 12 14 preq12d 
 |-  ( ( D e. ( *Met ` X ) /\ d = D ) -> { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } = { <. ( Base ` ndx ) , X >. , <. ( dist ` ndx ) , D >. } )
16 15 1 eqtr4di 
 |-  ( ( D e. ( *Met ` X ) /\ d = D ) -> { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } = M )
17 13 fveq2d 
 |-  ( ( D e. ( *Met ` X ) /\ d = D ) -> ( MetOpen ` d ) = ( MetOpen ` D ) )
18 17 opeq2d 
 |-  ( ( D e. ( *Met ` X ) /\ d = D ) -> <. ( TopSet ` ndx ) , ( MetOpen ` d ) >. = <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. )
19 16 18 oveq12d 
 |-  ( ( D e. ( *Met ` X ) /\ d = D ) -> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. ( TopSet ` ndx ) , ( MetOpen ` d ) >. ) = ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) )
20 fvssunirn 
 |-  ( *Met ` X ) C_ U. ran *Met
21 20 sseli 
 |-  ( D e. ( *Met ` X ) -> D e. U. ran *Met )
22 ovexd 
 |-  ( D e. ( *Met ` X ) -> ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) e. _V )
23 3 19 21 22 fvmptd2 
 |-  ( D e. ( *Met ` X ) -> ( toMetSp ` D ) = ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) )
24 2 23 syl5eq 
 |-  ( D e. ( *Met ` X ) -> K = ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) )