Metamath Proof Explorer

Theorem psercn

Description: An infinite series converges to a continuous function on the open disk of radius R , where R is the radius of convergence of the series. (Contributed by Mario Carneiro, 4-Mar-2015)

Ref Expression
Hypotheses pserf.g 
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
pserf.f 
|- F = ( y e. S |-> sum_ j e. NN0 ( ( G ` y ) ` j ) )
pserf.a 
|- ( ph -> A : NN0 --> CC )
pserf.r 
|- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )
psercn.s 
|- S = ( `' abs " ( 0 [,) R ) )
psercn.m 
|- M = if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) )
Assertion psercn 
|- ( ph -> F e. ( S -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 pserf.g 
 |-  G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )
2 pserf.f 
 |-  F = ( y e. S |-> sum_ j e. NN0 ( ( G ` y ) ` j ) )
3 pserf.a 
 |-  ( ph -> A : NN0 --> CC )
4 pserf.r 
 |-  R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )
5 psercn.s 
 |-  S = ( `' abs " ( 0 [,) R ) )
6 psercn.m 
 |-  M = if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) )
7 sumex 
 |-  sum_ j e. NN0 ( ( G ` y ) ` j ) e. _V
8 7 rgenw 
 |-  A. y e. S sum_ j e. NN0 ( ( G ` y ) ` j ) e. _V
9 2 fnmpt 
 |-  ( A. y e. S sum_ j e. NN0 ( ( G ` y ) ` j ) e. _V -> F Fn S )
10 8 9 mp1i 
 |-  ( ph -> F Fn S )
11 cnvimass 
 |-  ( `' abs " ( 0 [,) R ) ) C_ dom abs
12 absf 
 |-  abs : CC --> RR
13 12 fdmi 
 |-  dom abs = CC
14 11 13 sseqtri 
 |-  ( `' abs " ( 0 [,) R ) ) C_ CC
15 5 14 eqsstri 
 |-  S C_ CC
16 15 a1i 
 |-  ( ph -> S C_ CC )
17 16 sselda 
 |-  ( ( ph /\ a e. S ) -> a e. CC )
18 0cn 
 |-  0 e. CC
19 eqid 
 |-  ( abs o. - ) = ( abs o. - )
20 19 cnmetdval 
 |-  ( ( 0 e. CC /\ a e. CC ) -> ( 0 ( abs o. - ) a ) = ( abs ` ( 0 - a ) ) )
21 18 17 20 sylancr 
 |-  ( ( ph /\ a e. S ) -> ( 0 ( abs o. - ) a ) = ( abs ` ( 0 - a ) ) )
22 abssub 
 |-  ( ( 0 e. CC /\ a e. CC ) -> ( abs ` ( 0 - a ) ) = ( abs ` ( a - 0 ) ) )
23 18 17 22 sylancr 
 |-  ( ( ph /\ a e. S ) -> ( abs ` ( 0 - a ) ) = ( abs ` ( a - 0 ) ) )
24 17 subid1d 
 |-  ( ( ph /\ a e. S ) -> ( a - 0 ) = a )
25 24 fveq2d 
 |-  ( ( ph /\ a e. S ) -> ( abs ` ( a - 0 ) ) = ( abs ` a ) )
26 21 23 25 3eqtrd 
 |-  ( ( ph /\ a e. S ) -> ( 0 ( abs o. - ) a ) = ( abs ` a ) )
27 breq2 
 |-  ( ( ( ( abs ` a ) + R ) / 2 ) = if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) ) -> ( ( abs ` a ) < ( ( ( abs ` a ) + R ) / 2 ) <-> ( abs ` a ) < if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) ) ) )
28 breq2 
 |-  ( ( ( abs ` a ) + 1 ) = if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) ) -> ( ( abs ` a ) < ( ( abs ` a ) + 1 ) <-> ( abs ` a ) < if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) ) ) )
29 simpr 
 |-  ( ( ph /\ a e. S ) -> a e. S )
30 29 5 eleqtrdi 
 |-  ( ( ph /\ a e. S ) -> a e. ( `' abs " ( 0 [,) R ) ) )
31 ffn 
 |-  ( abs : CC --> RR -> abs Fn CC )
32 elpreima 
 |-  ( abs Fn CC -> ( a e. ( `' abs " ( 0 [,) R ) ) <-> ( a e. CC /\ ( abs ` a ) e. ( 0 [,) R ) ) ) )
33 12 31 32 mp2b 
 |-  ( a e. ( `' abs " ( 0 [,) R ) ) <-> ( a e. CC /\ ( abs ` a ) e. ( 0 [,) R ) ) )
34 30 33 sylib 
 |-  ( ( ph /\ a e. S ) -> ( a e. CC /\ ( abs ` a ) e. ( 0 [,) R ) ) )
35 34 simprd 
 |-  ( ( ph /\ a e. S ) -> ( abs ` a ) e. ( 0 [,) R ) )
36 0re 
 |-  0 e. RR
37 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
38 1 3 4 radcnvcl 
 |-  ( ph -> R e. ( 0 [,] +oo ) )
39 38 adantr 
 |-  ( ( ph /\ a e. S ) -> R e. ( 0 [,] +oo ) )
40 37 39 sselid 
 |-  ( ( ph /\ a e. S ) -> R e. RR* )
41 elico2 
 |-  ( ( 0 e. RR /\ R e. RR* ) -> ( ( abs ` a ) e. ( 0 [,) R ) <-> ( ( abs ` a ) e. RR /\ 0 <_ ( abs ` a ) /\ ( abs ` a ) < R ) ) )
42 36 40 41 sylancr 
 |-  ( ( ph /\ a e. S ) -> ( ( abs ` a ) e. ( 0 [,) R ) <-> ( ( abs ` a ) e. RR /\ 0 <_ ( abs ` a ) /\ ( abs ` a ) < R ) ) )
43 35 42 mpbid 
 |-  ( ( ph /\ a e. S ) -> ( ( abs ` a ) e. RR /\ 0 <_ ( abs ` a ) /\ ( abs ` a ) < R ) )
44 43 simp3d 
 |-  ( ( ph /\ a e. S ) -> ( abs ` a ) < R )
45 44 adantr 
 |-  ( ( ( ph /\ a e. S ) /\ R e. RR ) -> ( abs ` a ) < R )
46 17 abscld 
 |-  ( ( ph /\ a e. S ) -> ( abs ` a ) e. RR )
47 avglt1 
 |-  ( ( ( abs ` a ) e. RR /\ R e. RR ) -> ( ( abs ` a ) < R <-> ( abs ` a ) < ( ( ( abs ` a ) + R ) / 2 ) ) )
48 46 47 sylan 
 |-  ( ( ( ph /\ a e. S ) /\ R e. RR ) -> ( ( abs ` a ) < R <-> ( abs ` a ) < ( ( ( abs ` a ) + R ) / 2 ) ) )
49 45 48 mpbid 
 |-  ( ( ( ph /\ a e. S ) /\ R e. RR ) -> ( abs ` a ) < ( ( ( abs ` a ) + R ) / 2 ) )
50 46 ltp1d 
 |-  ( ( ph /\ a e. S ) -> ( abs ` a ) < ( ( abs ` a ) + 1 ) )
51 50 adantr 
 |-  ( ( ( ph /\ a e. S ) /\ -. R e. RR ) -> ( abs ` a ) < ( ( abs ` a ) + 1 ) )
52 27 28 49 51 ifbothda 
 |-  ( ( ph /\ a e. S ) -> ( abs ` a ) < if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) ) )
53 52 6 breqtrrdi 
 |-  ( ( ph /\ a e. S ) -> ( abs ` a ) < M )
54 26 53 eqbrtrd 
 |-  ( ( ph /\ a e. S ) -> ( 0 ( abs o. - ) a ) < M )
55 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
56 1 2 3 4 5 6 psercnlem1 
 |-  ( ( ph /\ a e. S ) -> ( M e. RR+ /\ ( abs ` a ) < M /\ M < R ) )
57 56 simp1d 
 |-  ( ( ph /\ a e. S ) -> M e. RR+ )
58 57 rpxrd 
 |-  ( ( ph /\ a e. S ) -> M e. RR* )
59 elbl 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ M e. RR* ) -> ( a e. ( 0 ( ball ` ( abs o. - ) ) M ) <-> ( a e. CC /\ ( 0 ( abs o. - ) a ) < M ) ) )
60 55 18 58 59 mp3an12i 
 |-  ( ( ph /\ a e. S ) -> ( a e. ( 0 ( ball ` ( abs o. - ) ) M ) <-> ( a e. CC /\ ( 0 ( abs o. - ) a ) < M ) ) )
61 17 54 60 mpbir2and 
 |-  ( ( ph /\ a e. S ) -> a e. ( 0 ( ball ` ( abs o. - ) ) M ) )
62 61 fvresd 
 |-  ( ( ph /\ a e. S ) -> ( ( F |` ( 0 ( ball ` ( abs o. - ) ) M ) ) ` a ) = ( F ` a ) )
63 2 reseq1i 
 |-  ( F |` ( 0 ( ball ` ( abs o. - ) ) M ) ) = ( ( y e. S |-> sum_ j e. NN0 ( ( G ` y ) ` j ) ) |` ( 0 ( ball ` ( abs o. - ) ) M ) )
64 1 2 3 4 5 56 psercnlem2 
 |-  ( ( ph /\ a e. S ) -> ( a e. ( 0 ( ball ` ( abs o. - ) ) M ) /\ ( 0 ( ball ` ( abs o. - ) ) M ) C_ ( `' abs " ( 0 [,] M ) ) /\ ( `' abs " ( 0 [,] M ) ) C_ S ) )
65 64 simp2d 
 |-  ( ( ph /\ a e. S ) -> ( 0 ( ball ` ( abs o. - ) ) M ) C_ ( `' abs " ( 0 [,] M ) ) )
66 64 simp3d 
 |-  ( ( ph /\ a e. S ) -> ( `' abs " ( 0 [,] M ) ) C_ S )
67 65 66 sstrd 
 |-  ( ( ph /\ a e. S ) -> ( 0 ( ball ` ( abs o. - ) ) M ) C_ S )
68 67 resmptd 
 |-  ( ( ph /\ a e. S ) -> ( ( y e. S |-> sum_ j e. NN0 ( ( G ` y ) ` j ) ) |` ( 0 ( ball ` ( abs o. - ) ) M ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) M ) |-> sum_ j e. NN0 ( ( G ` y ) ` j ) ) )
69 63 68 syl5eq 
 |-  ( ( ph /\ a e. S ) -> ( F |` ( 0 ( ball ` ( abs o. - ) ) M ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) M ) |-> sum_ j e. NN0 ( ( G ` y ) ` j ) ) )
70 eqid 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) M ) |-> sum_ j e. NN0 ( ( G ` y ) ` j ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) M ) |-> sum_ j e. NN0 ( ( G ` y ) ` j ) )
71 3 adantr 
 |-  ( ( ph /\ a e. S ) -> A : NN0 --> CC )
72 fveq2 
 |-  ( k = y -> ( G ` k ) = ( G ` y ) )
73 72 seqeq3d 
 |-  ( k = y -> seq 0 ( + , ( G ` k ) ) = seq 0 ( + , ( G ` y ) ) )
74 73 fveq1d 
 |-  ( k = y -> ( seq 0 ( + , ( G ` k ) ) ` s ) = ( seq 0 ( + , ( G ` y ) ) ` s ) )
75 74 cbvmptv 
 |-  ( k e. ( 0 ( ball ` ( abs o. - ) ) M ) |-> ( seq 0 ( + , ( G ` k ) ) ` s ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) M ) |-> ( seq 0 ( + , ( G ` y ) ) ` s ) )
76 fveq2 
 |-  ( s = i -> ( seq 0 ( + , ( G ` y ) ) ` s ) = ( seq 0 ( + , ( G ` y ) ) ` i ) )
77 76 mpteq2dv 
 |-  ( s = i -> ( y e. ( 0 ( ball ` ( abs o. - ) ) M ) |-> ( seq 0 ( + , ( G ` y ) ) ` s ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) M ) |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) )
78 75 77 syl5eq 
 |-  ( s = i -> ( k e. ( 0 ( ball ` ( abs o. - ) ) M ) |-> ( seq 0 ( + , ( G ` k ) ) ` s ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) M ) |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) )
79 78 cbvmptv 
 |-  ( s e. NN0 |-> ( k e. ( 0 ( ball ` ( abs o. - ) ) M ) |-> ( seq 0 ( + , ( G ` k ) ) ` s ) ) ) = ( i e. NN0 |-> ( y e. ( 0 ( ball ` ( abs o. - ) ) M ) |-> ( seq 0 ( + , ( G ` y ) ) ` i ) ) )
80 57 rpred 
 |-  ( ( ph /\ a e. S ) -> M e. RR )
81 56 simp3d 
 |-  ( ( ph /\ a e. S ) -> M < R )
82 1 70 71 4 79 80 81 65 psercn2 
 |-  ( ( ph /\ a e. S ) -> ( y e. ( 0 ( ball ` ( abs o. - ) ) M ) |-> sum_ j e. NN0 ( ( G ` y ) ` j ) ) e. ( ( 0 ( ball ` ( abs o. - ) ) M ) -cn-> CC ) )
83 69 82 eqeltrd 
 |-  ( ( ph /\ a e. S ) -> ( F |` ( 0 ( ball ` ( abs o. - ) ) M ) ) e. ( ( 0 ( ball ` ( abs o. - ) ) M ) -cn-> CC ) )
84 cncff 
 |-  ( ( F |` ( 0 ( ball ` ( abs o. - ) ) M ) ) e. ( ( 0 ( ball ` ( abs o. - ) ) M ) -cn-> CC ) -> ( F |` ( 0 ( ball ` ( abs o. - ) ) M ) ) : ( 0 ( ball ` ( abs o. - ) ) M ) --> CC )
85 83 84 syl 
 |-  ( ( ph /\ a e. S ) -> ( F |` ( 0 ( ball ` ( abs o. - ) ) M ) ) : ( 0 ( ball ` ( abs o. - ) ) M ) --> CC )
86 85 61 ffvelrnd 
 |-  ( ( ph /\ a e. S ) -> ( ( F |` ( 0 ( ball ` ( abs o. - ) ) M ) ) ` a ) e. CC )
87 62 86 eqeltrrd 
 |-  ( ( ph /\ a e. S ) -> ( F ` a ) e. CC )
88 87 ralrimiva 
 |-  ( ph -> A. a e. S ( F ` a ) e. CC )
89 ffnfv 
 |-  ( F : S --> CC <-> ( F Fn S /\ A. a e. S ( F ` a ) e. CC ) )
90 10 88 89 sylanbrc 
 |-  ( ph -> F : S --> CC )
91 67 15 sstrdi 
 |-  ( ( ph /\ a e. S ) -> ( 0 ( ball ` ( abs o. - ) ) M ) C_ CC )
92 ssid 
 |-  CC C_ CC
93 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
94 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) = ( ( TopOpen ` CCfld ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) )
95 93 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
96 95 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
97 93 94 96 cncfcn 
 |-  ( ( ( 0 ( ball ` ( abs o. - ) ) M ) C_ CC /\ CC C_ CC ) -> ( ( 0 ( ball ` ( abs o. - ) ) M ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) Cn ( TopOpen ` CCfld ) ) )
98 91 92 97 sylancl 
 |-  ( ( ph /\ a e. S ) -> ( ( 0 ( ball ` ( abs o. - ) ) M ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) Cn ( TopOpen ` CCfld ) ) )
99 83 98 eleqtrd 
 |-  ( ( ph /\ a e. S ) -> ( F |` ( 0 ( ball ` ( abs o. - ) ) M ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) Cn ( TopOpen ` CCfld ) ) )
100 93 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
101 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
102 101 restuni 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( 0 ( ball ` ( abs o. - ) ) M ) C_ CC ) -> ( 0 ( ball ` ( abs o. - ) ) M ) = U. ( ( TopOpen ` CCfld ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) )
103 100 91 102 sylancr 
 |-  ( ( ph /\ a e. S ) -> ( 0 ( ball ` ( abs o. - ) ) M ) = U. ( ( TopOpen ` CCfld ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) )
104 61 103 eleqtrd 
 |-  ( ( ph /\ a e. S ) -> a e. U. ( ( TopOpen ` CCfld ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) )
105 eqid 
 |-  U. ( ( TopOpen ` CCfld ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) = U. ( ( TopOpen ` CCfld ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) )
106 105 cncnpi 
 |-  ( ( ( F |` ( 0 ( ball ` ( abs o. - ) ) M ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) Cn ( TopOpen ` CCfld ) ) /\ a e. U. ( ( TopOpen ` CCfld ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) ) -> ( F |` ( 0 ( ball ` ( abs o. - ) ) M ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) CnP ( TopOpen ` CCfld ) ) ` a ) )
107 99 104 106 syl2anc 
 |-  ( ( ph /\ a e. S ) -> ( F |` ( 0 ( ball ` ( abs o. - ) ) M ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) CnP ( TopOpen ` CCfld ) ) ` a ) )
108 cnex 
 |-  CC e. _V
109 108 15 ssexi 
 |-  S e. _V
110 109 a1i 
 |-  ( ( ph /\ a e. S ) -> S e. _V )
111 restabs 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( 0 ( ball ` ( abs o. - ) ) M ) C_ S /\ S e. _V ) -> ( ( ( TopOpen ` CCfld ) |`t S ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) = ( ( TopOpen ` CCfld ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) )
112 100 67 110 111 mp3an2i 
 |-  ( ( ph /\ a e. S ) -> ( ( ( TopOpen ` CCfld ) |`t S ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) = ( ( TopOpen ` CCfld ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) )
113 112 oveq1d 
 |-  ( ( ph /\ a e. S ) -> ( ( ( ( TopOpen ` CCfld ) |`t S ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) CnP ( TopOpen ` CCfld ) ) = ( ( ( TopOpen ` CCfld ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) CnP ( TopOpen ` CCfld ) ) )
114 113 fveq1d 
 |-  ( ( ph /\ a e. S ) -> ( ( ( ( ( TopOpen ` CCfld ) |`t S ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) CnP ( TopOpen ` CCfld ) ) ` a ) = ( ( ( ( TopOpen ` CCfld ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) CnP ( TopOpen ` CCfld ) ) ` a ) )
115 107 114 eleqtrrd 
 |-  ( ( ph /\ a e. S ) -> ( F |` ( 0 ( ball ` ( abs o. - ) ) M ) ) e. ( ( ( ( ( TopOpen ` CCfld ) |`t S ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) CnP ( TopOpen ` CCfld ) ) ` a ) )
116 resttop 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ S e. _V ) -> ( ( TopOpen ` CCfld ) |`t S ) e. Top )
117 100 109 116 mp2an 
 |-  ( ( TopOpen ` CCfld ) |`t S ) e. Top
118 117 a1i 
 |-  ( ( ph /\ a e. S ) -> ( ( TopOpen ` CCfld ) |`t S ) e. Top )
119 df-ss 
 |-  ( ( 0 ( ball ` ( abs o. - ) ) M ) C_ S <-> ( ( 0 ( ball ` ( abs o. - ) ) M ) i^i S ) = ( 0 ( ball ` ( abs o. - ) ) M ) )
120 67 119 sylib 
 |-  ( ( ph /\ a e. S ) -> ( ( 0 ( ball ` ( abs o. - ) ) M ) i^i S ) = ( 0 ( ball ` ( abs o. - ) ) M ) )
121 93 cnfldtopn 
 |-  ( TopOpen ` CCfld ) = ( MetOpen ` ( abs o. - ) )
122 121 blopn 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ M e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) M ) e. ( TopOpen ` CCfld ) )
123 55 18 58 122 mp3an12i 
 |-  ( ( ph /\ a e. S ) -> ( 0 ( ball ` ( abs o. - ) ) M ) e. ( TopOpen ` CCfld ) )
124 elrestr 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ S e. _V /\ ( 0 ( ball ` ( abs o. - ) ) M ) e. ( TopOpen ` CCfld ) ) -> ( ( 0 ( ball ` ( abs o. - ) ) M ) i^i S ) e. ( ( TopOpen ` CCfld ) |`t S ) )
125 100 109 123 124 mp3an12i 
 |-  ( ( ph /\ a e. S ) -> ( ( 0 ( ball ` ( abs o. - ) ) M ) i^i S ) e. ( ( TopOpen ` CCfld ) |`t S ) )
126 120 125 eqeltrrd 
 |-  ( ( ph /\ a e. S ) -> ( 0 ( ball ` ( abs o. - ) ) M ) e. ( ( TopOpen ` CCfld ) |`t S ) )
127 isopn3i 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t S ) e. Top /\ ( 0 ( ball ` ( abs o. - ) ) M ) e. ( ( TopOpen ` CCfld ) |`t S ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` ( 0 ( ball ` ( abs o. - ) ) M ) ) = ( 0 ( ball ` ( abs o. - ) ) M ) )
128 117 126 127 sylancr 
 |-  ( ( ph /\ a e. S ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` ( 0 ( ball ` ( abs o. - ) ) M ) ) = ( 0 ( ball ` ( abs o. - ) ) M ) )
129 61 128 eleqtrrd 
 |-  ( ( ph /\ a e. S ) -> a e. ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` ( 0 ( ball ` ( abs o. - ) ) M ) ) )
130 90 adantr 
 |-  ( ( ph /\ a e. S ) -> F : S --> CC )
131 101 restuni 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ S C_ CC ) -> S = U. ( ( TopOpen ` CCfld ) |`t S ) )
132 100 15 131 mp2an 
 |-  S = U. ( ( TopOpen ` CCfld ) |`t S )
133 132 101 cnprest 
 |-  ( ( ( ( ( TopOpen ` CCfld ) |`t S ) e. Top /\ ( 0 ( ball ` ( abs o. - ) ) M ) C_ S ) /\ ( a e. ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` ( 0 ( ball ` ( abs o. - ) ) M ) ) /\ F : S --> CC ) ) -> ( F e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` a ) <-> ( F |` ( 0 ( ball ` ( abs o. - ) ) M ) ) e. ( ( ( ( ( TopOpen ` CCfld ) |`t S ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) CnP ( TopOpen ` CCfld ) ) ` a ) ) )
134 118 67 129 130 133 syl22anc 
 |-  ( ( ph /\ a e. S ) -> ( F e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` a ) <-> ( F |` ( 0 ( ball ` ( abs o. - ) ) M ) ) e. ( ( ( ( ( TopOpen ` CCfld ) |`t S ) |`t ( 0 ( ball ` ( abs o. - ) ) M ) ) CnP ( TopOpen ` CCfld ) ) ` a ) ) )
135 115 134 mpbird 
 |-  ( ( ph /\ a e. S ) -> F e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` a ) )
136 135 ralrimiva 
 |-  ( ph -> A. a e. S F e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` a ) )
137 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ S C_ CC ) -> ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S ) )
138 95 15 137 mp2an 
 |-  ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S )
139 cncnp 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S ) /\ ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) -> ( F e. ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( TopOpen ` CCfld ) ) <-> ( F : S --> CC /\ A. a e. S F e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` a ) ) ) )
140 138 95 139 mp2an 
 |-  ( F e. ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( TopOpen ` CCfld ) ) <-> ( F : S --> CC /\ A. a e. S F e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` a ) ) )
141 90 136 140 sylanbrc 
 |-  ( ph -> F e. ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( TopOpen ` CCfld ) ) )
142 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t S ) = ( ( TopOpen ` CCfld ) |`t S )
143 93 142 96 cncfcn 
 |-  ( ( S C_ CC /\ CC C_ CC ) -> ( S -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( TopOpen ` CCfld ) ) )
144 15 92 143 mp2an 
 |-  ( S -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( TopOpen ` CCfld ) )
145 141 144 eleqtrrdi 
 |-  ( ph -> F e. ( S -cn-> CC ) )