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 eqtrid
 |-  ( ( 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 eqtrid
 |-  ( 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 ) )