Description: A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | xpsms.t | |
|
Assertion | xpsxms | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpsms.t | |
|
2 | eqid | |
|
3 | eqid | |
|
4 | simpl | |
|
5 | simpr | |
|
6 | eqid | |
|
7 | eqid | |
|
8 | eqid | |
|
9 | 1 2 3 4 5 6 7 8 | xpsval | |
10 | 1 2 3 4 5 6 7 8 | xpsrnbas | |
11 | 6 | xpsff1o2 | |
12 | f1ocnv | |
|
13 | 11 12 | mp1i | |
14 | fvexd | |
|
15 | 2onn | |
|
16 | nnfi | |
|
17 | 15 16 | mp1i | |
18 | xpscf | |
|
19 | 18 | biimpri | |
20 | 8 | prdsxms | |
21 | 14 17 19 20 | syl3anc | |
22 | 9 10 13 21 | imasf1oxms | |