Metamath Proof Explorer

Theorem dvres

Description: Restriction of a derivative. Note that our definition of derivative df-dv would still make sense if we demanded that x be an element of the domain instead of an interior point of the domain, but then it is possible for a non-differentiable function to have two different derivatives at a single point x when restricted to different subsets containing x ; a classic example is the absolute value function restricted to [ 0 , +oo ) and ( -oo , 0 ] . (Contributed by Mario Carneiro, 8-Aug-2014) (Revised by Mario Carneiro, 9-Feb-2015)

Ref Expression
Hypotheses dvres.k 
|- K = ( TopOpen ` CCfld )
dvres.t 
|- T = ( K |`t S )
Assertion dvres 
|- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( S _D ( F |` B ) ) = ( ( S _D F ) |` ( ( int ` T ) ` B ) ) )

Proof

Step Hyp Ref Expression
1 dvres.k 
 |-  K = ( TopOpen ` CCfld )
2 dvres.t 
 |-  T = ( K |`t S )
3 reldv 
 |-  Rel ( S _D ( F |` B ) )
4 relres 
 |-  Rel ( ( S _D F ) |` ( ( int ` T ) ` B ) )
5 simpll 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> S C_ CC )
6 simplr 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> F : A --> CC )
7 inss1 
 |-  ( A i^i B ) C_ A
8 fssres 
 |-  ( ( F : A --> CC /\ ( A i^i B ) C_ A ) -> ( F |` ( A i^i B ) ) : ( A i^i B ) --> CC )
9 6 7 8 sylancl 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( F |` ( A i^i B ) ) : ( A i^i B ) --> CC )
10 resres 
 |-  ( ( F |` A ) |` B ) = ( F |` ( A i^i B ) )
11 ffn 
 |-  ( F : A --> CC -> F Fn A )
12 fnresdm 
 |-  ( F Fn A -> ( F |` A ) = F )
13 6 11 12 3syl 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( F |` A ) = F )
14 13 reseq1d 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( ( F |` A ) |` B ) = ( F |` B ) )
15 10 14 eqtr3id 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( F |` ( A i^i B ) ) = ( F |` B ) )
16 15 feq1d 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( ( F |` ( A i^i B ) ) : ( A i^i B ) --> CC <-> ( F |` B ) : ( A i^i B ) --> CC ) )
17 9 16 mpbid 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( F |` B ) : ( A i^i B ) --> CC )
18 simprl 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> A C_ S )
19 7 18 sstrid 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( A i^i B ) C_ S )
20 5 17 19 dvcl 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) /\ x ( S _D ( F |` B ) ) y ) -> y e. CC )
21 20 ex 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( x ( S _D ( F |` B ) ) y -> y e. CC ) )
22 5 6 18 dvcl 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) /\ x ( S _D F ) y ) -> y e. CC )
23 22 ex 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( x ( S _D F ) y -> y e. CC ) )
24 23 adantld 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( ( x e. ( ( int ` T ) ` B ) /\ x ( S _D F ) y ) -> y e. CC ) )
25 eqid 
 |-  ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) = ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) )
26 5 adantr 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) /\ y e. CC ) -> S C_ CC )
27 6 adantr 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) /\ y e. CC ) -> F : A --> CC )
28 18 adantr 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) /\ y e. CC ) -> A C_ S )
29 simplrr 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) /\ y e. CC ) -> B C_ S )
30 simpr 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) /\ y e. CC ) -> y e. CC )
31 1 2 25 26 27 28 29 30 dvreslem 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) /\ y e. CC ) -> ( x ( S _D ( F |` B ) ) y <-> ( x e. ( ( int ` T ) ` B ) /\ x ( S _D F ) y ) ) )
32 31 ex 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( y e. CC -> ( x ( S _D ( F |` B ) ) y <-> ( x e. ( ( int ` T ) ` B ) /\ x ( S _D F ) y ) ) ) )
33 21 24 32 pm5.21ndd 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( x ( S _D ( F |` B ) ) y <-> ( x e. ( ( int ` T ) ` B ) /\ x ( S _D F ) y ) ) )
34 vex 
 |-  y e. _V
35 34 brresi 
 |-  ( x ( ( S _D F ) |` ( ( int ` T ) ` B ) ) y <-> ( x e. ( ( int ` T ) ` B ) /\ x ( S _D F ) y ) )
36 33 35 bitr4di 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( x ( S _D ( F |` B ) ) y <-> x ( ( S _D F ) |` ( ( int ` T ) ` B ) ) y ) )
37 3 4 36 eqbrrdiv 
 |-  ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( S _D ( F |` B ) ) = ( ( S _D F ) |` ( ( int ` T ) ` B ) ) )