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