Metamath Proof Explorer

Theorem dvmptntr

Description: Function-builder for derivative: expand the function from an open set to its closure. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses dvmptntr.s 
|- ( ph -> S C_ CC )
dvmptntr.x 
|- ( ph -> X C_ S )
dvmptntr.a 
|- ( ( ph /\ x e. X ) -> A e. CC )
dvmptntr.j 
|- J = ( K |`t S )
dvmptntr.k 
|- K = ( TopOpen ` CCfld )
dvmptntr.i 
|- ( ph -> ( ( int ` J ) ` X ) = Y )
Assertion dvmptntr 
|- ( ph -> ( S _D ( x e. X |-> A ) ) = ( S _D ( x e. Y |-> A ) ) )

Proof

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