Metamath Proof Explorer

Theorem cnmpt1ds

Description: Continuity of the metric function; analogue of cnmpt12f 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 ) )
cnmpt1ds.a 
|- ( ph -> ( x e. X |-> A ) e. ( K Cn J ) )
cnmpt1ds.b 
|- ( ph -> ( x e. X |-> B ) e. ( K Cn J ) )
Assertion cnmpt1ds 
|- ( ph -> ( x e. X |-> ( A D B ) ) e. ( K 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 cnmpt1ds.a 
 |-  ( ph -> ( x e. X |-> A ) e. ( K Cn J ) )
7 cnmpt1ds.b 
 |-  ( ph -> ( x e. X |-> B ) e. ( K Cn J ) )
8 mstps 
 |-  ( G e. MetSp -> G e. TopSp )
9 4 8 syl 
 |-  ( ph -> G e. TopSp )
10 eqid 
 |-  ( Base ` G ) = ( Base ` G )
11 10 2 istps 
 |-  ( G e. TopSp <-> J e. ( TopOn ` ( Base ` G ) ) )
12 9 11 sylib 
 |-  ( ph -> J e. ( TopOn ` ( Base ` G ) ) )
13 cnf2 
 |-  ( ( K e. ( TopOn ` X ) /\ J e. ( TopOn ` ( Base ` G ) ) /\ ( x e. X |-> A ) e. ( K Cn J ) ) -> ( x e. X |-> A ) : X --> ( Base ` G ) )
14 5 12 6 13 syl3anc 
 |-  ( ph -> ( x e. X |-> A ) : X --> ( Base ` G ) )
15 14 fvmptelrn 
 |-  ( ( ph /\ x e. X ) -> A e. ( Base ` G ) )
16 cnf2 
 |-  ( ( K e. ( TopOn ` X ) /\ J e. ( TopOn ` ( Base ` G ) ) /\ ( x e. X |-> B ) e. ( K Cn J ) ) -> ( x e. X |-> B ) : X --> ( Base ` G ) )
17 5 12 7 16 syl3anc 
 |-  ( ph -> ( x e. X |-> B ) : X --> ( Base ` G ) )
18 17 fvmptelrn 
 |-  ( ( ph /\ x e. X ) -> B e. ( Base ` G ) )
19 15 18 ovresd 
 |-  ( ( ph /\ x e. X ) -> ( A ( D |` ( ( Base ` G ) X. ( Base ` G ) ) ) B ) = ( A D B ) )
20 19 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( A ( D |` ( ( Base ` G ) X. ( Base ` G ) ) ) B ) ) = ( x e. X |-> ( A D B ) ) )
21 10 1 2 3 msdcn 
 |-  ( G e. MetSp -> ( D |` ( ( Base ` G ) X. ( Base ` G ) ) ) e. ( ( J tX J ) Cn R ) )
22 4 21 syl 
 |-  ( ph -> ( D |` ( ( Base ` G ) X. ( Base ` G ) ) ) e. ( ( J tX J ) Cn R ) )
23 5 6 7 22 cnmpt12f 
 |-  ( ph -> ( x e. X |-> ( A ( D |` ( ( Base ` G ) X. ( Base ` G ) ) ) B ) ) e. ( K Cn R ) )
24 20 23 eqeltrrd 
 |-  ( ph -> ( x e. X |-> ( A D B ) ) e. ( K Cn R ) )