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=TopOpenfld
dvres.t T=K𝑡S
Assertion dvres SF:AASBSSDFB=FSintTB

Proof

Step Hyp Ref Expression
1 dvres.k K=TopOpenfld
2 dvres.t T=K𝑡S
3 reldv RelFBS
4 relres RelFSintTB
5 simpll SF:AASBSS
6 simplr SF:AASBSF:A
7 inss1 ABA
8 fssres F:AABAFAB:AB
9 6 7 8 sylancl SF:AASBSFAB:AB
10 resres FAB=FAB
11 ffn F:AFFnA
12 fnresdm FFnAFA=F
13 6 11 12 3syl SF:AASBSFA=F
14 13 reseq1d SF:AASBSFAB=FB
15 10 14 eqtr3id SF:AASBSFAB=FB
16 15 feq1d SF:AASBSFAB:ABFB:AB
17 9 16 mpbid SF:AASBSFB:AB
18 simprl SF:AASBSAS
19 7 18 sstrid SF:AASBSABS
20 5 17 19 dvcl SF:AASBSxFBSyy
21 20 ex SF:AASBSxFBSyy
22 5 6 18 dvcl SF:AASBSxFSyy
23 22 ex SF:AASBSxFSyy
24 23 adantld SF:AASBSxintTBxFSyy
25 eqid zAxFzFxzx=zAxFzFxzx
26 5 adantr SF:AASBSyS
27 6 adantr SF:AASBSyF:A
28 18 adantr SF:AASBSyAS
29 simplrr SF:AASBSyBS
30 simpr SF:AASBSyy
31 1 2 25 26 27 28 29 30 dvreslem SF:AASBSyxFBSyxintTBxFSy
32 31 ex SF:AASBSyxFBSyxintTBxFSy
33 21 24 32 pm5.21ndd SF:AASBSxFBSyxintTBxFSy
34 vex yV
35 34 brresi xFSintTByxintTBxFSy
36 33 35 bitr4di SF:AASBSxFBSyxFSintTBy
37 3 4 36 eqbrrdiv SF:AASBSSDFB=FSintTB