Metamath Proof Explorer

Theorem dvfval

Description: Value and set bounds on the derivative operator. (Contributed by Mario Carneiro, 7-Aug-2014) (Revised by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses dvval.t 
|- T = ( K |`t S )
dvval.k 
|- K = ( TopOpen ` CCfld )
Assertion dvfval 
|- ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> ( ( S _D F ) = U_ x e. ( ( int ` T ) ` A ) ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) /\ ( S _D F ) C_ ( ( ( int ` T ) ` A ) X. CC ) ) )

Proof

Step Hyp Ref Expression
1 dvval.t 
 |-  T = ( K |`t S )
2 dvval.k 
 |-  K = ( TopOpen ` CCfld )
3 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 ) ) )
4 3 a1i 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> _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 ) ) ) )
5 2 oveq1i 
 |-  ( K |`t s ) = ( ( TopOpen ` CCfld ) |`t s )
6 simprl 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ ( s = S /\ f = F ) ) -> s = S )
7 6 oveq2d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ ( s = S /\ f = F ) ) -> ( K |`t s ) = ( K |`t S ) )
8 7 1 eqtr4di 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ ( s = S /\ f = F ) ) -> ( K |`t s ) = T )
9 5 8 eqtr3id 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ ( s = S /\ f = F ) ) -> ( ( TopOpen ` CCfld ) |`t s ) = T )
10 9 fveq2d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ ( s = S /\ f = F ) ) -> ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) = ( int ` T ) )
11 simprr 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ ( s = S /\ f = F ) ) -> f = F )
12 11 dmeqd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ ( s = S /\ f = F ) ) -> dom f = dom F )
13 simpl2 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ ( s = S /\ f = F ) ) -> F : A --> CC )
14 13 fdmd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ ( s = S /\ f = F ) ) -> dom F = A )
15 12 14 eqtrd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ ( s = S /\ f = F ) ) -> dom f = A )
16 10 15 fveq12d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ ( s = S /\ f = F ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom f ) = ( ( int ` T ) ` A ) )
17 15 difeq1d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ ( s = S /\ f = F ) ) -> ( dom f \ { x } ) = ( A \ { x } ) )
18 11 fveq1d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ ( s = S /\ f = F ) ) -> ( f ` z ) = ( F ` z ) )
19 11 fveq1d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ ( s = S /\ f = F ) ) -> ( f ` x ) = ( F ` x ) )
20 18 19 oveq12d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ ( s = S /\ f = F ) ) -> ( ( f ` z ) - ( f ` x ) ) = ( ( F ` z ) - ( F ` x ) ) )
21 20 oveq1d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ ( s = S /\ f = F ) ) -> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) = ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) )
22 17 21 mpteq12dv 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ ( s = S /\ f = F ) ) -> ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) = ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) )
23 22 oveq1d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ ( s = S /\ f = F ) ) -> ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) limCC x ) = ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) )
24 23 xpeq2d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ ( s = S /\ f = F ) ) -> ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) limCC x ) ) = ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) )
25 16 24 iuneq12d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ ( s = S /\ f = F ) ) -> 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 ) ) = U_ x e. ( ( int ` T ) ` A ) ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) )
26 simpr 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ s = S ) -> s = S )
27 26 oveq2d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ s = S ) -> ( CC ^pm s ) = ( CC ^pm S ) )
28 simp1 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> S C_ CC )
29 cnex 
 |-  CC e. _V
30 29 elpw2 
 |-  ( S e. ~P CC <-> S C_ CC )
31 28 30 sylibr 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> S e. ~P CC )
32 29 a1i 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> CC e. _V )
33 simp2 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> F : A --> CC )
34 simp3 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> A C_ S )
35 elpm2r 
 |-  ( ( ( CC e. _V /\ S e. ~P CC ) /\ ( F : A --> CC /\ A C_ S ) ) -> F e. ( CC ^pm S ) )
36 32 31 33 34 35 syl22anc 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> F e. ( CC ^pm S ) )
37 limccl 
 |-  ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) C_ CC
38 xpss2 
 |-  ( ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) C_ CC -> ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) C_ ( { x } X. CC ) )
39 37 38 ax-mp 
 |-  ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) C_ ( { x } X. CC )
40 39 rgenw 
 |-  A. x e. ( ( int ` T ) ` A ) ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) C_ ( { x } X. CC )
41 ss2iun 
 |-  ( A. x e. ( ( int ` T ) ` A ) ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) C_ ( { x } X. CC ) -> U_ x e. ( ( int ` T ) ` A ) ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) C_ U_ x e. ( ( int ` T ) ` A ) ( { x } X. CC ) )
42 40 41 ax-mp 
 |-  U_ x e. ( ( int ` T ) ` A ) ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) C_ U_ x e. ( ( int ` T ) ` A ) ( { x } X. CC )
43 iunxpconst 
 |-  U_ x e. ( ( int ` T ) ` A ) ( { x } X. CC ) = ( ( ( int ` T ) ` A ) X. CC )
44 42 43 sseqtri 
 |-  U_ x e. ( ( int ` T ) ` A ) ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) C_ ( ( ( int ` T ) ` A ) X. CC )
45 44 a1i 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> U_ x e. ( ( int ` T ) ` A ) ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) C_ ( ( ( int ` T ) ` A ) X. CC ) )
46 fvex 
 |-  ( ( int ` T ) ` A ) e. _V
47 46 29 xpex 
 |-  ( ( ( int ` T ) ` A ) X. CC ) e. _V
48 47 ssex 
 |-  ( U_ x e. ( ( int ` T ) ` A ) ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) C_ ( ( ( int ` T ) ` A ) X. CC ) -> U_ x e. ( ( int ` T ) ` A ) ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) e. _V )
49 45 48 syl 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> U_ x e. ( ( int ` T ) ` A ) ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) e. _V )
50 4 25 27 31 36 49 ovmpodx 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> ( S _D F ) = U_ x e. ( ( int ` T ) ` A ) ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) )
51 50 45 eqsstrd 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> ( S _D F ) C_ ( ( ( int ` T ) ` A ) X. CC ) )
52 50 51 jca 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> ( ( S _D F ) = U_ x e. ( ( int ` T ) ` A ) ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) /\ ( S _D F ) C_ ( ( ( int ` T ) ` A ) X. CC ) ) )