Step |
Hyp |
Ref |
Expression |
1 |
|
tmsxps.p |
⊢ 𝑃 = ( dist ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) |
2 |
|
tmsxps.1 |
⊢ ( 𝜑 → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ) |
3 |
|
tmsxps.2 |
⊢ ( 𝜑 → 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) |
4 |
|
tmsxpsmopn.j |
⊢ 𝐽 = ( MetOpen ‘ 𝑀 ) |
5 |
|
tmsxpsmopn.k |
⊢ 𝐾 = ( MetOpen ‘ 𝑁 ) |
6 |
|
tmsxpsmopn.l |
⊢ 𝐿 = ( MetOpen ‘ 𝑃 ) |
7 |
|
eqid |
⊢ ( toMetSp ‘ 𝑀 ) = ( toMetSp ‘ 𝑀 ) |
8 |
7
|
tmsxms |
⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → ( toMetSp ‘ 𝑀 ) ∈ ∞MetSp ) |
9 |
2 8
|
syl |
⊢ ( 𝜑 → ( toMetSp ‘ 𝑀 ) ∈ ∞MetSp ) |
10 |
|
xmstps |
⊢ ( ( toMetSp ‘ 𝑀 ) ∈ ∞MetSp → ( toMetSp ‘ 𝑀 ) ∈ TopSp ) |
11 |
9 10
|
syl |
⊢ ( 𝜑 → ( toMetSp ‘ 𝑀 ) ∈ TopSp ) |
12 |
|
eqid |
⊢ ( toMetSp ‘ 𝑁 ) = ( toMetSp ‘ 𝑁 ) |
13 |
12
|
tmsxms |
⊢ ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) → ( toMetSp ‘ 𝑁 ) ∈ ∞MetSp ) |
14 |
3 13
|
syl |
⊢ ( 𝜑 → ( toMetSp ‘ 𝑁 ) ∈ ∞MetSp ) |
15 |
|
xmstps |
⊢ ( ( toMetSp ‘ 𝑁 ) ∈ ∞MetSp → ( toMetSp ‘ 𝑁 ) ∈ TopSp ) |
16 |
14 15
|
syl |
⊢ ( 𝜑 → ( toMetSp ‘ 𝑁 ) ∈ TopSp ) |
17 |
|
eqid |
⊢ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) = ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) |
18 |
|
eqid |
⊢ ( TopOpen ‘ ( toMetSp ‘ 𝑀 ) ) = ( TopOpen ‘ ( toMetSp ‘ 𝑀 ) ) |
19 |
|
eqid |
⊢ ( TopOpen ‘ ( toMetSp ‘ 𝑁 ) ) = ( TopOpen ‘ ( toMetSp ‘ 𝑁 ) ) |
20 |
|
eqid |
⊢ ( TopOpen ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) = ( TopOpen ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) |
21 |
17 18 19 20
|
xpstopn |
⊢ ( ( ( toMetSp ‘ 𝑀 ) ∈ TopSp ∧ ( toMetSp ‘ 𝑁 ) ∈ TopSp ) → ( TopOpen ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) = ( ( TopOpen ‘ ( toMetSp ‘ 𝑀 ) ) ×t ( TopOpen ‘ ( toMetSp ‘ 𝑁 ) ) ) ) |
22 |
11 16 21
|
syl2anc |
⊢ ( 𝜑 → ( TopOpen ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) = ( ( TopOpen ‘ ( toMetSp ‘ 𝑀 ) ) ×t ( TopOpen ‘ ( toMetSp ‘ 𝑁 ) ) ) ) |
23 |
17
|
xpsxms |
⊢ ( ( ( toMetSp ‘ 𝑀 ) ∈ ∞MetSp ∧ ( toMetSp ‘ 𝑁 ) ∈ ∞MetSp ) → ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ∈ ∞MetSp ) |
24 |
9 14 23
|
syl2anc |
⊢ ( 𝜑 → ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ∈ ∞MetSp ) |
25 |
|
eqid |
⊢ ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) = ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) |
26 |
1
|
reseq1i |
⊢ ( 𝑃 ↾ ( ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) × ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) ) ) = ( ( dist ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) ↾ ( ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) × ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) ) ) |
27 |
20 25 26
|
xmstopn |
⊢ ( ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ∈ ∞MetSp → ( TopOpen ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) = ( MetOpen ‘ ( 𝑃 ↾ ( ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) × ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) ) ) ) ) |
28 |
24 27
|
syl |
⊢ ( 𝜑 → ( TopOpen ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) = ( MetOpen ‘ ( 𝑃 ↾ ( ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) × ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) ) ) ) ) |
29 |
|
eqid |
⊢ ( Base ‘ ( toMetSp ‘ 𝑀 ) ) = ( Base ‘ ( toMetSp ‘ 𝑀 ) ) |
30 |
|
eqid |
⊢ ( Base ‘ ( toMetSp ‘ 𝑁 ) ) = ( Base ‘ ( toMetSp ‘ 𝑁 ) ) |
31 |
17 29 30 9 14 1
|
xpsdsfn2 |
⊢ ( 𝜑 → 𝑃 Fn ( ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) × ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) ) ) |
32 |
|
fnresdm |
⊢ ( 𝑃 Fn ( ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) × ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) ) → ( 𝑃 ↾ ( ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) × ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) ) ) = 𝑃 ) |
33 |
31 32
|
syl |
⊢ ( 𝜑 → ( 𝑃 ↾ ( ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) × ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) ) ) = 𝑃 ) |
34 |
33
|
fveq2d |
⊢ ( 𝜑 → ( MetOpen ‘ ( 𝑃 ↾ ( ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) × ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) ) ) ) = ( MetOpen ‘ 𝑃 ) ) |
35 |
28 34
|
eqtr2d |
⊢ ( 𝜑 → ( MetOpen ‘ 𝑃 ) = ( TopOpen ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) ) |
36 |
6 35
|
syl5eq |
⊢ ( 𝜑 → 𝐿 = ( TopOpen ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) ) |
37 |
7 4
|
tmstopn |
⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 = ( TopOpen ‘ ( toMetSp ‘ 𝑀 ) ) ) |
38 |
2 37
|
syl |
⊢ ( 𝜑 → 𝐽 = ( TopOpen ‘ ( toMetSp ‘ 𝑀 ) ) ) |
39 |
12 5
|
tmstopn |
⊢ ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) → 𝐾 = ( TopOpen ‘ ( toMetSp ‘ 𝑁 ) ) ) |
40 |
3 39
|
syl |
⊢ ( 𝜑 → 𝐾 = ( TopOpen ‘ ( toMetSp ‘ 𝑁 ) ) ) |
41 |
38 40
|
oveq12d |
⊢ ( 𝜑 → ( 𝐽 ×t 𝐾 ) = ( ( TopOpen ‘ ( toMetSp ‘ 𝑀 ) ) ×t ( TopOpen ‘ ( toMetSp ‘ 𝑁 ) ) ) ) |
42 |
22 36 41
|
3eqtr4d |
⊢ ( 𝜑 → 𝐿 = ( 𝐽 ×t 𝐾 ) ) |