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 ∞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 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 ∞Met X D : X × X *
7 6 fdmd D ∞Met X dom D = X × X
8 7 dmeqd D ∞Met X dom dom D = dom X × X
9 dmxpid dom X × X = X
10 8 9 eqtrdi D ∞Met X dom dom D = X
11 5 10 sylan9eqr D ∞Met X d = D dom dom d = X
12 11 opeq2d D ∞Met X d = D Base ndx dom dom d = Base ndx X
13 simpr D ∞Met X d = D d = D
14 13 opeq2d D ∞Met X d = D dist ndx d = dist ndx D
15 12 14 preq12d D ∞Met X d = D Base ndx dom dom d dist ndx d = Base ndx X dist ndx D
16 15 1 eqtr4di D ∞Met X d = D Base ndx dom dom d dist ndx d = M
17 13 fveq2d D ∞Met X d = D MetOpen d = MetOpen D
18 17 opeq2d D ∞Met X d = D TopSet ndx MetOpen d = TopSet ndx MetOpen D
19 16 18 oveq12d D ∞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 ran ∞Met
21 20 sseli D ∞Met X D ran ∞Met
22 ovexd D ∞Met X M sSet TopSet ndx MetOpen D V
23 3 19 21 22 fvmptd2 D ∞Met X toMetSp D = M sSet TopSet ndx MetOpen D
24 2 23 syl5eq D ∞Met X K = M sSet TopSet ndx MetOpen D