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 eqtrid ⊢ ( 𝜑 → 𝐿 = ( 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 𝐾 ) )