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 𝑃 = ( dist ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) )
tmsxps.1 ( 𝜑𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
tmsxps.2 ( 𝜑𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
tmsxpsmopn.j 𝐽 = ( MetOpen ‘ 𝑀 )
tmsxpsmopn.k 𝐾 = ( MetOpen ‘ 𝑁 )
tmsxpsmopn.l 𝐿 = ( MetOpen ‘ 𝑃 )
Assertion tmsxpsmopn ( 𝜑𝐿 = ( 𝐽 ×t 𝐾 ) )

Proof

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 𝐾 ) )