Metamath Proof Explorer

Theorem dvmptresicc

Description: Derivative of a function restricted to a closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dvmptresicc.f 
|- F = ( x e. CC |-> A )
dvmptresicc.a 
|- ( ( ph /\ x e. CC ) -> A e. CC )
dvmptresicc.fdv 
|- ( ph -> ( CC _D F ) = ( x e. CC |-> B ) )
dvmptresicc.b 
|- ( ( ph /\ x e. CC ) -> B e. CC )
dvmptresicc.c 
|- ( ph -> C e. RR )
dvmptresicc.d 
|- ( ph -> D e. RR )
Assertion dvmptresicc 
|- ( ph -> ( RR _D ( x e. ( C [,] D ) |-> A ) ) = ( x e. ( C (,) D ) |-> B ) )

Proof

Step Hyp Ref Expression
1 dvmptresicc.f 
 |-  F = ( x e. CC |-> A )
2 dvmptresicc.a 
 |-  ( ( ph /\ x e. CC ) -> A e. CC )
3 dvmptresicc.fdv 
 |-  ( ph -> ( CC _D F ) = ( x e. CC |-> B ) )
4 dvmptresicc.b 
 |-  ( ( ph /\ x e. CC ) -> B e. CC )
5 dvmptresicc.c 
 |-  ( ph -> C e. RR )
6 dvmptresicc.d 
 |-  ( ph -> D e. RR )
7 1 reseq1i 
 |-  ( F |` ( C [,] D ) ) = ( ( x e. CC |-> A ) |` ( C [,] D ) )
8 5 6 iccssred 
 |-  ( ph -> ( C [,] D ) C_ RR )
9 ax-resscn 
 |-  RR C_ CC
10 9 a1i 
 |-  ( ph -> RR C_ CC )
11 8 10 sstrd 
 |-  ( ph -> ( C [,] D ) C_ CC )
12 11 resmptd 
 |-  ( ph -> ( ( x e. CC |-> A ) |` ( C [,] D ) ) = ( x e. ( C [,] D ) |-> A ) )
13 7 12 syl5eq 
 |-  ( ph -> ( F |` ( C [,] D ) ) = ( x e. ( C [,] D ) |-> A ) )
14 13 oveq2d 
 |-  ( ph -> ( RR _D ( F |` ( C [,] D ) ) ) = ( RR _D ( x e. ( C [,] D ) |-> A ) ) )
15 8 resabs1d 
 |-  ( ph -> ( ( F |` RR ) |` ( C [,] D ) ) = ( F |` ( C [,] D ) ) )
16 15 eqcomd 
 |-  ( ph -> ( F |` ( C [,] D ) ) = ( ( F |` RR ) |` ( C [,] D ) ) )
17 16 oveq2d 
 |-  ( ph -> ( RR _D ( F |` ( C [,] D ) ) ) = ( RR _D ( ( F |` RR ) |` ( C [,] D ) ) ) )
18 2 1 fmptd 
 |-  ( ph -> F : CC --> CC )
19 18 10 fssresd 
 |-  ( ph -> ( F |` RR ) : RR --> CC )
20 ssidd 
 |-  ( ph -> RR C_ RR )
21 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
22 21 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
23 21 22 dvres 
 |-  ( ( ( RR C_ CC /\ ( F |` RR ) : RR --> CC ) /\ ( RR C_ RR /\ ( C [,] D ) C_ RR ) ) -> ( RR _D ( ( F |` RR ) |` ( C [,] D ) ) ) = ( ( RR _D ( F |` RR ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( C [,] D ) ) ) )
24 10 19 20 8 23 syl22anc 
 |-  ( ph -> ( RR _D ( ( F |` RR ) |` ( C [,] D ) ) ) = ( ( RR _D ( F |` RR ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( C [,] D ) ) ) )
25 reelprrecn 
 |-  RR e. { RR , CC }
26 25 a1i 
 |-  ( ph -> RR e. { RR , CC } )
27 ssidd 
 |-  ( ph -> CC C_ CC )
28 3 dmeqd 
 |-  ( ph -> dom ( CC _D F ) = dom ( x e. CC |-> B ) )
29 4 ralrimiva 
 |-  ( ph -> A. x e. CC B e. CC )
30 dmmptg 
 |-  ( A. x e. CC B e. CC -> dom ( x e. CC |-> B ) = CC )
31 29 30 syl 
 |-  ( ph -> dom ( x e. CC |-> B ) = CC )
32 28 31 eqtr2d 
 |-  ( ph -> CC = dom ( CC _D F ) )
33 10 32 sseqtrd 
 |-  ( ph -> RR C_ dom ( CC _D F ) )
34 dvres3 
 |-  ( ( ( RR e. { RR , CC } /\ F : CC --> CC ) /\ ( CC C_ CC /\ RR C_ dom ( CC _D F ) ) ) -> ( RR _D ( F |` RR ) ) = ( ( CC _D F ) |` RR ) )
35 26 18 27 33 34 syl22anc 
 |-  ( ph -> ( RR _D ( F |` RR ) ) = ( ( CC _D F ) |` RR ) )
36 iccntr 
 |-  ( ( C e. RR /\ D e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( C [,] D ) ) = ( C (,) D ) )
37 5 6 36 syl2anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( C [,] D ) ) = ( C (,) D ) )
38 35 37 reseq12d 
 |-  ( ph -> ( ( RR _D ( F |` RR ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( C [,] D ) ) ) = ( ( ( CC _D F ) |` RR ) |` ( C (,) D ) ) )
39 ioossre 
 |-  ( C (,) D ) C_ RR
40 resabs1 
 |-  ( ( C (,) D ) C_ RR -> ( ( ( CC _D F ) |` RR ) |` ( C (,) D ) ) = ( ( CC _D F ) |` ( C (,) D ) ) )
41 39 40 mp1i 
 |-  ( ph -> ( ( ( CC _D F ) |` RR ) |` ( C (,) D ) ) = ( ( CC _D F ) |` ( C (,) D ) ) )
42 3 reseq1d 
 |-  ( ph -> ( ( CC _D F ) |` ( C (,) D ) ) = ( ( x e. CC |-> B ) |` ( C (,) D ) ) )
43 ioosscn 
 |-  ( C (,) D ) C_ CC
44 resmpt 
 |-  ( ( C (,) D ) C_ CC -> ( ( x e. CC |-> B ) |` ( C (,) D ) ) = ( x e. ( C (,) D ) |-> B ) )
45 43 44 mp1i 
 |-  ( ph -> ( ( x e. CC |-> B ) |` ( C (,) D ) ) = ( x e. ( C (,) D ) |-> B ) )
46 42 45 eqtrd 
 |-  ( ph -> ( ( CC _D F ) |` ( C (,) D ) ) = ( x e. ( C (,) D ) |-> B ) )
47 38 41 46 3eqtrd 
 |-  ( ph -> ( ( RR _D ( F |` RR ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( C [,] D ) ) ) = ( x e. ( C (,) D ) |-> B ) )
48 17 24 47 3eqtrd 
 |-  ( ph -> ( RR _D ( F |` ( C [,] D ) ) ) = ( x e. ( C (,) D ) |-> B ) )
49 14 48 eqtr3d 
 |-  ( ph -> ( RR _D ( x e. ( C [,] D ) |-> A ) ) = ( x e. ( C (,) D ) |-> B ) )