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 syl5eq 
 |-  ( 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 ) )