Metamath Proof Explorer

Theorem dvmptres3

Description: Function-builder for derivative: restrict a derivative to a subset. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses dvmptres3.j 
|- J = ( TopOpen ` CCfld )
dvmptres3.s 
|- ( ph -> S e. { RR , CC } )
dvmptres3.x 
|- ( ph -> X e. J )
dvmptres3.y 
|- ( ph -> ( S i^i X ) = Y )
dvmptres3.a 
|- ( ( ph /\ x e. X ) -> A e. CC )
dvmptres3.b 
|- ( ( ph /\ x e. X ) -> B e. V )
dvmptres3.d 
|- ( ph -> ( CC _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )
Assertion dvmptres3 
|- ( ph -> ( S _D ( x e. Y |-> A ) ) = ( x e. Y |-> B ) )

Proof

Step Hyp Ref Expression
1 dvmptres3.j 
 |-  J = ( TopOpen ` CCfld )
2 dvmptres3.s 
 |-  ( ph -> S e. { RR , CC } )
3 dvmptres3.x 
 |-  ( ph -> X e. J )
4 dvmptres3.y 
 |-  ( ph -> ( S i^i X ) = Y )
5 dvmptres3.a 
 |-  ( ( ph /\ x e. X ) -> A e. CC )
6 dvmptres3.b 
 |-  ( ( ph /\ x e. X ) -> B e. V )
7 dvmptres3.d 
 |-  ( ph -> ( CC _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )
8 5 fmpttd 
 |-  ( ph -> ( x e. X |-> A ) : X --> CC )
9 7 dmeqd 
 |-  ( ph -> dom ( CC _D ( x e. X |-> A ) ) = dom ( x e. X |-> B ) )
10 eqid 
 |-  ( x e. X |-> B ) = ( x e. X |-> B )
11 10 6 dmmptd 
 |-  ( ph -> dom ( x e. X |-> B ) = X )
12 9 11 eqtrd 
 |-  ( ph -> dom ( CC _D ( x e. X |-> A ) ) = X )
13 1 dvres3a 
 |-  ( ( ( S e. { RR , CC } /\ ( x e. X |-> A ) : X --> CC ) /\ ( X e. J /\ dom ( CC _D ( x e. X |-> A ) ) = X ) ) -> ( S _D ( ( x e. X |-> A ) |` S ) ) = ( ( CC _D ( x e. X |-> A ) ) |` S ) )
14 2 8 3 12 13 syl22anc 
 |-  ( ph -> ( S _D ( ( x e. X |-> A ) |` S ) ) = ( ( CC _D ( x e. X |-> A ) ) |` S ) )
15 rescom 
 |-  ( ( ( x e. X |-> A ) |` X ) |` S ) = ( ( ( x e. X |-> A ) |` S ) |` X )
16 resres 
 |-  ( ( ( x e. X |-> A ) |` S ) |` X ) = ( ( x e. X |-> A ) |` ( S i^i X ) )
17 15 16 eqtri 
 |-  ( ( ( x e. X |-> A ) |` X ) |` S ) = ( ( x e. X |-> A ) |` ( S i^i X ) )
18 4 reseq2d 
 |-  ( ph -> ( ( x e. X |-> A ) |` ( S i^i X ) ) = ( ( x e. X |-> A ) |` Y ) )
19 17 18 eqtrid 
 |-  ( ph -> ( ( ( x e. X |-> A ) |` X ) |` S ) = ( ( x e. X |-> A ) |` Y ) )
20 ffn 
 |-  ( ( x e. X |-> A ) : X --> CC -> ( x e. X |-> A ) Fn X )
21 fnresdm 
 |-  ( ( x e. X |-> A ) Fn X -> ( ( x e. X |-> A ) |` X ) = ( x e. X |-> A ) )
22 8 20 21 3syl 
 |-  ( ph -> ( ( x e. X |-> A ) |` X ) = ( x e. X |-> A ) )
23 22 reseq1d 
 |-  ( ph -> ( ( ( x e. X |-> A ) |` X ) |` S ) = ( ( x e. X |-> A ) |` S ) )
24 inss2 
 |-  ( S i^i X ) C_ X
25 4 24 eqsstrrdi 
 |-  ( ph -> Y C_ X )
26 25 resmptd 
 |-  ( ph -> ( ( x e. X |-> A ) |` Y ) = ( x e. Y |-> A ) )
27 19 23 26 3eqtr3d 
 |-  ( ph -> ( ( x e. X |-> A ) |` S ) = ( x e. Y |-> A ) )
28 27 oveq2d 
 |-  ( ph -> ( S _D ( ( x e. X |-> A ) |` S ) ) = ( S _D ( x e. Y |-> A ) ) )
29 rescom 
 |-  ( ( ( x e. X |-> B ) |` X ) |` S ) = ( ( ( x e. X |-> B ) |` S ) |` X )
30 resres 
 |-  ( ( ( x e. X |-> B ) |` S ) |` X ) = ( ( x e. X |-> B ) |` ( S i^i X ) )
31 29 30 eqtri 
 |-  ( ( ( x e. X |-> B ) |` X ) |` S ) = ( ( x e. X |-> B ) |` ( S i^i X ) )
32 4 reseq2d 
 |-  ( ph -> ( ( x e. X |-> B ) |` ( S i^i X ) ) = ( ( x e. X |-> B ) |` Y ) )
33 31 32 eqtrid 
 |-  ( ph -> ( ( ( x e. X |-> B ) |` X ) |` S ) = ( ( x e. X |-> B ) |` Y ) )
34 6 ralrimiva 
 |-  ( ph -> A. x e. X B e. V )
35 10 fnmpt 
 |-  ( A. x e. X B e. V -> ( x e. X |-> B ) Fn X )
36 fnresdm 
 |-  ( ( x e. X |-> B ) Fn X -> ( ( x e. X |-> B ) |` X ) = ( x e. X |-> B ) )
37 34 35 36 3syl 
 |-  ( ph -> ( ( x e. X |-> B ) |` X ) = ( x e. X |-> B ) )
38 37 7 eqtr4d 
 |-  ( ph -> ( ( x e. X |-> B ) |` X ) = ( CC _D ( x e. X |-> A ) ) )
39 38 reseq1d 
 |-  ( ph -> ( ( ( x e. X |-> B ) |` X ) |` S ) = ( ( CC _D ( x e. X |-> A ) ) |` S ) )
40 25 resmptd 
 |-  ( ph -> ( ( x e. X |-> B ) |` Y ) = ( x e. Y |-> B ) )
41 33 39 40 3eqtr3d 
 |-  ( ph -> ( ( CC _D ( x e. X |-> A ) ) |` S ) = ( x e. Y |-> B ) )
42 14 28 41 3eqtr3d 
 |-  ( ph -> ( S _D ( x e. Y |-> A ) ) = ( x e. Y |-> B ) )