Metamath Proof Explorer


Theorem prdsxms

Description: The indexed product structure is an extended metric space when the index set is finite. (Although the extended metric is still valid when the index set is infinite, it no longer agrees with the product topology, which is not metrizable in any case.) (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypothesis prdsxms.y Y=S𝑠R
Assertion prdsxms SWIFinR:I∞MetSpY∞MetSp

Proof

Step Hyp Ref Expression
1 prdsxms.y Y=S𝑠R
2 simp1 SWIFinR:I∞MetSpSW
3 simp2 SWIFinR:I∞MetSpIFin
4 eqid distY=distY
5 eqid BaseY=BaseY
6 simp3 SWIFinR:I∞MetSpR:I∞MetSp
7 1 2 3 4 5 6 prdsxmslem1 SWIFinR:I∞MetSpdistY∞MetBaseY
8 ssid BaseYBaseY
9 xmetres2 distY∞MetBaseYBaseYBaseYdistYBaseY×BaseY∞MetBaseY
10 7 8 9 sylancl SWIFinR:I∞MetSpdistYBaseY×BaseY∞MetBaseY
11 eqid TopOpenY=TopOpenY
12 eqid BaseRk=BaseRk
13 eqid distRkBaseRk×BaseRk=distRkBaseRk×BaseRk
14 eqid TopOpenRk=TopOpenRk
15 eqid x|ggFnIkIgkTopOpenRkzFinkIzgk=TopOpenRkx=kIgk=x|ggFnIkIgkTopOpenRkzFinkIzgk=TopOpenRkx=kIgk
16 1 2 3 4 5 6 11 12 13 14 15 prdsxmslem2 SWIFinR:I∞MetSpTopOpenY=MetOpendistY
17 xmetf distY∞MetBaseYdistY:BaseY×BaseY*
18 ffn distY:BaseY×BaseY*distYFnBaseY×BaseY
19 fnresdm distYFnBaseY×BaseYdistYBaseY×BaseY=distY
20 7 17 18 19 4syl SWIFinR:I∞MetSpdistYBaseY×BaseY=distY
21 20 fveq2d SWIFinR:I∞MetSpMetOpendistYBaseY×BaseY=MetOpendistY
22 16 21 eqtr4d SWIFinR:I∞MetSpTopOpenY=MetOpendistYBaseY×BaseY
23 eqid distYBaseY×BaseY=distYBaseY×BaseY
24 11 5 23 isxms2 Y∞MetSpdistYBaseY×BaseY∞MetBaseYTopOpenY=MetOpendistYBaseY×BaseY
25 10 22 24 sylanbrc SWIFinR:I∞MetSpY∞MetSp