Metamath Proof Explorer

Theorem lebnumlem3

Description: Lemma for lebnum . By the previous lemmas, F is continuous and positive on a compact set, so it has a positive minimum r . Then setting d = r / # ( U ) , since for each u e. U we have ball ( x , d ) C_ u iff d <_ d ( x , X \ u ) , if -. ball ( x , d ) C_ u for all u then summing over u yields sum_ u e. U d ( x , X \ u ) = F ( x ) < sum_ u e. U d = r , in contradiction to the assumption that r is the minimum of F . (Contributed by Mario Carneiro, 14-Feb-2015) (Revised by Mario Carneiro, 5-Sep-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 lebnumlem3 
|- ( ph -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u )

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 1rp 
 |-  1 e. RR+
11 10 ne0ii 
 |-  RR+ =/= (/)
12 ral0 
 |-  A. x e. (/) E. u e. U ( x ( ball ` D ) d ) C_ u
13 simpr 
 |-  ( ( ph /\ X = (/) ) -> X = (/) )
14 13 raleqdv 
 |-  ( ( ph /\ X = (/) ) -> ( A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u <-> A. x e. (/) E. u e. U ( x ( ball ` D ) d ) C_ u ) )
15 12 14 mpbiri 
 |-  ( ( ph /\ X = (/) ) -> A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u )
16 15 ralrimivw 
 |-  ( ( ph /\ X = (/) ) -> A. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u )
17 r19.2z 
 |-  ( ( RR+ =/= (/) /\ A. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u ) -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u )
18 11 16 17 sylancr 
 |-  ( ( ph /\ X = (/) ) -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u )
19 1 2 3 4 5 6 7 8 lebnumlem1 
 |-  ( ph -> F : X --> RR+ )
20 19 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> F : X --> RR+ )
21 20 frnd 
 |-  ( ( ph /\ X =/= (/) ) -> ran F C_ RR+ )
22 eqid 
 |-  U. J = U. J
23 3 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> J e. Comp )
24 1 2 3 4 5 6 7 8 9 lebnumlem2 
 |-  ( ph -> F e. ( J Cn K ) )
25 24 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> F e. ( J Cn K ) )
26 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
27 1 mopnuni 
 |-  ( D e. ( *Met ` X ) -> X = U. J )
28 2 26 27 3syl 
 |-  ( ph -> X = U. J )
29 28 neeq1d 
 |-  ( ph -> ( X =/= (/) <-> U. J =/= (/) ) )
30 29 biimpa 
 |-  ( ( ph /\ X =/= (/) ) -> U. J =/= (/) )
31 22 9 23 25 30 evth2 
 |-  ( ( ph /\ X =/= (/) ) -> E. w e. U. J A. x e. U. J ( F ` w ) <_ ( F ` x ) )
32 28 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> X = U. J )
33 raleq 
 |-  ( X = U. J -> ( A. x e. X ( F ` w ) <_ ( F ` x ) <-> A. x e. U. J ( F ` w ) <_ ( F ` x ) ) )
34 33 rexeqbi1dv 
 |-  ( X = U. J -> ( E. w e. X A. x e. X ( F ` w ) <_ ( F ` x ) <-> E. w e. U. J A. x e. U. J ( F ` w ) <_ ( F ` x ) ) )
35 32 34 syl 
 |-  ( ( ph /\ X =/= (/) ) -> ( E. w e. X A. x e. X ( F ` w ) <_ ( F ` x ) <-> E. w e. U. J A. x e. U. J ( F ` w ) <_ ( F ` x ) ) )
36 31 35 mpbird 
 |-  ( ( ph /\ X =/= (/) ) -> E. w e. X A. x e. X ( F ` w ) <_ ( F ` x ) )
37 ffn 
 |-  ( F : X --> RR+ -> F Fn X )
38 breq1 
 |-  ( r = ( F ` w ) -> ( r <_ ( F ` x ) <-> ( F ` w ) <_ ( F ` x ) ) )
39 38 ralbidv 
 |-  ( r = ( F ` w ) -> ( A. x e. X r <_ ( F ` x ) <-> A. x e. X ( F ` w ) <_ ( F ` x ) ) )
40 39 rexrn 
 |-  ( F Fn X -> ( E. r e. ran F A. x e. X r <_ ( F ` x ) <-> E. w e. X A. x e. X ( F ` w ) <_ ( F ` x ) ) )
41 20 37 40 3syl 
 |-  ( ( ph /\ X =/= (/) ) -> ( E. r e. ran F A. x e. X r <_ ( F ` x ) <-> E. w e. X A. x e. X ( F ` w ) <_ ( F ` x ) ) )
42 36 41 mpbird 
 |-  ( ( ph /\ X =/= (/) ) -> E. r e. ran F A. x e. X r <_ ( F ` x ) )
43 ssrexv 
 |-  ( ran F C_ RR+ -> ( E. r e. ran F A. x e. X r <_ ( F ` x ) -> E. r e. RR+ A. x e. X r <_ ( F ` x ) ) )
44 21 42 43 sylc 
 |-  ( ( ph /\ X =/= (/) ) -> E. r e. RR+ A. x e. X r <_ ( F ` x ) )
45 simpr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) -> r e. RR+ )
46 5 ad2antrr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) -> X = U. U )
47 simplr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) -> X =/= (/) )
48 46 47 eqnetrrd 
 |-  ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) -> U. U =/= (/) )
49 unieq 
 |-  ( U = (/) -> U. U = U. (/) )
50 uni0 
 |-  U. (/) = (/)
51 49 50 eqtrdi 
 |-  ( U = (/) -> U. U = (/) )
52 51 necon3i 
 |-  ( U. U =/= (/) -> U =/= (/) )
53 48 52 syl 
 |-  ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) -> U =/= (/) )
54 6 ad2antrr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) -> U e. Fin )
55 hashnncl 
 |-  ( U e. Fin -> ( ( # ` U ) e. NN <-> U =/= (/) ) )
56 54 55 syl 
 |-  ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) -> ( ( # ` U ) e. NN <-> U =/= (/) ) )
57 53 56 mpbird 
 |-  ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) -> ( # ` U ) e. NN )
58 57 nnrpd 
 |-  ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) -> ( # ` U ) e. RR+ )
59 45 58 rpdivcld 
 |-  ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) -> ( r / ( # ` U ) ) e. RR+ )
60 ralnex 
 |-  ( A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u <-> -. E. u e. U ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u )
61 54 adantr 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> U e. Fin )
62 53 adantr 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> U =/= (/) )
63 simprl 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> x e. X )
64 63 adantr 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> x e. X )
65 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* , < ) )
66 65 metdsval 
 |-  ( x e. X -> ( ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) ` x ) = inf ( ran ( z e. ( X \ k ) |-> ( x D z ) ) , RR* , < ) )
67 64 66 syl 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> ( ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) ` x ) = inf ( ran ( z e. ( X \ k ) |-> ( x D z ) ) , RR* , < ) )
68 2 ad2antrr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) -> D e. ( Met ` X ) )
69 68 ad2antrr 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> D e. ( Met ` X ) )
70 difssd 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> ( X \ k ) C_ X )
71 elssuni 
 |-  ( k e. U -> k C_ U. U )
72 71 adantl 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> k C_ U. U )
73 46 ad2antrr 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> X = U. U )
74 72 73 sseqtrrd 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> k C_ X )
75 eleq1 
 |-  ( k = X -> ( k e. U <-> X e. U ) )
76 75 notbid 
 |-  ( k = X -> ( -. k e. U <-> -. X e. U ) )
77 7 76 syl5ibrcom 
 |-  ( ph -> ( k = X -> -. k e. U ) )
78 77 necon2ad 
 |-  ( ph -> ( k e. U -> k =/= X ) )
79 78 ad3antrrr 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> ( k e. U -> k =/= X ) )
80 79 imp 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> k =/= X )
81 pssdifn0 
 |-  ( ( k C_ X /\ k =/= X ) -> ( X \ k ) =/= (/) )
82 74 80 81 syl2anc 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> ( X \ k ) =/= (/) )
83 65 metdsre 
 |-  ( ( D e. ( Met ` X ) /\ ( X \ k ) C_ X /\ ( X \ k ) =/= (/) ) -> ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) : X --> RR )
84 69 70 82 83 syl3anc 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) : X --> RR )
85 84 64 ffvelrnd 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> ( ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) ` x ) e. RR )
86 67 85 eqeltrrd 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> inf ( ran ( z e. ( X \ k ) |-> ( x D z ) ) , RR* , < ) e. RR )
87 59 ad2antrr 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> ( r / ( # ` U ) ) e. RR+ )
88 87 rpred 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> ( r / ( # ` U ) ) e. RR )
89 simprr 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u )
90 sseq2 
 |-  ( u = k -> ( ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u <-> ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ k ) )
91 90 notbid 
 |-  ( u = k -> ( -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u <-> -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ k ) )
92 91 rspccva 
 |-  ( ( A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u /\ k e. U ) -> -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ k )
93 89 92 sylan 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ k )
94 69 26 syl 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> D e. ( *Met ` X ) )
95 87 rpxrd 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> ( r / ( # ` U ) ) e. RR* )
96 65 metdsge 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( X \ k ) C_ X /\ x e. X ) /\ ( r / ( # ` U ) ) e. RR* ) -> ( ( r / ( # ` U ) ) <_ ( ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) ` x ) <-> ( ( X \ k ) i^i ( x ( ball ` D ) ( r / ( # ` U ) ) ) ) = (/) ) )
97 94 70 64 95 96 syl31anc 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> ( ( r / ( # ` U ) ) <_ ( ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) ` x ) <-> ( ( X \ k ) i^i ( x ( ball ` D ) ( r / ( # ` U ) ) ) ) = (/) ) )
98 blssm 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X /\ ( r / ( # ` U ) ) e. RR* ) -> ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ X )
99 94 64 95 98 syl3anc 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ X )
100 difin0ss 
 |-  ( ( ( X \ k ) i^i ( x ( ball ` D ) ( r / ( # ` U ) ) ) ) = (/) -> ( ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ X -> ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ k ) )
101 99 100 syl5com 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> ( ( ( X \ k ) i^i ( x ( ball ` D ) ( r / ( # ` U ) ) ) ) = (/) -> ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ k ) )
102 97 101 sylbid 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> ( ( r / ( # ` U ) ) <_ ( ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) ` x ) -> ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ k ) )
103 93 102 mtod 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> -. ( r / ( # ` U ) ) <_ ( ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) ` x ) )
104 85 88 ltnled 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> ( ( ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) ` x ) < ( r / ( # ` U ) ) <-> -. ( r / ( # ` U ) ) <_ ( ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) ` x ) ) )
105 103 104 mpbird 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> ( ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) ` x ) < ( r / ( # ` U ) ) )
106 67 105 eqbrtrrd 
 |-  ( ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) /\ k e. U ) -> inf ( ran ( z e. ( X \ k ) |-> ( x D z ) ) , RR* , < ) < ( r / ( # ` U ) ) )
107 61 62 86 88 106 fsumlt 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( x D z ) ) , RR* , < ) < sum_ k e. U ( r / ( # ` U ) ) )
108 oveq1 
 |-  ( y = x -> ( y D z ) = ( x D z ) )
109 108 mpteq2dv 
 |-  ( y = x -> ( z e. ( X \ k ) |-> ( y D z ) ) = ( z e. ( X \ k ) |-> ( x D z ) ) )
110 109 rneqd 
 |-  ( y = x -> ran ( z e. ( X \ k ) |-> ( y D z ) ) = ran ( z e. ( X \ k ) |-> ( x D z ) ) )
111 110 infeq1d 
 |-  ( y = x -> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) = inf ( ran ( z e. ( X \ k ) |-> ( x D z ) ) , RR* , < ) )
112 111 sumeq2sdv 
 |-  ( y = x -> sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) = sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( x D z ) ) , RR* , < ) )
113 sumex 
 |-  sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( x D z ) ) , RR* , < ) e. _V
114 112 8 113 fvmpt 
 |-  ( x e. X -> ( F ` x ) = sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( x D z ) ) , RR* , < ) )
115 63 114 syl 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> ( F ` x ) = sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( x D z ) ) , RR* , < ) )
116 59 adantr 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> ( r / ( # ` U ) ) e. RR+ )
117 116 rpcnd 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> ( r / ( # ` U ) ) e. CC )
118 fsumconst 
 |-  ( ( U e. Fin /\ ( r / ( # ` U ) ) e. CC ) -> sum_ k e. U ( r / ( # ` U ) ) = ( ( # ` U ) x. ( r / ( # ` U ) ) ) )
119 61 117 118 syl2anc 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> sum_ k e. U ( r / ( # ` U ) ) = ( ( # ` U ) x. ( r / ( # ` U ) ) ) )
120 simplr 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> r e. RR+ )
121 120 rpcnd 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> r e. CC )
122 57 adantr 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> ( # ` U ) e. NN )
123 122 nncnd 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> ( # ` U ) e. CC )
124 122 nnne0d 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> ( # ` U ) =/= 0 )
125 121 123 124 divcan2d 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> ( ( # ` U ) x. ( r / ( # ` U ) ) ) = r )
126 119 125 eqtr2d 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> r = sum_ k e. U ( r / ( # ` U ) ) )
127 107 115 126 3brtr4d 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> ( F ` x ) < r )
128 20 ad2antrr 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> F : X --> RR+ )
129 128 63 ffvelrnd 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> ( F ` x ) e. RR+ )
130 129 rpred 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> ( F ` x ) e. RR )
131 120 rpred 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> r e. RR )
132 130 131 ltnled 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> ( ( F ` x ) < r <-> -. r <_ ( F ` x ) ) )
133 127 132 mpbid 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ ( x e. X /\ A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) ) -> -. r <_ ( F ` x ) )
134 133 expr 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ x e. X ) -> ( A. u e. U -. ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u -> -. r <_ ( F ` x ) ) )
135 60 134 syl5bir 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ x e. X ) -> ( -. E. u e. U ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u -> -. r <_ ( F ` x ) ) )
136 135 con4d 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) /\ x e. X ) -> ( r <_ ( F ` x ) -> E. u e. U ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) )
137 136 ralimdva 
 |-  ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) -> ( A. x e. X r <_ ( F ` x ) -> A. x e. X E. u e. U ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) )
138 oveq2 
 |-  ( d = ( r / ( # ` U ) ) -> ( x ( ball ` D ) d ) = ( x ( ball ` D ) ( r / ( # ` U ) ) ) )
139 138 sseq1d 
 |-  ( d = ( r / ( # ` U ) ) -> ( ( x ( ball ` D ) d ) C_ u <-> ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) )
140 139 rexbidv 
 |-  ( d = ( r / ( # ` U ) ) -> ( E. u e. U ( x ( ball ` D ) d ) C_ u <-> E. u e. U ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) )
141 140 ralbidv 
 |-  ( d = ( r / ( # ` U ) ) -> ( A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u <-> A. x e. X E. u e. U ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) )
142 141 rspcev 
 |-  ( ( ( r / ( # ` U ) ) e. RR+ /\ A. x e. X E. u e. U ( x ( ball ` D ) ( r / ( # ` U ) ) ) C_ u ) -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u )
143 59 137 142 syl6an 
 |-  ( ( ( ph /\ X =/= (/) ) /\ r e. RR+ ) -> ( A. x e. X r <_ ( F ` x ) -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u ) )
144 143 rexlimdva 
 |-  ( ( ph /\ X =/= (/) ) -> ( E. r e. RR+ A. x e. X r <_ ( F ` x ) -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u ) )
145 44 144 mpd 
 |-  ( ( ph /\ X =/= (/) ) -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u )
146 18 145 pm2.61dane 
 |-  ( ph -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u )