Metamath Proof Explorer

Theorem ftc2ditglem

Description: Lemma for ftc2ditg . (Contributed by Mario Carneiro, 3-Sep-2014)

Ref Expression
Hypotheses ftc2ditg.x 
|- ( ph -> X e. RR )
ftc2ditg.y 
|- ( ph -> Y e. RR )
ftc2ditg.a 
|- ( ph -> A e. ( X [,] Y ) )
ftc2ditg.b 
|- ( ph -> B e. ( X [,] Y ) )
ftc2ditg.c 
|- ( ph -> ( RR _D F ) e. ( ( X (,) Y ) -cn-> CC ) )
ftc2ditg.i 
|- ( ph -> ( RR _D F ) e. L^1 )
ftc2ditg.f 
|- ( ph -> F e. ( ( X [,] Y ) -cn-> CC ) )
Assertion ftc2ditglem 
|- ( ( ph /\ A <_ B ) -> S_ [ A -> B ] ( ( RR _D F ) ` t ) _d t = ( ( F ` B ) - ( F ` A ) ) )

Proof

Step Hyp Ref Expression
1 ftc2ditg.x 
 |-  ( ph -> X e. RR )
2 ftc2ditg.y 
 |-  ( ph -> Y e. RR )
3 ftc2ditg.a 
 |-  ( ph -> A e. ( X [,] Y ) )
4 ftc2ditg.b 
 |-  ( ph -> B e. ( X [,] Y ) )
5 ftc2ditg.c 
 |-  ( ph -> ( RR _D F ) e. ( ( X (,) Y ) -cn-> CC ) )
6 ftc2ditg.i 
 |-  ( ph -> ( RR _D F ) e. L^1 )
7 ftc2ditg.f 
 |-  ( ph -> F e. ( ( X [,] Y ) -cn-> CC ) )
8 simpr 
 |-  ( ( ph /\ A <_ B ) -> A <_ B )
9 8 ditgpos 
 |-  ( ( ph /\ A <_ B ) -> S_ [ A -> B ] ( ( RR _D F ) ` t ) _d t = S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t )
10 iccssre 
 |-  ( ( X e. RR /\ Y e. RR ) -> ( X [,] Y ) C_ RR )
11 1 2 10 syl2anc 
 |-  ( ph -> ( X [,] Y ) C_ RR )
12 11 3 sseldd 
 |-  ( ph -> A e. RR )
13 12 adantr 
 |-  ( ( ph /\ A <_ B ) -> A e. RR )
14 11 4 sseldd 
 |-  ( ph -> B e. RR )
15 14 adantr 
 |-  ( ( ph /\ A <_ B ) -> B e. RR )
16 ax-resscn 
 |-  RR C_ CC
17 16 a1i 
 |-  ( ( ph /\ A <_ B ) -> RR C_ CC )
18 cncff 
 |-  ( F e. ( ( X [,] Y ) -cn-> CC ) -> F : ( X [,] Y ) --> CC )
19 7 18 syl 
 |-  ( ph -> F : ( X [,] Y ) --> CC )
20 19 adantr 
 |-  ( ( ph /\ A <_ B ) -> F : ( X [,] Y ) --> CC )
21 11 adantr 
 |-  ( ( ph /\ A <_ B ) -> ( X [,] Y ) C_ RR )
22 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
23 12 14 22 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
24 23 adantr 
 |-  ( ( ph /\ A <_ B ) -> ( A [,] B ) C_ RR )
25 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
26 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
27 25 26 dvres 
 |-  ( ( ( RR C_ CC /\ F : ( X [,] Y ) --> CC ) /\ ( ( X [,] Y ) C_ RR /\ ( A [,] B ) C_ RR ) ) -> ( RR _D ( F |` ( A [,] B ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) ) )
28 17 20 21 24 27 syl22anc 
 |-  ( ( ph /\ A <_ B ) -> ( RR _D ( F |` ( A [,] B ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) ) )
29 iccntr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
30 12 14 29 syl2anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
31 30 adantr 
 |-  ( ( ph /\ A <_ B ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
32 31 reseq2d 
 |-  ( ( ph /\ A <_ B ) -> ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) ) = ( ( RR _D F ) |` ( A (,) B ) ) )
33 28 32 eqtrd 
 |-  ( ( ph /\ A <_ B ) -> ( RR _D ( F |` ( A [,] B ) ) ) = ( ( RR _D F ) |` ( A (,) B ) ) )
34 1 rexrd 
 |-  ( ph -> X e. RR* )
35 elicc2 
 |-  ( ( X e. RR /\ Y e. RR ) -> ( A e. ( X [,] Y ) <-> ( A e. RR /\ X <_ A /\ A <_ Y ) ) )
36 1 2 35 syl2anc 
 |-  ( ph -> ( A e. ( X [,] Y ) <-> ( A e. RR /\ X <_ A /\ A <_ Y ) ) )
37 3 36 mpbid 
 |-  ( ph -> ( A e. RR /\ X <_ A /\ A <_ Y ) )
38 37 simp2d 
 |-  ( ph -> X <_ A )
39 iooss1 
 |-  ( ( X e. RR* /\ X <_ A ) -> ( A (,) B ) C_ ( X (,) B ) )
40 34 38 39 syl2anc 
 |-  ( ph -> ( A (,) B ) C_ ( X (,) B ) )
41 2 rexrd 
 |-  ( ph -> Y e. RR* )
42 elicc2 
 |-  ( ( X e. RR /\ Y e. RR ) -> ( B e. ( X [,] Y ) <-> ( B e. RR /\ X <_ B /\ B <_ Y ) ) )
43 1 2 42 syl2anc 
 |-  ( ph -> ( B e. ( X [,] Y ) <-> ( B e. RR /\ X <_ B /\ B <_ Y ) ) )
44 4 43 mpbid 
 |-  ( ph -> ( B e. RR /\ X <_ B /\ B <_ Y ) )
45 44 simp3d 
 |-  ( ph -> B <_ Y )
46 iooss2 
 |-  ( ( Y e. RR* /\ B <_ Y ) -> ( X (,) B ) C_ ( X (,) Y ) )
47 41 45 46 syl2anc 
 |-  ( ph -> ( X (,) B ) C_ ( X (,) Y ) )
48 40 47 sstrd 
 |-  ( ph -> ( A (,) B ) C_ ( X (,) Y ) )
49 48 adantr 
 |-  ( ( ph /\ A <_ B ) -> ( A (,) B ) C_ ( X (,) Y ) )
50 5 adantr 
 |-  ( ( ph /\ A <_ B ) -> ( RR _D F ) e. ( ( X (,) Y ) -cn-> CC ) )
51 rescncf 
 |-  ( ( A (,) B ) C_ ( X (,) Y ) -> ( ( RR _D F ) e. ( ( X (,) Y ) -cn-> CC ) -> ( ( RR _D F ) |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) ) )
52 49 50 51 sylc 
 |-  ( ( ph /\ A <_ B ) -> ( ( RR _D F ) |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) )
53 33 52 eqeltrd 
 |-  ( ( ph /\ A <_ B ) -> ( RR _D ( F |` ( A [,] B ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
54 cncff 
 |-  ( ( RR _D F ) e. ( ( X (,) Y ) -cn-> CC ) -> ( RR _D F ) : ( X (,) Y ) --> CC )
55 5 54 syl 
 |-  ( ph -> ( RR _D F ) : ( X (,) Y ) --> CC )
56 55 feqmptd 
 |-  ( ph -> ( RR _D F ) = ( t e. ( X (,) Y ) |-> ( ( RR _D F ) ` t ) ) )
57 56 adantr 
 |-  ( ( ph /\ A <_ B ) -> ( RR _D F ) = ( t e. ( X (,) Y ) |-> ( ( RR _D F ) ` t ) ) )
58 57 reseq1d 
 |-  ( ( ph /\ A <_ B ) -> ( ( RR _D F ) |` ( A (,) B ) ) = ( ( t e. ( X (,) Y ) |-> ( ( RR _D F ) ` t ) ) |` ( A (,) B ) ) )
59 49 resmptd 
 |-  ( ( ph /\ A <_ B ) -> ( ( t e. ( X (,) Y ) |-> ( ( RR _D F ) ` t ) ) |` ( A (,) B ) ) = ( t e. ( A (,) B ) |-> ( ( RR _D F ) ` t ) ) )
60 58 59 eqtrd 
 |-  ( ( ph /\ A <_ B ) -> ( ( RR _D F ) |` ( A (,) B ) ) = ( t e. ( A (,) B ) |-> ( ( RR _D F ) ` t ) ) )
61 33 60 eqtrd 
 |-  ( ( ph /\ A <_ B ) -> ( RR _D ( F |` ( A [,] B ) ) ) = ( t e. ( A (,) B ) |-> ( ( RR _D F ) ` t ) ) )
62 ioombl 
 |-  ( A (,) B ) e. dom vol
63 62 a1i 
 |-  ( ( ph /\ A <_ B ) -> ( A (,) B ) e. dom vol )
64 fvexd 
 |-  ( ( ( ph /\ A <_ B ) /\ t e. ( X (,) Y ) ) -> ( ( RR _D F ) ` t ) e. _V )
65 6 adantr 
 |-  ( ( ph /\ A <_ B ) -> ( RR _D F ) e. L^1 )
66 57 65 eqeltrrd 
 |-  ( ( ph /\ A <_ B ) -> ( t e. ( X (,) Y ) |-> ( ( RR _D F ) ` t ) ) e. L^1 )
67 49 63 64 66 iblss 
 |-  ( ( ph /\ A <_ B ) -> ( t e. ( A (,) B ) |-> ( ( RR _D F ) ` t ) ) e. L^1 )
68 61 67 eqeltrd 
 |-  ( ( ph /\ A <_ B ) -> ( RR _D ( F |` ( A [,] B ) ) ) e. L^1 )
69 iccss2 
 |-  ( ( A e. ( X [,] Y ) /\ B e. ( X [,] Y ) ) -> ( A [,] B ) C_ ( X [,] Y ) )
70 3 4 69 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ ( X [,] Y ) )
71 rescncf 
 |-  ( ( A [,] B ) C_ ( X [,] Y ) -> ( F e. ( ( X [,] Y ) -cn-> CC ) -> ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) )
72 70 7 71 sylc 
 |-  ( ph -> ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
73 72 adantr 
 |-  ( ( ph /\ A <_ B ) -> ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
74 13 15 8 53 68 73 ftc2 
 |-  ( ( ph /\ A <_ B ) -> S. ( A (,) B ) ( ( RR _D ( F |` ( A [,] B ) ) ) ` t ) _d t = ( ( ( F |` ( A [,] B ) ) ` B ) - ( ( F |` ( A [,] B ) ) ` A ) ) )
75 33 fveq1d 
 |-  ( ( ph /\ A <_ B ) -> ( ( RR _D ( F |` ( A [,] B ) ) ) ` t ) = ( ( ( RR _D F ) |` ( A (,) B ) ) ` t ) )
76 fvres 
 |-  ( t e. ( A (,) B ) -> ( ( ( RR _D F ) |` ( A (,) B ) ) ` t ) = ( ( RR _D F ) ` t ) )
77 75 76 sylan9eq 
 |-  ( ( ( ph /\ A <_ B ) /\ t e. ( A (,) B ) ) -> ( ( RR _D ( F |` ( A [,] B ) ) ) ` t ) = ( ( RR _D F ) ` t ) )
78 77 itgeq2dv 
 |-  ( ( ph /\ A <_ B ) -> S. ( A (,) B ) ( ( RR _D ( F |` ( A [,] B ) ) ) ` t ) _d t = S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t )
79 13 rexrd 
 |-  ( ( ph /\ A <_ B ) -> A e. RR* )
80 15 rexrd 
 |-  ( ( ph /\ A <_ B ) -> B e. RR* )
81 ubicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
82 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
83 fvres 
 |-  ( B e. ( A [,] B ) -> ( ( F |` ( A [,] B ) ) ` B ) = ( F ` B ) )
84 fvres 
 |-  ( A e. ( A [,] B ) -> ( ( F |` ( A [,] B ) ) ` A ) = ( F ` A ) )
85 83 84 oveqan12d 
 |-  ( ( B e. ( A [,] B ) /\ A e. ( A [,] B ) ) -> ( ( ( F |` ( A [,] B ) ) ` B ) - ( ( F |` ( A [,] B ) ) ` A ) ) = ( ( F ` B ) - ( F ` A ) ) )
86 81 82 85 syl2anc 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( ( F |` ( A [,] B ) ) ` B ) - ( ( F |` ( A [,] B ) ) ` A ) ) = ( ( F ` B ) - ( F ` A ) ) )
87 79 80 8 86 syl3anc 
 |-  ( ( ph /\ A <_ B ) -> ( ( ( F |` ( A [,] B ) ) ` B ) - ( ( F |` ( A [,] B ) ) ` A ) ) = ( ( F ` B ) - ( F ` A ) ) )
88 74 78 87 3eqtr3d 
 |-  ( ( ph /\ A <_ B ) -> S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t = ( ( F ` B ) - ( F ` A ) ) )
89 9 88 eqtrd 
 |-  ( ( ph /\ A <_ B ) -> S_ [ A -> B ] ( ( RR _D F ) ` t ) _d t = ( ( F ` B ) - ( F ` A ) ) )