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 × t K

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 × t TopOpen ⁡ toMetSp ⁡ N
22 11 16 21 syl2anc ⊢ φ → TopOpen ⁡ toMetSp ⁡ M × 𝑠 toMetSp ⁡ N = TopOpen ⁡ toMetSp ⁡ M × t TopOpen ⁡ 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 ⊢ Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N = Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N
26 1 reseq1i ⊢ P ↾ Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N × Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N = dist ⁡ toMetSp ⁡ M × 𝑠 toMetSp ⁡ N ↾ Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N × Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N
27 20 25 26 xmstopn ⊢ toMetSp ⁡ M × 𝑠 toMetSp ⁡ N ∈ ∞MetSp → TopOpen ⁡ toMetSp ⁡ M × 𝑠 toMetSp ⁡ N = MetOpen ⁡ P ↾ Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N × Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N
28 24 27 syl ⊢ φ → TopOpen ⁡ toMetSp ⁡ M × 𝑠 toMetSp ⁡ N = MetOpen ⁡ P ↾ Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N × Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N
29 eqid ⊢ Base toMetSp ⁡ M = Base toMetSp ⁡ M
30 eqid ⊢ Base toMetSp ⁡ N = Base toMetSp ⁡ N
31 17 29 30 9 14 1 xpsdsfn2 ⊢ φ → P Fn Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N × Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N
32 fnresdm ⊢ P Fn Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N × Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N → P ↾ Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N × Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N = P
33 31 32 syl ⊢ φ → P ↾ Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N × Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N = P
34 33 fveq2d ⊢ φ → MetOpen ⁡ P ↾ Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N × Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N = MetOpen ⁡ P
35 28 34 eqtr2d ⊢ φ → MetOpen ⁡ P = TopOpen ⁡ toMetSp ⁡ M × 𝑠 toMetSp ⁡ N
36 6 35 syl5eq ⊢ φ → 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 × t K = TopOpen ⁡ toMetSp ⁡ M × t TopOpen ⁡ toMetSp ⁡ N
42 22 36 41 3eqtr4d ⊢ φ → L = J × t K