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 | |
|
Assertion | prdsxms | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prdsxms.y | |
|
2 | simp1 | |
|
3 | simp2 | |
|
4 | eqid | |
|
5 | eqid | |
|
6 | simp3 | |
|
7 | 1 2 3 4 5 6 | prdsxmslem1 | |
8 | ssid | |
|
9 | xmetres2 | |
|
10 | 7 8 9 | sylancl | |
11 | eqid | |
|
12 | eqid | |
|
13 | eqid | |
|
14 | eqid | |
|
15 | eqid | |
|
16 | 1 2 3 4 5 6 11 12 13 14 15 | prdsxmslem2 | |
17 | xmetf | |
|
18 | ffn | |
|
19 | fnresdm | |
|
20 | 7 17 18 19 | 4syl | |
21 | 20 | fveq2d | |
22 | 16 21 | eqtr4d | |
23 | eqid | |
|
24 | 11 5 23 | isxms2 | |
25 | 10 22 24 | sylanbrc | |