Metamath Proof Explorer

Theorem lebnumlem2

Description: Lemma for lebnum . As a finite sum of point-to-set distance functions, which are continuous by metdscn , the function F is also continuous. (Contributed by Mario Carneiro, 14-Feb-2015) (Revised by AV, 30-Sep-2020)

Ref Expression
Hypotheses lebnum.j 
|- J = ( MetOpen ` D )
lebnum.d 
|- ( ph -> D e. ( Met ` X ) )
lebnum.c 
|- ( ph -> J e. Comp )
lebnum.s 
|- ( ph -> U C_ J )
lebnum.u 
|- ( ph -> X = U. U )
lebnumlem1.u 
|- ( ph -> U e. Fin )
lebnumlem1.n 
|- ( ph -> -. X e. U )
lebnumlem1.f 
|- F = ( y e. X |-> sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) )
lebnumlem2.k 
|- K = ( topGen ` ran (,) )
Assertion lebnumlem2 
|- ( ph -> F e. ( J Cn K ) )

Proof

Step Hyp Ref Expression
1 lebnum.j 
 |-  J = ( MetOpen ` D )
2 lebnum.d 
 |-  ( ph -> D e. ( Met ` X ) )
3 lebnum.c 
 |-  ( ph -> J e. Comp )
4 lebnum.s 
 |-  ( ph -> U C_ J )
5 lebnum.u 
 |-  ( ph -> X = U. U )
6 lebnumlem1.u 
 |-  ( ph -> U e. Fin )
7 lebnumlem1.n 
 |-  ( ph -> -. X e. U )
8 lebnumlem1.f 
 |-  F = ( y e. X |-> sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) )
9 lebnumlem2.k 
 |-  K = ( topGen ` ran (,) )
10 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
11 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
12 2 11 syl 
 |-  ( ph -> D e. ( *Met ` X ) )
13 1 mopntopon 
 |-  ( D e. ( *Met ` X ) -> J e. ( TopOn ` X ) )
14 12 13 syl 
 |-  ( ph -> J e. ( TopOn ` X ) )
15 2 adantr 
 |-  ( ( ph /\ k e. U ) -> D e. ( Met ` X ) )
16 difssd 
 |-  ( ( ph /\ k e. U ) -> ( X \ k ) C_ X )
17 12 adantr 
 |-  ( ( ph /\ k e. U ) -> D e. ( *Met ` X ) )
18 17 13 syl 
 |-  ( ( ph /\ k e. U ) -> J e. ( TopOn ` X ) )
19 4 sselda 
 |-  ( ( ph /\ k e. U ) -> k e. J )
20 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ k e. J ) -> k C_ X )
21 18 19 20 syl2anc 
 |-  ( ( ph /\ k e. U ) -> k C_ X )
22 eleq1 
 |-  ( k = X -> ( k e. U <-> X e. U ) )
23 22 notbid 
 |-  ( k = X -> ( -. k e. U <-> -. X e. U ) )
24 7 23 syl5ibrcom 
 |-  ( ph -> ( k = X -> -. k e. U ) )
25 24 necon2ad 
 |-  ( ph -> ( k e. U -> k =/= X ) )
26 25 imp 
 |-  ( ( ph /\ k e. U ) -> k =/= X )
27 pssdifn0 
 |-  ( ( k C_ X /\ k =/= X ) -> ( X \ k ) =/= (/) )
28 21 26 27 syl2anc 
 |-  ( ( ph /\ k e. U ) -> ( X \ k ) =/= (/) )
29 eqid 
 |-  ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) = ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) )
30 29 1 10 metdscn2 
 |-  ( ( D e. ( Met ` X ) /\ ( X \ k ) C_ X /\ ( X \ k ) =/= (/) ) -> ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) e. ( J Cn ( TopOpen ` CCfld ) ) )
31 15 16 28 30 syl3anc 
 |-  ( ( ph /\ k e. U ) -> ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) e. ( J Cn ( TopOpen ` CCfld ) ) )
32 10 14 6 31 fsumcn 
 |-  ( ph -> ( y e. X |-> sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) e. ( J Cn ( TopOpen ` CCfld ) ) )
33 8 32 eqeltrid 
 |-  ( ph -> F e. ( J Cn ( TopOpen ` CCfld ) ) )
34 10 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
35 34 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
36 1 2 3 4 5 6 7 8 lebnumlem1 
 |-  ( ph -> F : X --> RR+ )
37 36 frnd 
 |-  ( ph -> ran F C_ RR+ )
38 rpssre 
 |-  RR+ C_ RR
39 37 38 sstrdi 
 |-  ( ph -> ran F C_ RR )
40 ax-resscn 
 |-  RR C_ CC
41 40 a1i 
 |-  ( ph -> RR C_ CC )
42 cnrest2 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ran F C_ RR /\ RR C_ CC ) -> ( F e. ( J Cn ( TopOpen ` CCfld ) ) <-> F e. ( J Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) )
43 35 39 41 42 syl3anc 
 |-  ( ph -> ( F e. ( J Cn ( TopOpen ` CCfld ) ) <-> F e. ( J Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) )
44 33 43 mpbid 
 |-  ( ph -> F e. ( J Cn ( ( TopOpen ` CCfld ) |`t RR ) ) )
45 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
46 9 45 eqtri 
 |-  K = ( ( TopOpen ` CCfld ) |`t RR )
47 46 oveq2i 
 |-  ( J Cn K ) = ( J Cn ( ( TopOpen ` CCfld ) |`t RR ) )
48 44 47 eleqtrrdi 
 |-  ( ph -> F e. ( J Cn K ) )