Metamath Proof Explorer

Theorem dvresntr

Description: Function-builder for derivative: expand the function from an open set to its closure. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dvresntr.s 
|- ( ph -> S C_ CC )
dvresntr.x 
|- ( ph -> X C_ S )
dvresntr.f 
|- ( ph -> F : X --> CC )
dvresntr.j 
|- J = ( K |`t S )
dvresntr.k 
|- K = ( TopOpen ` CCfld )
dvresntr.i 
|- ( ph -> ( ( int ` J ) ` X ) = Y )
Assertion dvresntr 
|- ( ph -> ( S _D F ) = ( S _D ( F |` Y ) ) )

Proof

Step Hyp Ref Expression
1 dvresntr.s 
 |-  ( ph -> S C_ CC )
2 dvresntr.x 
 |-  ( ph -> X C_ S )
3 dvresntr.f 
 |-  ( ph -> F : X --> CC )
4 dvresntr.j 
 |-  J = ( K |`t S )
5 dvresntr.k 
 |-  K = ( TopOpen ` CCfld )
6 dvresntr.i 
 |-  ( ph -> ( ( int ` J ) ` X ) = Y )
7 5 4 dvres 
 |-  ( ( ( S C_ CC /\ F : X --> CC ) /\ ( X C_ S /\ X C_ S ) ) -> ( S _D ( F |` X ) ) = ( ( S _D F ) |` ( ( int ` J ) ` X ) ) )
8 1 3 2 2 7 syl22anc 
 |-  ( ph -> ( S _D ( F |` X ) ) = ( ( S _D F ) |` ( ( int ` J ) ` X ) ) )
9 ffn 
 |-  ( F : X --> CC -> F Fn X )
10 fnresdm 
 |-  ( F Fn X -> ( F |` X ) = F )
11 3 9 10 3syl 
 |-  ( ph -> ( F |` X ) = F )
12 11 oveq2d 
 |-  ( ph -> ( S _D ( F |` X ) ) = ( S _D F ) )
13 5 cnfldtopon 
 |-  K e. ( TopOn ` CC )
14 resttopon 
 |-  ( ( K e. ( TopOn ` CC ) /\ S C_ CC ) -> ( K |`t S ) e. ( TopOn ` S ) )
15 13 1 14 sylancr 
 |-  ( ph -> ( K |`t S ) e. ( TopOn ` S ) )
16 4 15 eqeltrid 
 |-  ( ph -> J e. ( TopOn ` S ) )
17 topontop 
 |-  ( J e. ( TopOn ` S ) -> J e. Top )
18 16 17 syl 
 |-  ( ph -> J e. Top )
19 toponuni 
 |-  ( J e. ( TopOn ` S ) -> S = U. J )
20 16 19 syl 
 |-  ( ph -> S = U. J )
21 2 20 sseqtrd 
 |-  ( ph -> X C_ U. J )
22 eqid 
 |-  U. J = U. J
23 22 ntridm 
 |-  ( ( J e. Top /\ X C_ U. J ) -> ( ( int ` J ) ` ( ( int ` J ) ` X ) ) = ( ( int ` J ) ` X ) )
24 18 21 23 syl2anc 
 |-  ( ph -> ( ( int ` J ) ` ( ( int ` J ) ` X ) ) = ( ( int ` J ) ` X ) )
25 6 fveq2d 
 |-  ( ph -> ( ( int ` J ) ` ( ( int ` J ) ` X ) ) = ( ( int ` J ) ` Y ) )
26 24 25 6 3eqtr3d 
 |-  ( ph -> ( ( int ` J ) ` Y ) = Y )
27 26 reseq2d 
 |-  ( ph -> ( ( S _D F ) |` ( ( int ` J ) ` Y ) ) = ( ( S _D F ) |` Y ) )
28 22 ntrss2 
 |-  ( ( J e. Top /\ X C_ U. J ) -> ( ( int ` J ) ` X ) C_ X )
29 18 21 28 syl2anc 
 |-  ( ph -> ( ( int ` J ) ` X ) C_ X )
30 6 29 eqsstrrd 
 |-  ( ph -> Y C_ X )
31 30 2 sstrd 
 |-  ( ph -> Y C_ S )
32 5 4 dvres 
 |-  ( ( ( S C_ CC /\ F : X --> CC ) /\ ( X C_ S /\ Y C_ S ) ) -> ( S _D ( F |` Y ) ) = ( ( S _D F ) |` ( ( int ` J ) ` Y ) ) )
33 1 3 2 31 32 syl22anc 
 |-  ( ph -> ( S _D ( F |` Y ) ) = ( ( S _D F ) |` ( ( int ` J ) ` Y ) ) )
34 6 reseq2d 
 |-  ( ph -> ( ( S _D F ) |` ( ( int ` J ) ` X ) ) = ( ( S _D F ) |` Y ) )
35 27 33 34 3eqtr4rd 
 |-  ( ph -> ( ( S _D F ) |` ( ( int ` J ) ` X ) ) = ( S _D ( F |` Y ) ) )
36 8 12 35 3eqtr3d 
 |-  ( ph -> ( S _D F ) = ( S _D ( F |` Y ) ) )