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