Metamath Proof Explorer

Theorem ftc1lem2

Description: Lemma for ftc1 . (Contributed by Mario Carneiro, 12-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 )
Assertion ftc1lem2 
|- ( ph -> G : ( A [,] B ) --> CC )

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 fvexd 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ t e. ( A (,) x ) ) -> ( F ` t ) e. _V )
10 3 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> B e. RR )
11 10 rexrd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> B e. RR* )
12 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
13 2 3 12 syl2anc 
 |-  ( ph -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
14 13 biimpa 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( x e. RR /\ A <_ x /\ x <_ B ) )
15 14 simp3d 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x <_ B )
16 iooss2 
 |-  ( ( B e. RR* /\ x <_ B ) -> ( A (,) x ) C_ ( A (,) B ) )
17 11 15 16 syl2anc 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( A (,) x ) C_ ( A (,) B ) )
18 5 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( A (,) B ) C_ D )
19 17 18 sstrd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( A (,) x ) C_ D )
20 ioombl 
 |-  ( A (,) x ) e. dom vol
21 20 a1i 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( A (,) x ) e. dom vol )
22 fvexd 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ t e. D ) -> ( F ` t ) e. _V )
23 8 feqmptd 
 |-  ( ph -> F = ( t e. D |-> ( F ` t ) ) )
24 23 7 eqeltrrd 
 |-  ( ph -> ( t e. D |-> ( F ` t ) ) e. L^1 )
25 24 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( t e. D |-> ( F ` t ) ) e. L^1 )
26 19 21 22 25 iblss 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( t e. ( A (,) x ) |-> ( F ` t ) ) e. L^1 )
27 9 26 itgcl 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> S. ( A (,) x ) ( F ` t ) _d t e. CC )
28 27 1 fmptd 
 |-  ( ph -> G : ( A [,] B ) --> CC )