Metamath Proof Explorer

Theorem tmsxpsmopn

Description: Express the product of two metrics as another metric. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses tmsxps.p ⊢P=dist⁡toMetSp⁡M×𝑠toMetSp⁡N
tmsxps.1 ⊢φ→M∈∞Met⁡X
tmsxps.2 ⊢φ→N∈∞Met⁡Y
tmsxpsmopn.j ⊢J=MetOpen⁡M
tmsxpsmopn.k ⊢K=MetOpen⁡N
tmsxpsmopn.l ⊢L=MetOpen⁡P
Assertion tmsxpsmopn ⊢φ→L=J×tK

Proof

Step Hyp Ref Expression
1 tmsxps.p ⊢P=dist⁡toMetSp⁡M×𝑠toMetSp⁡N
2 tmsxps.1 ⊢φ→M∈∞Met⁡X
3 tmsxps.2 ⊢φ→N∈∞Met⁡Y
4 tmsxpsmopn.j ⊢J=MetOpen⁡M
5 tmsxpsmopn.k ⊢K=MetOpen⁡N
6 tmsxpsmopn.l ⊢L=MetOpen⁡P
7 eqid ⊢toMetSp⁡M=toMetSp⁡M
8 7 tmsxms ⊢M∈∞Met⁡X→toMetSp⁡M∈∞MetSp
9 2 8 syl ⊢φ→toMetSp⁡M∈∞MetSp
10 xmstps ⊢toMetSp⁡M∈∞MetSp→toMetSp⁡M∈TopSp
11 9 10 syl ⊢φ→toMetSp⁡M∈TopSp
12 eqid ⊢toMetSp⁡N=toMetSp⁡N
13 12 tmsxms ⊢N∈∞Met⁡Y→toMetSp⁡N∈∞MetSp
14 3 13 syl ⊢φ→toMetSp⁡N∈∞MetSp
15 xmstps ⊢toMetSp⁡N∈∞MetSp→toMetSp⁡N∈TopSp
16 14 15 syl ⊢φ→toMetSp⁡N∈TopSp
17 eqid ⊢toMetSp⁡M×𝑠toMetSp⁡N=toMetSp⁡M×𝑠toMetSp⁡N
18 eqid ⊢TopOpen⁡toMetSp⁡M=TopOpen⁡toMetSp⁡M
19 eqid ⊢TopOpen⁡toMetSp⁡N=TopOpen⁡toMetSp⁡N
20 eqid ⊢TopOpen⁡toMetSp⁡M×𝑠toMetSp⁡N=TopOpen⁡toMetSp⁡M×𝑠toMetSp⁡N
21 17 18 19 20 xpstopn ⊢toMetSp⁡M∈TopSp∧toMetSp⁡N∈TopSp→TopOpen⁡toMetSp⁡M×𝑠toMetSp⁡N=TopOpen⁡toMetSp⁡M×tTopOpen⁡toMetSp⁡N
22 11 16 21 syl2anc ⊢φ→TopOpen⁡toMetSp⁡M×𝑠toMetSp⁡N=TopOpen⁡toMetSp⁡M×tTopOpen⁡toMetSp⁡N
23 17 xpsxms ⊢toMetSp⁡M∈∞MetSp∧toMetSp⁡N∈∞MetSp→toMetSp⁡M×𝑠toMetSp⁡N∈∞MetSp
24 9 14 23 syl2anc ⊢φ→toMetSp⁡M×𝑠toMetSp⁡N∈∞MetSp
25 eqid ⊢BasetoMetSp⁡M×𝑠toMetSp⁡N=BasetoMetSp⁡M×𝑠toMetSp⁡N
26 1 reseq1i ⊢P↾BasetoMetSp⁡M×𝑠toMetSp⁡N×BasetoMetSp⁡M×𝑠toMetSp⁡N=dist⁡toMetSp⁡M×𝑠toMetSp⁡N↾BasetoMetSp⁡M×𝑠toMetSp⁡N×BasetoMetSp⁡M×𝑠toMetSp⁡N
27 20 25 26 xmstopn ⊢toMetSp⁡M×𝑠toMetSp⁡N∈∞MetSp→TopOpen⁡toMetSp⁡M×𝑠toMetSp⁡N=MetOpen⁡P↾BasetoMetSp⁡M×𝑠toMetSp⁡N×BasetoMetSp⁡M×𝑠toMetSp⁡N
28 24 27 syl ⊢φ→TopOpen⁡toMetSp⁡M×𝑠toMetSp⁡N=MetOpen⁡P↾BasetoMetSp⁡M×𝑠toMetSp⁡N×BasetoMetSp⁡M×𝑠toMetSp⁡N
29 eqid ⊢BasetoMetSp⁡M=BasetoMetSp⁡M
30 eqid ⊢BasetoMetSp⁡N=BasetoMetSp⁡N
31 17 29 30 9 14 1 xpsdsfn2 ⊢φ→PFnBasetoMetSp⁡M×𝑠toMetSp⁡N×BasetoMetSp⁡M×𝑠toMetSp⁡N
32 fnresdm ⊢PFnBasetoMetSp⁡M×𝑠toMetSp⁡N×BasetoMetSp⁡M×𝑠toMetSp⁡N→P↾BasetoMetSp⁡M×𝑠toMetSp⁡N×BasetoMetSp⁡M×𝑠toMetSp⁡N=P
33 31 32 syl ⊢φ→P↾BasetoMetSp⁡M×𝑠toMetSp⁡N×BasetoMetSp⁡M×𝑠toMetSp⁡N=P
34 33 fveq2d ⊢φ→MetOpen⁡P↾BasetoMetSp⁡M×𝑠toMetSp⁡N×BasetoMetSp⁡M×𝑠toMetSp⁡N=MetOpen⁡P
35 28 34 eqtr2d ⊢φ→MetOpen⁡P=TopOpen⁡toMetSp⁡M×𝑠toMetSp⁡N
36 6 35 eqtrid ⊢φ→L=TopOpen⁡toMetSp⁡M×𝑠toMetSp⁡N
37 7 4 tmstopn ⊢M∈∞Met⁡X→J=TopOpen⁡toMetSp⁡M
38 2 37 syl ⊢φ→J=TopOpen⁡toMetSp⁡M
39 12 5 tmstopn ⊢N∈∞Met⁡Y→K=TopOpen⁡toMetSp⁡N
40 3 39 syl ⊢φ→K=TopOpen⁡toMetSp⁡N
41 38 40 oveq12d ⊢φ→J×tK=TopOpen⁡toMetSp⁡M×tTopOpen⁡toMetSp⁡N
42 22 36 41 3eqtr4d ⊢φ→L=J×tK