Metamath Proof Explorer

Theorem perfdvf

Description: The derivative is a function, whenever it is defined relative to a perfect subset of the complex numbers. (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypothesis perfdvf.1 
|- K = ( TopOpen ` CCfld )
Assertion perfdvf 
|- ( ( K |`t S ) e. Perf -> ( S _D F ) : dom ( S _D F ) --> CC )

Proof

Step Hyp Ref Expression
1 perfdvf.1 
 |-  K = ( TopOpen ` CCfld )
2 df-dv 
 |-  _D = ( s e. ~P CC , f e. ( CC ^pm s ) |-> U_ x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom f ) ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) limCC x ) ) )
3 2 dmmpossx 
 |-  dom _D C_ U_ s e. ~P CC ( { s } X. ( CC ^pm s ) )
4 simpl 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> <. S , F >. e. dom _D )
5 3 4 sselid 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> <. S , F >. e. U_ s e. ~P CC ( { s } X. ( CC ^pm s ) ) )
6 oveq2 
 |-  ( s = S -> ( CC ^pm s ) = ( CC ^pm S ) )
7 6 opeliunxp2 
 |-  ( <. S , F >. e. U_ s e. ~P CC ( { s } X. ( CC ^pm s ) ) <-> ( S e. ~P CC /\ F e. ( CC ^pm S ) ) )
8 5 7 sylib 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( S e. ~P CC /\ F e. ( CC ^pm S ) ) )
9 8 simprd 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> F e. ( CC ^pm S ) )
10 cnex 
 |-  CC e. _V
11 8 simpld 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> S e. ~P CC )
12 elpm2g 
 |-  ( ( CC e. _V /\ S e. ~P CC ) -> ( F e. ( CC ^pm S ) <-> ( F : dom F --> CC /\ dom F C_ S ) ) )
13 10 11 12 sylancr 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( F e. ( CC ^pm S ) <-> ( F : dom F --> CC /\ dom F C_ S ) ) )
14 9 13 mpbid 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( F : dom F --> CC /\ dom F C_ S ) )
15 14 simpld 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> F : dom F --> CC )
16 15 adantr 
 |-  ( ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) /\ x e. ( ( int ` ( K |`t S ) ) ` dom F ) ) -> F : dom F --> CC )
17 3 sseli 
 |-  ( <. S , F >. e. dom _D -> <. S , F >. e. U_ s e. ~P CC ( { s } X. ( CC ^pm s ) ) )
18 17 7 sylib 
 |-  ( <. S , F >. e. dom _D -> ( S e. ~P CC /\ F e. ( CC ^pm S ) ) )
19 18 simprd 
 |-  ( <. S , F >. e. dom _D -> F e. ( CC ^pm S ) )
20 18 simpld 
 |-  ( <. S , F >. e. dom _D -> S e. ~P CC )
21 10 20 12 sylancr 
 |-  ( <. S , F >. e. dom _D -> ( F e. ( CC ^pm S ) <-> ( F : dom F --> CC /\ dom F C_ S ) ) )
22 19 21 mpbid 
 |-  ( <. S , F >. e. dom _D -> ( F : dom F --> CC /\ dom F C_ S ) )
23 22 simprd 
 |-  ( <. S , F >. e. dom _D -> dom F C_ S )
24 23 adantr 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> dom F C_ S )
25 11 elpwid 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> S C_ CC )
26 24 25 sstrd 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> dom F C_ CC )
27 26 adantr 
 |-  ( ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) /\ x e. ( ( int ` ( K |`t S ) ) ` dom F ) ) -> dom F C_ CC )
28 1 cnfldtopon 
 |-  K e. ( TopOn ` CC )
29 resttopon 
 |-  ( ( K e. ( TopOn ` CC ) /\ S C_ CC ) -> ( K |`t S ) e. ( TopOn ` S ) )
30 28 25 29 sylancr 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( K |`t S ) e. ( TopOn ` S ) )
31 topontop 
 |-  ( ( K |`t S ) e. ( TopOn ` S ) -> ( K |`t S ) e. Top )
32 30 31 syl 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( K |`t S ) e. Top )
33 toponuni 
 |-  ( ( K |`t S ) e. ( TopOn ` S ) -> S = U. ( K |`t S ) )
34 30 33 syl 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> S = U. ( K |`t S ) )
35 24 34 sseqtrd 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> dom F C_ U. ( K |`t S ) )
36 eqid 
 |-  U. ( K |`t S ) = U. ( K |`t S )
37 36 ntrss2 
 |-  ( ( ( K |`t S ) e. Top /\ dom F C_ U. ( K |`t S ) ) -> ( ( int ` ( K |`t S ) ) ` dom F ) C_ dom F )
38 32 35 37 syl2anc 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( ( int ` ( K |`t S ) ) ` dom F ) C_ dom F )
39 38 sselda 
 |-  ( ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) /\ x e. ( ( int ` ( K |`t S ) ) ` dom F ) ) -> x e. dom F )
40 16 27 39 dvlem 
 |-  ( ( ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) /\ x e. ( ( int ` ( K |`t S ) ) ` dom F ) ) /\ z e. ( dom F \ { x } ) ) -> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) e. CC )
41 40 fmpttd 
 |-  ( ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) /\ x e. ( ( int ` ( K |`t S ) ) ` dom F ) ) -> ( z e. ( dom F \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) : ( dom F \ { x } ) --> CC )
42 27 ssdifssd 
 |-  ( ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) /\ x e. ( ( int ` ( K |`t S ) ) ` dom F ) ) -> ( dom F \ { x } ) C_ CC )
43 36 ntrss3 
 |-  ( ( ( K |`t S ) e. Top /\ dom F C_ U. ( K |`t S ) ) -> ( ( int ` ( K |`t S ) ) ` dom F ) C_ U. ( K |`t S ) )
44 32 35 43 syl2anc 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( ( int ` ( K |`t S ) ) ` dom F ) C_ U. ( K |`t S ) )
45 44 34 sseqtrrd 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( ( int ` ( K |`t S ) ) ` dom F ) C_ S )
46 restabs 
 |-  ( ( K e. ( TopOn ` CC ) /\ ( ( int ` ( K |`t S ) ) ` dom F ) C_ S /\ S e. ~P CC ) -> ( ( K |`t S ) |`t ( ( int ` ( K |`t S ) ) ` dom F ) ) = ( K |`t ( ( int ` ( K |`t S ) ) ` dom F ) ) )
47 28 45 11 46 mp3an2i 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( ( K |`t S ) |`t ( ( int ` ( K |`t S ) ) ` dom F ) ) = ( K |`t ( ( int ` ( K |`t S ) ) ` dom F ) ) )
48 simpr 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( K |`t S ) e. Perf )
49 36 ntropn 
 |-  ( ( ( K |`t S ) e. Top /\ dom F C_ U. ( K |`t S ) ) -> ( ( int ` ( K |`t S ) ) ` dom F ) e. ( K |`t S ) )
50 32 35 49 syl2anc 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( ( int ` ( K |`t S ) ) ` dom F ) e. ( K |`t S ) )
51 eqid 
 |-  ( ( K |`t S ) |`t ( ( int ` ( K |`t S ) ) ` dom F ) ) = ( ( K |`t S ) |`t ( ( int ` ( K |`t S ) ) ` dom F ) )
52 36 51 perfopn 
 |-  ( ( ( K |`t S ) e. Perf /\ ( ( int ` ( K |`t S ) ) ` dom F ) e. ( K |`t S ) ) -> ( ( K |`t S ) |`t ( ( int ` ( K |`t S ) ) ` dom F ) ) e. Perf )
53 48 50 52 syl2anc 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( ( K |`t S ) |`t ( ( int ` ( K |`t S ) ) ` dom F ) ) e. Perf )
54 47 53 eqeltrrd 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( K |`t ( ( int ` ( K |`t S ) ) ` dom F ) ) e. Perf )
55 1 cnfldtop 
 |-  K e. Top
56 45 25 sstrd 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( ( int ` ( K |`t S ) ) ` dom F ) C_ CC )
57 28 toponunii 
 |-  CC = U. K
58 eqid 
 |-  ( K |`t ( ( int ` ( K |`t S ) ) ` dom F ) ) = ( K |`t ( ( int ` ( K |`t S ) ) ` dom F ) )
59 57 58 restperf 
 |-  ( ( K e. Top /\ ( ( int ` ( K |`t S ) ) ` dom F ) C_ CC ) -> ( ( K |`t ( ( int ` ( K |`t S ) ) ` dom F ) ) e. Perf <-> ( ( int ` ( K |`t S ) ) ` dom F ) C_ ( ( limPt ` K ) ` ( ( int ` ( K |`t S ) ) ` dom F ) ) ) )
60 55 56 59 sylancr 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( ( K |`t ( ( int ` ( K |`t S ) ) ` dom F ) ) e. Perf <-> ( ( int ` ( K |`t S ) ) ` dom F ) C_ ( ( limPt ` K ) ` ( ( int ` ( K |`t S ) ) ` dom F ) ) ) )
61 54 60 mpbid 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( ( int ` ( K |`t S ) ) ` dom F ) C_ ( ( limPt ` K ) ` ( ( int ` ( K |`t S ) ) ` dom F ) ) )
62 57 lpss3 
 |-  ( ( K e. Top /\ dom F C_ CC /\ ( ( int ` ( K |`t S ) ) ` dom F ) C_ dom F ) -> ( ( limPt ` K ) ` ( ( int ` ( K |`t S ) ) ` dom F ) ) C_ ( ( limPt ` K ) ` dom F ) )
63 55 26 38 62 mp3an2i 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( ( limPt ` K ) ` ( ( int ` ( K |`t S ) ) ` dom F ) ) C_ ( ( limPt ` K ) ` dom F ) )
64 61 63 sstrd 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( ( int ` ( K |`t S ) ) ` dom F ) C_ ( ( limPt ` K ) ` dom F ) )
65 64 sselda 
 |-  ( ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) /\ x e. ( ( int ` ( K |`t S ) ) ` dom F ) ) -> x e. ( ( limPt ` K ) ` dom F ) )
66 57 lpdifsn 
 |-  ( ( K e. Top /\ dom F C_ CC ) -> ( x e. ( ( limPt ` K ) ` dom F ) <-> x e. ( ( limPt ` K ) ` ( dom F \ { x } ) ) ) )
67 55 27 66 sylancr 
 |-  ( ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) /\ x e. ( ( int ` ( K |`t S ) ) ` dom F ) ) -> ( x e. ( ( limPt ` K ) ` dom F ) <-> x e. ( ( limPt ` K ) ` ( dom F \ { x } ) ) ) )
68 65 67 mpbid 
 |-  ( ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) /\ x e. ( ( int ` ( K |`t S ) ) ` dom F ) ) -> x e. ( ( limPt ` K ) ` ( dom F \ { x } ) ) )
69 41 42 68 1 limcmo 
 |-  ( ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) /\ x e. ( ( int ` ( K |`t S ) ) ` dom F ) ) -> E* y y e. ( ( z e. ( dom F \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) )
70 69 ex 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( x e. ( ( int ` ( K |`t S ) ) ` dom F ) -> E* y y e. ( ( z e. ( dom F \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) )
71 moanimv 
 |-  ( E* y ( x e. ( ( int ` ( K |`t S ) ) ` dom F ) /\ y e. ( ( z e. ( dom F \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) <-> ( x e. ( ( int ` ( K |`t S ) ) ` dom F ) -> E* y y e. ( ( z e. ( dom F \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) )
72 70 71 sylibr 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> E* y ( x e. ( ( int ` ( K |`t S ) ) ` dom F ) /\ y e. ( ( z e. ( dom F \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) )
73 eqid 
 |-  ( K |`t S ) = ( K |`t S )
74 eqid 
 |-  ( z e. ( dom F \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) = ( z e. ( dom F \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) )
75 73 1 74 25 15 24 eldv 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( x ( S _D F ) y <-> ( x e. ( ( int ` ( K |`t S ) ) ` dom F ) /\ y e. ( ( z e. ( dom F \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) ) )
76 75 mobidv 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( E* y x ( S _D F ) y <-> E* y ( x e. ( ( int ` ( K |`t S ) ) ` dom F ) /\ y e. ( ( z e. ( dom F \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) ) )
77 72 76 mpbird 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> E* y x ( S _D F ) y )
78 77 alrimiv 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> A. x E* y x ( S _D F ) y )
79 reldv 
 |-  Rel ( S _D F )
80 dffun6 
 |-  ( Fun ( S _D F ) <-> ( Rel ( S _D F ) /\ A. x E* y x ( S _D F ) y ) )
81 79 80 mpbiran 
 |-  ( Fun ( S _D F ) <-> A. x E* y x ( S _D F ) y )
82 78 81 sylibr 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> Fun ( S _D F ) )
83 82 funfnd 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( S _D F ) Fn dom ( S _D F ) )
84 vex 
 |-  y e. _V
85 84 elrn 
 |-  ( y e. ran ( S _D F ) <-> E. x x ( S _D F ) y )
86 25 15 24 dvcl 
 |-  ( ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) /\ x ( S _D F ) y ) -> y e. CC )
87 86 ex 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( x ( S _D F ) y -> y e. CC ) )
88 87 exlimdv 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( E. x x ( S _D F ) y -> y e. CC ) )
89 85 88 biimtrid 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( y e. ran ( S _D F ) -> y e. CC ) )
90 89 ssrdv 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ran ( S _D F ) C_ CC )
91 df-f 
 |-  ( ( S _D F ) : dom ( S _D F ) --> CC <-> ( ( S _D F ) Fn dom ( S _D F ) /\ ran ( S _D F ) C_ CC ) )
92 83 90 91 sylanbrc 
 |-  ( ( <. S , F >. e. dom _D /\ ( K |`t S ) e. Perf ) -> ( S _D F ) : dom ( S _D F ) --> CC )
93 92 ex 
 |-  ( <. S , F >. e. dom _D -> ( ( K |`t S ) e. Perf -> ( S _D F ) : dom ( S _D F ) --> CC ) )
94 f0 
 |-  (/) : (/) --> CC
95 df-ov 
 |-  ( S _D F ) = ( _D ` <. S , F >. )
96 ndmfv 
 |-  ( -. <. S , F >. e. dom _D -> ( _D ` <. S , F >. ) = (/) )
97 95 96 eqtrid 
 |-  ( -. <. S , F >. e. dom _D -> ( S _D F ) = (/) )
98 97 dmeqd 
 |-  ( -. <. S , F >. e. dom _D -> dom ( S _D F ) = dom (/) )
99 dm0 
 |-  dom (/) = (/)
100 98 99 eqtrdi 
 |-  ( -. <. S , F >. e. dom _D -> dom ( S _D F ) = (/) )
101 97 100 feq12d 
 |-  ( -. <. S , F >. e. dom _D -> ( ( S _D F ) : dom ( S _D F ) --> CC <-> (/) : (/) --> CC ) )
102 94 101 mpbiri 
 |-  ( -. <. S , F >. e. dom _D -> ( S _D F ) : dom ( S _D F ) --> CC )
103 102 a1d 
 |-  ( -. <. S , F >. e. dom _D -> ( ( K |`t S ) e. Perf -> ( S _D F ) : dom ( S _D F ) --> CC ) )
104 93 103 pm2.61i 
 |-  ( ( K |`t S ) e. Perf -> ( S _D F ) : dom ( S _D F ) --> CC )