Metamath Proof Explorer

Theorem itgulm2

Description: A uniform limit of integrals of integrable functions converges to the integral of the limit function. (Contributed by Mario Carneiro, 18-Mar-2015)

Ref Expression
Hypotheses itgulm2.z 
|- Z = ( ZZ>= ` M )
itgulm2.m 
|- ( ph -> M e. ZZ )
itgulm2.l 
|- ( ( ph /\ k e. Z ) -> ( x e. S |-> A ) e. L^1 )
itgulm2.u 
|- ( ph -> ( k e. Z |-> ( x e. S |-> A ) ) ( ~~>u ` S ) ( x e. S |-> B ) )
itgulm2.s 
|- ( ph -> ( vol ` S ) e. RR )
Assertion itgulm2 
|- ( ph -> ( ( x e. S |-> B ) e. L^1 /\ ( k e. Z |-> S. S A _d x ) ~~> S. S B _d x ) )

Proof

Step Hyp Ref Expression
1 itgulm2.z 
 |-  Z = ( ZZ>= ` M )
2 itgulm2.m 
 |-  ( ph -> M e. ZZ )
3 itgulm2.l 
 |-  ( ( ph /\ k e. Z ) -> ( x e. S |-> A ) e. L^1 )
4 itgulm2.u 
 |-  ( ph -> ( k e. Z |-> ( x e. S |-> A ) ) ( ~~>u ` S ) ( x e. S |-> B ) )
5 itgulm2.s 
 |-  ( ph -> ( vol ` S ) e. RR )
6 3 fmpttd 
 |-  ( ph -> ( k e. Z |-> ( x e. S |-> A ) ) : Z --> L^1 )
7 1 2 6 4 5 iblulm 
 |-  ( ph -> ( x e. S |-> B ) e. L^1 )
8 1 2 6 4 5 itgulm 
 |-  ( ph -> ( n e. Z |-> S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` z ) _d z ) ~~> S. S ( ( x e. S |-> B ) ` z ) _d z )
9 nfcv 
 |-  F/_ k S
10 nffvmpt1 
 |-  F/_ k ( ( k e. Z |-> ( x e. S |-> A ) ) ` n )
11 nfcv 
 |-  F/_ k z
12 10 11 nffv 
 |-  F/_ k ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` z )
13 9 12 nfitg 
 |-  F/_ k S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` z ) _d z
14 nfcv 
 |-  F/_ n S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) ` x ) _d x
15 fveq2 
 |-  ( z = x -> ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` z ) = ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` x ) )
16 nfcv 
 |-  F/_ x Z
17 nfmpt1 
 |-  F/_ x ( x e. S |-> A )
18 16 17 nfmpt 
 |-  F/_ x ( k e. Z |-> ( x e. S |-> A ) )
19 nfcv 
 |-  F/_ x n
20 18 19 nffv 
 |-  F/_ x ( ( k e. Z |-> ( x e. S |-> A ) ) ` n )
21 nfcv 
 |-  F/_ x z
22 20 21 nffv 
 |-  F/_ x ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` z )
23 nfcv 
 |-  F/_ z ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` x )
24 15 22 23 cbvitg 
 |-  S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` z ) _d z = S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` x ) _d x
25 fveq2 
 |-  ( n = k -> ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) = ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) )
26 25 fveq1d 
 |-  ( n = k -> ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` x ) = ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) ` x ) )
27 26 adantr 
 |-  ( ( n = k /\ x e. S ) -> ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` x ) = ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) ` x ) )
28 27 itgeq2dv 
 |-  ( n = k -> S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` x ) _d x = S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) ` x ) _d x )
29 24 28 syl5eq 
 |-  ( n = k -> S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` z ) _d z = S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) ` x ) _d x )
30 13 14 29 cbvmpt 
 |-  ( n e. Z |-> S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` z ) _d z ) = ( k e. Z |-> S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) ` x ) _d x )
31 simplr 
 |-  ( ( ( ph /\ k e. Z ) /\ x e. S ) -> k e. Z )
32 ulmscl 
 |-  ( ( k e. Z |-> ( x e. S |-> A ) ) ( ~~>u ` S ) ( x e. S |-> B ) -> S e. _V )
33 mptexg 
 |-  ( S e. _V -> ( x e. S |-> A ) e. _V )
34 4 32 33 3syl 
 |-  ( ph -> ( x e. S |-> A ) e. _V )
35 34 ad2antrr 
 |-  ( ( ( ph /\ k e. Z ) /\ x e. S ) -> ( x e. S |-> A ) e. _V )
36 eqid 
 |-  ( k e. Z |-> ( x e. S |-> A ) ) = ( k e. Z |-> ( x e. S |-> A ) )
37 36 fvmpt2 
 |-  ( ( k e. Z /\ ( x e. S |-> A ) e. _V ) -> ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) = ( x e. S |-> A ) )
38 31 35 37 syl2anc 
 |-  ( ( ( ph /\ k e. Z ) /\ x e. S ) -> ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) = ( x e. S |-> A ) )
39 38 fveq1d 
 |-  ( ( ( ph /\ k e. Z ) /\ x e. S ) -> ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) ` x ) = ( ( x e. S |-> A ) ` x ) )
40 simpr 
 |-  ( ( ( ph /\ k e. Z ) /\ x e. S ) -> x e. S )
41 34 ralrimivw 
 |-  ( ph -> A. k e. Z ( x e. S |-> A ) e. _V )
42 36 fnmpt 
 |-  ( A. k e. Z ( x e. S |-> A ) e. _V -> ( k e. Z |-> ( x e. S |-> A ) ) Fn Z )
43 41 42 syl 
 |-  ( ph -> ( k e. Z |-> ( x e. S |-> A ) ) Fn Z )
44 ulmf2 
 |-  ( ( ( k e. Z |-> ( x e. S |-> A ) ) Fn Z /\ ( k e. Z |-> ( x e. S |-> A ) ) ( ~~>u ` S ) ( x e. S |-> B ) ) -> ( k e. Z |-> ( x e. S |-> A ) ) : Z --> ( CC ^m S ) )
45 43 4 44 syl2anc 
 |-  ( ph -> ( k e. Z |-> ( x e. S |-> A ) ) : Z --> ( CC ^m S ) )
46 45 fvmptelrn 
 |-  ( ( ph /\ k e. Z ) -> ( x e. S |-> A ) e. ( CC ^m S ) )
47 elmapi 
 |-  ( ( x e. S |-> A ) e. ( CC ^m S ) -> ( x e. S |-> A ) : S --> CC )
48 46 47 syl 
 |-  ( ( ph /\ k e. Z ) -> ( x e. S |-> A ) : S --> CC )
49 48 fvmptelrn 
 |-  ( ( ( ph /\ k e. Z ) /\ x e. S ) -> A e. CC )
50 eqid 
 |-  ( x e. S |-> A ) = ( x e. S |-> A )
51 50 fvmpt2 
 |-  ( ( x e. S /\ A e. CC ) -> ( ( x e. S |-> A ) ` x ) = A )
52 40 49 51 syl2anc 
 |-  ( ( ( ph /\ k e. Z ) /\ x e. S ) -> ( ( x e. S |-> A ) ` x ) = A )
53 39 52 eqtrd 
 |-  ( ( ( ph /\ k e. Z ) /\ x e. S ) -> ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) ` x ) = A )
54 53 itgeq2dv 
 |-  ( ( ph /\ k e. Z ) -> S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) ` x ) _d x = S. S A _d x )
55 54 mpteq2dva 
 |-  ( ph -> ( k e. Z |-> S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) ` x ) _d x ) = ( k e. Z |-> S. S A _d x ) )
56 30 55 syl5eq 
 |-  ( ph -> ( n e. Z |-> S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` z ) _d z ) = ( k e. Z |-> S. S A _d x ) )
57 fveq2 
 |-  ( z = x -> ( ( x e. S |-> B ) ` z ) = ( ( x e. S |-> B ) ` x ) )
58 nffvmpt1 
 |-  F/_ x ( ( x e. S |-> B ) ` z )
59 nfcv 
 |-  F/_ z ( ( x e. S |-> B ) ` x )
60 57 58 59 cbvitg 
 |-  S. S ( ( x e. S |-> B ) ` z ) _d z = S. S ( ( x e. S |-> B ) ` x ) _d x
61 simpr 
 |-  ( ( ph /\ x e. S ) -> x e. S )
62 ulmcl 
 |-  ( ( k e. Z |-> ( x e. S |-> A ) ) ( ~~>u ` S ) ( x e. S |-> B ) -> ( x e. S |-> B ) : S --> CC )
63 4 62 syl 
 |-  ( ph -> ( x e. S |-> B ) : S --> CC )
64 63 fvmptelrn 
 |-  ( ( ph /\ x e. S ) -> B e. CC )
65 eqid 
 |-  ( x e. S |-> B ) = ( x e. S |-> B )
66 65 fvmpt2 
 |-  ( ( x e. S /\ B e. CC ) -> ( ( x e. S |-> B ) ` x ) = B )
67 61 64 66 syl2anc 
 |-  ( ( ph /\ x e. S ) -> ( ( x e. S |-> B ) ` x ) = B )
68 67 itgeq2dv 
 |-  ( ph -> S. S ( ( x e. S |-> B ) ` x ) _d x = S. S B _d x )
69 60 68 syl5eq 
 |-  ( ph -> S. S ( ( x e. S |-> B ) ` z ) _d z = S. S B _d x )
70 8 56 69 3brtr3d 
 |-  ( ph -> ( k e. Z |-> S. S A _d x ) ~~> S. S B _d x )
71 7 70 jca 
 |-  ( ph -> ( ( x e. S |-> B ) e. L^1 /\ ( k e. Z |-> S. S A _d x ) ~~> S. S B _d x ) )