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 ) )