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 S W I Fin R : I ∞MetSp Y ∞MetSp

Proof

Step Hyp Ref Expression
1 prdsxms.y Y = S 𝑠 R
2 simp1 S W I Fin R : I ∞MetSp S W
3 simp2 S W I Fin R : I ∞MetSp I Fin
4 eqid dist Y = dist Y
5 eqid Base Y = Base Y
6 simp3 S W I Fin R : I ∞MetSp R : I ∞MetSp
7 1 2 3 4 5 6 prdsxmslem1 S W I Fin R : I ∞MetSp dist Y ∞Met Base Y
8 ssid Base Y Base Y
9 xmetres2 dist Y ∞Met Base Y Base Y Base Y dist Y Base Y × Base Y ∞Met Base Y
10 7 8 9 sylancl S W I Fin R : I ∞MetSp dist Y Base Y × Base Y ∞Met Base Y
11 eqid TopOpen Y = TopOpen Y
12 eqid Base R k = Base R k
13 eqid dist R k Base R k × Base R k = dist R k Base R k × Base R k
14 eqid TopOpen R k = TopOpen R k
15 eqid x | g g Fn I k I g k TopOpen R k z Fin k I z g k = TopOpen R k x = k I g k = x | g g Fn I k I g k TopOpen R k z Fin k I z g k = TopOpen R k x = k I g k
16 1 2 3 4 5 6 11 12 13 14 15 prdsxmslem2 S W I Fin R : I ∞MetSp TopOpen Y = MetOpen dist Y
17 xmetf dist Y ∞Met Base Y dist Y : Base Y × Base Y *
18 ffn dist Y : Base Y × Base Y * dist Y Fn Base Y × Base Y
19 fnresdm dist Y Fn Base Y × Base Y dist Y Base Y × Base Y = dist Y
20 7 17 18 19 4syl S W I Fin R : I ∞MetSp dist Y Base Y × Base Y = dist Y
21 20 fveq2d S W I Fin R : I ∞MetSp MetOpen dist Y Base Y × Base Y = MetOpen dist Y
22 16 21 eqtr4d S W I Fin R : I ∞MetSp TopOpen Y = MetOpen dist Y Base Y × Base Y
23 eqid dist Y Base Y × Base Y = dist Y Base Y × Base Y
24 11 5 23 isxms2 Y ∞MetSp dist Y Base Y × Base Y ∞Met Base Y TopOpen Y = MetOpen dist Y Base Y × Base Y
25 10 22 24 sylanbrc S W I Fin R : I ∞MetSp Y ∞MetSp