Metamath Proof Explorer

Theorem ftc1lem1

Description: Lemma for ftc1a and ftc1 . (Contributed by Mario Carneiro, 31-Aug-2014)

Ref Expression
Hypotheses ftc1.g 
|- G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )
ftc1.a 
|- ( ph -> A e. RR )
ftc1.b 
|- ( ph -> B e. RR )
ftc1.le 
|- ( ph -> A <_ B )
ftc1.s 
|- ( ph -> ( A (,) B ) C_ D )
ftc1.d 
|- ( ph -> D C_ RR )
ftc1.i 
|- ( ph -> F e. L^1 )
ftc1a.f 
|- ( ph -> F : D --> CC )
ftc1lem1.x 
|- ( ph -> X e. ( A [,] B ) )
ftc1lem1.y 
|- ( ph -> Y e. ( A [,] B ) )
Assertion ftc1lem1 
|- ( ( ph /\ X <_ Y ) -> ( ( G ` Y ) - ( G ` X ) ) = S. ( X (,) Y ) ( F ` t ) _d t )

Proof

Step Hyp Ref Expression
1 ftc1.g 
 |-  G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )
2 ftc1.a 
 |-  ( ph -> A e. RR )
3 ftc1.b 
 |-  ( ph -> B e. RR )
4 ftc1.le 
 |-  ( ph -> A <_ B )
5 ftc1.s 
 |-  ( ph -> ( A (,) B ) C_ D )
6 ftc1.d 
 |-  ( ph -> D C_ RR )
7 ftc1.i 
 |-  ( ph -> F e. L^1 )
8 ftc1a.f 
 |-  ( ph -> F : D --> CC )
9 ftc1lem1.x 
 |-  ( ph -> X e. ( A [,] B ) )
10 ftc1lem1.y 
 |-  ( ph -> Y e. ( A [,] B ) )
11 oveq2 
 |-  ( x = Y -> ( A (,) x ) = ( A (,) Y ) )
12 itgeq1 
 |-  ( ( A (,) x ) = ( A (,) Y ) -> S. ( A (,) x ) ( F ` t ) _d t = S. ( A (,) Y ) ( F ` t ) _d t )
13 11 12 syl 
 |-  ( x = Y -> S. ( A (,) x ) ( F ` t ) _d t = S. ( A (,) Y ) ( F ` t ) _d t )
14 itgex 
 |-  S. ( A (,) Y ) ( F ` t ) _d t e. _V
15 13 1 14 fvmpt 
 |-  ( Y e. ( A [,] B ) -> ( G ` Y ) = S. ( A (,) Y ) ( F ` t ) _d t )
16 10 15 syl 
 |-  ( ph -> ( G ` Y ) = S. ( A (,) Y ) ( F ` t ) _d t )
17 16 adantr 
 |-  ( ( ph /\ X <_ Y ) -> ( G ` Y ) = S. ( A (,) Y ) ( F ` t ) _d t )
18 2 adantr 
 |-  ( ( ph /\ X <_ Y ) -> A e. RR )
19 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
20 2 3 19 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
21 20 10 sseldd 
 |-  ( ph -> Y e. RR )
22 21 adantr 
 |-  ( ( ph /\ X <_ Y ) -> Y e. RR )
23 20 9 sseldd 
 |-  ( ph -> X e. RR )
24 23 adantr 
 |-  ( ( ph /\ X <_ Y ) -> X e. RR )
25 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( X e. ( A [,] B ) <-> ( X e. RR /\ A <_ X /\ X <_ B ) ) )
26 2 3 25 syl2anc 
 |-  ( ph -> ( X e. ( A [,] B ) <-> ( X e. RR /\ A <_ X /\ X <_ B ) ) )
27 9 26 mpbid 
 |-  ( ph -> ( X e. RR /\ A <_ X /\ X <_ B ) )
28 27 simp2d 
 |-  ( ph -> A <_ X )
29 28 adantr 
 |-  ( ( ph /\ X <_ Y ) -> A <_ X )
30 simpr 
 |-  ( ( ph /\ X <_ Y ) -> X <_ Y )
31 elicc2 
 |-  ( ( A e. RR /\ Y e. RR ) -> ( X e. ( A [,] Y ) <-> ( X e. RR /\ A <_ X /\ X <_ Y ) ) )
32 2 21 31 syl2anc 
 |-  ( ph -> ( X e. ( A [,] Y ) <-> ( X e. RR /\ A <_ X /\ X <_ Y ) ) )
33 32 adantr 
 |-  ( ( ph /\ X <_ Y ) -> ( X e. ( A [,] Y ) <-> ( X e. RR /\ A <_ X /\ X <_ Y ) ) )
34 24 29 30 33 mpbir3and 
 |-  ( ( ph /\ X <_ Y ) -> X e. ( A [,] Y ) )
35 3 rexrd 
 |-  ( ph -> B e. RR* )
36 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( Y e. ( A [,] B ) <-> ( Y e. RR /\ A <_ Y /\ Y <_ B ) ) )
37 2 3 36 syl2anc 
 |-  ( ph -> ( Y e. ( A [,] B ) <-> ( Y e. RR /\ A <_ Y /\ Y <_ B ) ) )
38 10 37 mpbid 
 |-  ( ph -> ( Y e. RR /\ A <_ Y /\ Y <_ B ) )
39 38 simp3d 
 |-  ( ph -> Y <_ B )
40 iooss2 
 |-  ( ( B e. RR* /\ Y <_ B ) -> ( A (,) Y ) C_ ( A (,) B ) )
41 35 39 40 syl2anc 
 |-  ( ph -> ( A (,) Y ) C_ ( A (,) B ) )
42 41 5 sstrd 
 |-  ( ph -> ( A (,) Y ) C_ D )
43 42 adantr 
 |-  ( ( ph /\ X <_ Y ) -> ( A (,) Y ) C_ D )
44 43 sselda 
 |-  ( ( ( ph /\ X <_ Y ) /\ t e. ( A (,) Y ) ) -> t e. D )
45 8 ffvelrnda 
 |-  ( ( ph /\ t e. D ) -> ( F ` t ) e. CC )
46 45 adantlr 
 |-  ( ( ( ph /\ X <_ Y ) /\ t e. D ) -> ( F ` t ) e. CC )
47 44 46 syldan 
 |-  ( ( ( ph /\ X <_ Y ) /\ t e. ( A (,) Y ) ) -> ( F ` t ) e. CC )
48 27 simp3d 
 |-  ( ph -> X <_ B )
49 iooss2 
 |-  ( ( B e. RR* /\ X <_ B ) -> ( A (,) X ) C_ ( A (,) B ) )
50 35 48 49 syl2anc 
 |-  ( ph -> ( A (,) X ) C_ ( A (,) B ) )
51 50 5 sstrd 
 |-  ( ph -> ( A (,) X ) C_ D )
52 ioombl 
 |-  ( A (,) X ) e. dom vol
53 52 a1i 
 |-  ( ph -> ( A (,) X ) e. dom vol )
54 fvexd 
 |-  ( ( ph /\ t e. D ) -> ( F ` t ) e. _V )
55 8 feqmptd 
 |-  ( ph -> F = ( t e. D |-> ( F ` t ) ) )
56 55 7 eqeltrrd 
 |-  ( ph -> ( t e. D |-> ( F ` t ) ) e. L^1 )
57 51 53 54 56 iblss 
 |-  ( ph -> ( t e. ( A (,) X ) |-> ( F ` t ) ) e. L^1 )
58 57 adantr 
 |-  ( ( ph /\ X <_ Y ) -> ( t e. ( A (,) X ) |-> ( F ` t ) ) e. L^1 )
59 2 rexrd 
 |-  ( ph -> A e. RR* )
60 iooss1 
 |-  ( ( A e. RR* /\ A <_ X ) -> ( X (,) Y ) C_ ( A (,) Y ) )
61 59 28 60 syl2anc 
 |-  ( ph -> ( X (,) Y ) C_ ( A (,) Y ) )
62 61 41 sstrd 
 |-  ( ph -> ( X (,) Y ) C_ ( A (,) B ) )
63 62 5 sstrd 
 |-  ( ph -> ( X (,) Y ) C_ D )
64 ioombl 
 |-  ( X (,) Y ) e. dom vol
65 64 a1i 
 |-  ( ph -> ( X (,) Y ) e. dom vol )
66 63 65 54 56 iblss 
 |-  ( ph -> ( t e. ( X (,) Y ) |-> ( F ` t ) ) e. L^1 )
67 66 adantr 
 |-  ( ( ph /\ X <_ Y ) -> ( t e. ( X (,) Y ) |-> ( F ` t ) ) e. L^1 )
68 18 22 34 47 58 67 itgsplitioo 
 |-  ( ( ph /\ X <_ Y ) -> S. ( A (,) Y ) ( F ` t ) _d t = ( S. ( A (,) X ) ( F ` t ) _d t + S. ( X (,) Y ) ( F ` t ) _d t ) )
69 17 68 eqtrd 
 |-  ( ( ph /\ X <_ Y ) -> ( G ` Y ) = ( S. ( A (,) X ) ( F ` t ) _d t + S. ( X (,) Y ) ( F ` t ) _d t ) )
70 oveq2 
 |-  ( x = X -> ( A (,) x ) = ( A (,) X ) )
71 itgeq1 
 |-  ( ( A (,) x ) = ( A (,) X ) -> S. ( A (,) x ) ( F ` t ) _d t = S. ( A (,) X ) ( F ` t ) _d t )
72 70 71 syl 
 |-  ( x = X -> S. ( A (,) x ) ( F ` t ) _d t = S. ( A (,) X ) ( F ` t ) _d t )
73 itgex 
 |-  S. ( A (,) X ) ( F ` t ) _d t e. _V
74 72 1 73 fvmpt 
 |-  ( X e. ( A [,] B ) -> ( G ` X ) = S. ( A (,) X ) ( F ` t ) _d t )
75 9 74 syl 
 |-  ( ph -> ( G ` X ) = S. ( A (,) X ) ( F ` t ) _d t )
76 75 adantr 
 |-  ( ( ph /\ X <_ Y ) -> ( G ` X ) = S. ( A (,) X ) ( F ` t ) _d t )
77 69 76 oveq12d 
 |-  ( ( ph /\ X <_ Y ) -> ( ( G ` Y ) - ( G ` X ) ) = ( ( S. ( A (,) X ) ( F ` t ) _d t + S. ( X (,) Y ) ( F ` t ) _d t ) - S. ( A (,) X ) ( F ` t ) _d t ) )
78 fvexd 
 |-  ( ( ph /\ t e. ( A (,) X ) ) -> ( F ` t ) e. _V )
79 78 57 itgcl 
 |-  ( ph -> S. ( A (,) X ) ( F ` t ) _d t e. CC )
80 63 sselda 
 |-  ( ( ph /\ t e. ( X (,) Y ) ) -> t e. D )
81 80 45 syldan 
 |-  ( ( ph /\ t e. ( X (,) Y ) ) -> ( F ` t ) e. CC )
82 81 66 itgcl 
 |-  ( ph -> S. ( X (,) Y ) ( F ` t ) _d t e. CC )
83 79 82 pncan2d 
 |-  ( ph -> ( ( S. ( A (,) X ) ( F ` t ) _d t + S. ( X (,) Y ) ( F ` t ) _d t ) - S. ( A (,) X ) ( F ` t ) _d t ) = S. ( X (,) Y ) ( F ` t ) _d t )
84 83 adantr 
 |-  ( ( ph /\ X <_ Y ) -> ( ( S. ( A (,) X ) ( F ` t ) _d t + S. ( X (,) Y ) ( F ` t ) _d t ) - S. ( A (,) X ) ( F ` t ) _d t ) = S. ( X (,) Y ) ( F ` t ) _d t )
85 77 84 eqtrd 
 |-  ( ( ph /\ X <_ Y ) -> ( ( G ` Y ) - ( G ` X ) ) = S. ( X (,) Y ) ( F ` t ) _d t )