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	eqtrid	\|- ( 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	fvmptelcdm	\|- ( ( 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	fvmptelcdm	\|- ( ( ( 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	eqtrid	\|- ( 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	fvmptelcdm	\|- ( ( 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	eqtrid	\|- ( 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 ) )

Metamath Proof Explorer

Theorem itgulm2

Proof