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 ) Xs. ( toMetSp ` N ) ) )
tmsxps.1
|- ( ph -> M e. ( *Met ` X ) )
tmsxps.2
|- ( ph -> N e. ( *Met ` Y ) )
tmsxpsmopn.j
|- J = ( MetOpen ` M )
tmsxpsmopn.k
|- K = ( MetOpen ` N )
tmsxpsmopn.l
|- L = ( MetOpen ` P )
Assertion tmsxpsmopn
|- ( ph -> L = ( J tX K ) )

Proof

Step Hyp Ref Expression
1 tmsxps.p
 |-  P = ( dist ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) )
2 tmsxps.1
 |-  ( ph -> M e. ( *Met ` X ) )
3 tmsxps.2
 |-  ( ph -> N e. ( *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 e. ( *Met ` X ) -> ( toMetSp ` M ) e. *MetSp )
9 2 8 syl
 |-  ( ph -> ( toMetSp ` M ) e. *MetSp )
10 xmstps
 |-  ( ( toMetSp ` M ) e. *MetSp -> ( toMetSp ` M ) e. TopSp )
11 9 10 syl
 |-  ( ph -> ( toMetSp ` M ) e. TopSp )
12 eqid
 |-  ( toMetSp ` N ) = ( toMetSp ` N )
13 12 tmsxms
 |-  ( N e. ( *Met ` Y ) -> ( toMetSp ` N ) e. *MetSp )
14 3 13 syl
 |-  ( ph -> ( toMetSp ` N ) e. *MetSp )
15 xmstps
 |-  ( ( toMetSp ` N ) e. *MetSp -> ( toMetSp ` N ) e. TopSp )
16 14 15 syl
 |-  ( ph -> ( toMetSp ` N ) e. TopSp )
17 eqid
 |-  ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) = ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) )
18 eqid
 |-  ( TopOpen ` ( toMetSp ` M ) ) = ( TopOpen ` ( toMetSp ` M ) )
19 eqid
 |-  ( TopOpen ` ( toMetSp ` N ) ) = ( TopOpen ` ( toMetSp ` N ) )
20 eqid
 |-  ( TopOpen ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) = ( TopOpen ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) )
21 17 18 19 20 xpstopn
 |-  ( ( ( toMetSp ` M ) e. TopSp /\ ( toMetSp ` N ) e. TopSp ) -> ( TopOpen ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) = ( ( TopOpen ` ( toMetSp ` M ) ) tX ( TopOpen ` ( toMetSp ` N ) ) ) )
22 11 16 21 syl2anc
 |-  ( ph -> ( TopOpen ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) = ( ( TopOpen ` ( toMetSp ` M ) ) tX ( TopOpen ` ( toMetSp ` N ) ) ) )
23 17 xpsxms
 |-  ( ( ( toMetSp ` M ) e. *MetSp /\ ( toMetSp ` N ) e. *MetSp ) -> ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) e. *MetSp )
24 9 14 23 syl2anc
 |-  ( ph -> ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) e. *MetSp )
25 eqid
 |-  ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) = ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) )
26 1 reseq1i
 |-  ( P |` ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) ) = ( ( dist ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) |` ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) )
27 20 25 26 xmstopn
 |-  ( ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) e. *MetSp -> ( TopOpen ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) = ( MetOpen ` ( P |` ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) ) ) )
28 24 27 syl
 |-  ( ph -> ( TopOpen ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) = ( MetOpen ` ( P |` ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( 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
 |-  ( ph -> P Fn ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) )
32 fnresdm
 |-  ( P Fn ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) -> ( P |` ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) ) = P )
33 31 32 syl
 |-  ( ph -> ( P |` ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) ) = P )
34 33 fveq2d
 |-  ( ph -> ( MetOpen ` ( P |` ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) ) ) = ( MetOpen ` P ) )
35 28 34 eqtr2d
 |-  ( ph -> ( MetOpen ` P ) = ( TopOpen ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) )
36 6 35 eqtrid
 |-  ( ph -> L = ( TopOpen ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) )
37 7 4 tmstopn
 |-  ( M e. ( *Met ` X ) -> J = ( TopOpen ` ( toMetSp ` M ) ) )
38 2 37 syl
 |-  ( ph -> J = ( TopOpen ` ( toMetSp ` M ) ) )
39 12 5 tmstopn
 |-  ( N e. ( *Met ` Y ) -> K = ( TopOpen ` ( toMetSp ` N ) ) )
40 3 39 syl
 |-  ( ph -> K = ( TopOpen ` ( toMetSp ` N ) ) )
41 38 40 oveq12d
 |-  ( ph -> ( J tX K ) = ( ( TopOpen ` ( toMetSp ` M ) ) tX ( TopOpen ` ( toMetSp ` N ) ) ) )
42 22 36 41 3eqtr4d
 |-  ( ph -> L = ( J tX K ) )