Metamath Proof Explorer

Theorem cnmpt2ds

Description: Continuity of the metric function; analogue of cnmpt22f which cannot be used directly because D is not necessarily a function. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypotheses cnmpt1ds.d 
|- D = ( dist ` G )
cnmpt1ds.j 
|- J = ( TopOpen ` G )
cnmpt1ds.r 
|- R = ( topGen ` ran (,) )
cnmpt1ds.g 
|- ( ph -> G e. MetSp )
cnmpt1ds.k 
|- ( ph -> K e. ( TopOn ` X ) )
cnmpt2ds.l 
|- ( ph -> L e. ( TopOn ` Y ) )
cnmpt2ds.a 
|- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( K tX L ) Cn J ) )
cnmpt2ds.b 
|- ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( K tX L ) Cn J ) )
Assertion cnmpt2ds 
|- ( ph -> ( x e. X , y e. Y |-> ( A D B ) ) e. ( ( K tX L ) Cn R ) )

Proof

Step Hyp Ref Expression
1 cnmpt1ds.d 
 |-  D = ( dist ` G )
2 cnmpt1ds.j 
 |-  J = ( TopOpen ` G )
3 cnmpt1ds.r 
 |-  R = ( topGen ` ran (,) )
4 cnmpt1ds.g 
 |-  ( ph -> G e. MetSp )
5 cnmpt1ds.k 
 |-  ( ph -> K e. ( TopOn ` X ) )
6 cnmpt2ds.l 
 |-  ( ph -> L e. ( TopOn ` Y ) )
7 cnmpt2ds.a 
 |-  ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( K tX L ) Cn J ) )
8 cnmpt2ds.b 
 |-  ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( K tX L ) Cn J ) )
9 txtopon 
 |-  ( ( K e. ( TopOn ` X ) /\ L e. ( TopOn ` Y ) ) -> ( K tX L ) e. ( TopOn ` ( X X. Y ) ) )
10 5 6 9 syl2anc 
 |-  ( ph -> ( K tX L ) e. ( TopOn ` ( X X. Y ) ) )
11 mstps 
 |-  ( G e. MetSp -> G e. TopSp )
12 4 11 syl 
 |-  ( ph -> G e. TopSp )
13 eqid 
 |-  ( Base ` G ) = ( Base ` G )
14 13 2 istps 
 |-  ( G e. TopSp <-> J e. ( TopOn ` ( Base ` G ) ) )
15 12 14 sylib 
 |-  ( ph -> J e. ( TopOn ` ( Base ` G ) ) )
16 cnf2 
 |-  ( ( ( K tX L ) e. ( TopOn ` ( X X. Y ) ) /\ J e. ( TopOn ` ( Base ` G ) ) /\ ( x e. X , y e. Y |-> A ) e. ( ( K tX L ) Cn J ) ) -> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> ( Base ` G ) )
17 10 15 7 16 syl3anc 
 |-  ( ph -> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> ( Base ` G ) )
18 eqid 
 |-  ( x e. X , y e. Y |-> A ) = ( x e. X , y e. Y |-> A )
19 18 fmpo 
 |-  ( A. x e. X A. y e. Y A e. ( Base ` G ) <-> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> ( Base ` G ) )
20 17 19 sylibr 
 |-  ( ph -> A. x e. X A. y e. Y A e. ( Base ` G ) )
21 20 r19.21bi 
 |-  ( ( ph /\ x e. X ) -> A. y e. Y A e. ( Base ` G ) )
22 21 r19.21bi 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> A e. ( Base ` G ) )
23 cnf2 
 |-  ( ( ( K tX L ) e. ( TopOn ` ( X X. Y ) ) /\ J e. ( TopOn ` ( Base ` G ) ) /\ ( x e. X , y e. Y |-> B ) e. ( ( K tX L ) Cn J ) ) -> ( x e. X , y e. Y |-> B ) : ( X X. Y ) --> ( Base ` G ) )
24 10 15 8 23 syl3anc 
 |-  ( ph -> ( x e. X , y e. Y |-> B ) : ( X X. Y ) --> ( Base ` G ) )
25 eqid 
 |-  ( x e. X , y e. Y |-> B ) = ( x e. X , y e. Y |-> B )
26 25 fmpo 
 |-  ( A. x e. X A. y e. Y B e. ( Base ` G ) <-> ( x e. X , y e. Y |-> B ) : ( X X. Y ) --> ( Base ` G ) )
27 24 26 sylibr 
 |-  ( ph -> A. x e. X A. y e. Y B e. ( Base ` G ) )
28 27 r19.21bi 
 |-  ( ( ph /\ x e. X ) -> A. y e. Y B e. ( Base ` G ) )
29 28 r19.21bi 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> B e. ( Base ` G ) )
30 22 29 ovresd 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> ( A ( D |` ( ( Base ` G ) X. ( Base ` G ) ) ) B ) = ( A D B ) )
31 30 3impa 
 |-  ( ( ph /\ x e. X /\ y e. Y ) -> ( A ( D |` ( ( Base ` G ) X. ( Base ` G ) ) ) B ) = ( A D B ) )
32 31 mpoeq3dva 
 |-  ( ph -> ( x e. X , y e. Y |-> ( A ( D |` ( ( Base ` G ) X. ( Base ` G ) ) ) B ) ) = ( x e. X , y e. Y |-> ( A D B ) ) )
33 13 1 2 3 msdcn 
 |-  ( G e. MetSp -> ( D |` ( ( Base ` G ) X. ( Base ` G ) ) ) e. ( ( J tX J ) Cn R ) )
34 4 33 syl 
 |-  ( ph -> ( D |` ( ( Base ` G ) X. ( Base ` G ) ) ) e. ( ( J tX J ) Cn R ) )
35 5 6 7 8 34 cnmpt22f 
 |-  ( ph -> ( x e. X , y e. Y |-> ( A ( D |` ( ( Base ` G ) X. ( Base ` G ) ) ) B ) ) e. ( ( K tX L ) Cn R ) )
36 32 35 eqeltrrd 
 |-  ( ph -> ( x e. X , y e. Y |-> ( A D B ) ) e. ( ( K tX L ) Cn R ) )