Theorem itg2i1fseq

Description: Subject to the conditions coming from mbfi1fseq , the integral of the sequence of simple functions converges to the integral of the target function. (Contributed by Mario Carneiro, 17-Aug-2014)

	Ref	Expression
Hypotheses	itg2i1fseq.1	|- ( ph -> F e. MblFn )
	itg2i1fseq.2	|- ( ph -> F : RR --> ( 0 [,) +oo ) )
	itg2i1fseq.3	|- ( ph -> P : NN --> dom S.1 )
	itg2i1fseq.4	|- ( ph -> A. n e. NN ( 0p oR <_ ( P ` n ) /\ ( P ` n ) oR <_ ( P ` ( n + 1 ) ) ) )
	itg2i1fseq.5	|- ( ph -> A. x e. RR ( n e. NN |-> ( ( P ` n ) ` x ) ) ~~> ( F ` x ) )
	itg2i1fseq.6	|- S = ( m e. NN |-> ( S.1 ` ( P ` m ) ) )
Assertion	itg2i1fseq	|- ( ph -> ( S.2 ` F ) = sup ( ran S , RR* , < ) )

Proof

Step	Hyp	Ref	Expression
1		itg2i1fseq.1	|- ( ph -> F e. MblFn )
2		itg2i1fseq.2	|- ( ph -> F : RR --> ( 0 [,) +oo ) )
3		itg2i1fseq.3	|- ( ph -> P : NN --> dom S.1 )
4		itg2i1fseq.4	|- ( ph -> A. n e. NN ( 0p oR <_ ( P ` n ) /\ ( P ` n ) oR <_ ( P ` ( n + 1 ) ) ) )
5		itg2i1fseq.5	|- ( ph -> A. x e. RR ( n e. NN |-> ( ( P ` n ) ` x ) ) ~~> ( F ` x ) )
6		itg2i1fseq.6	|- S = ( m e. NN |-> ( S.1 ` ( P ` m ) ) )
7		fveq2	|- ( n = m -> ( P ` n ) = ( P ` m ) )
8	7	fveq1d	|- ( n = m -> ( ( P ` n ) ` x ) = ( ( P ` m ) ` x ) )
9	8	cbvmptv	|- ( n e. NN |-> ( ( P ` n ) ` x ) ) = ( m e. NN |-> ( ( P ` m ) ` x ) )
10		fveq2	|- ( x = y -> ( ( P ` m ) ` x ) = ( ( P ` m ) ` y ) )
11	10	mpteq2dv	|- ( x = y -> ( m e. NN |-> ( ( P ` m ) ` x ) ) = ( m e. NN |-> ( ( P ` m ) ` y ) ) )
12	9 11	syl5eq	|- ( x = y -> ( n e. NN |-> ( ( P ` n ) ` x ) ) = ( m e. NN |-> ( ( P ` m ) ` y ) ) )
13	12	rneqd	|- ( x = y -> ran ( n e. NN |-> ( ( P ` n ) ` x ) ) = ran ( m e. NN |-> ( ( P ` m ) ` y ) ) )
14	13	supeq1d	|- ( x = y -> sup ( ran ( n e. NN |-> ( ( P ` n ) ` x ) ) , RR , < ) = sup ( ran ( m e. NN |-> ( ( P ` m ) ` y ) ) , RR , < ) )
15	14	cbvmptv	|- ( x e. RR |-> sup ( ran ( n e. NN |-> ( ( P ` n ) ` x ) ) , RR , < ) ) = ( y e. RR |-> sup ( ran ( m e. NN |-> ( ( P ` m ) ` y ) ) , RR , < ) )
16	3	ffvelrnda	|- ( ( ph /\ m e. NN ) -> ( P ` m ) e. dom S.1 )
17		i1fmbf	|- ( ( P ` m ) e. dom S.1 -> ( P ` m ) e. MblFn )
18	16 17	syl	|- ( ( ph /\ m e. NN ) -> ( P ` m ) e. MblFn )
19		i1ff	|- ( ( P ` m ) e. dom S.1 -> ( P ` m ) : RR --> RR )
20	16 19	syl	|- ( ( ph /\ m e. NN ) -> ( P ` m ) : RR --> RR )
21	7	breq2d	|- ( n = m -> ( 0p oR <_ ( P ` n ) <-> 0p oR <_ ( P ` m ) ) )
22		fvoveq1	|- ( n = m -> ( P ` ( n + 1 ) ) = ( P ` ( m + 1 ) ) )
23	7 22	breq12d	|- ( n = m -> ( ( P ` n ) oR <_ ( P ` ( n + 1 ) ) <-> ( P ` m ) oR <_ ( P ` ( m + 1 ) ) ) )
24	21 23	anbi12d	|- ( n = m -> ( ( 0p oR <_ ( P ` n ) /\ ( P ` n ) oR <_ ( P ` ( n + 1 ) ) ) <-> ( 0p oR <_ ( P ` m ) /\ ( P ` m ) oR <_ ( P ` ( m + 1 ) ) ) ) )
25	24	rspccva	|- ( ( A. n e. NN ( 0p oR <_ ( P ` n ) /\ ( P ` n ) oR <_ ( P ` ( n + 1 ) ) ) /\ m e. NN ) -> ( 0p oR <_ ( P ` m ) /\ ( P ` m ) oR <_ ( P ` ( m + 1 ) ) ) )
26	4 25	sylan	|- ( ( ph /\ m e. NN ) -> ( 0p oR <_ ( P ` m ) /\ ( P ` m ) oR <_ ( P ` ( m + 1 ) ) ) )
27	26	simpld	|- ( ( ph /\ m e. NN ) -> 0p oR <_ ( P ` m ) )
28		0plef	|- ( ( P ` m ) : RR --> ( 0 [,) +oo ) <-> ( ( P ` m ) : RR --> RR /\ 0p oR <_ ( P ` m ) ) )
29	20 27 28	sylanbrc	|- ( ( ph /\ m e. NN ) -> ( P ` m ) : RR --> ( 0 [,) +oo ) )
30	26	simprd	|- ( ( ph /\ m e. NN ) -> ( P ` m ) oR <_ ( P ` ( m + 1 ) ) )
31		rge0ssre	|- ( 0 [,) +oo ) C_ RR
32	2	ffvelrnda	|- ( ( ph /\ y e. RR ) -> ( F ` y ) e. ( 0 [,) +oo ) )
33	31 32	sselid	|- ( ( ph /\ y e. RR ) -> ( F ` y ) e. RR )
34	1 2 3 4 5	itg2i1fseqle	|- ( ( ph /\ m e. NN ) -> ( P ` m ) oR <_ F )
35	20	ffnd	|- ( ( ph /\ m e. NN ) -> ( P ` m ) Fn RR )
36	2	ffnd	|- ( ph -> F Fn RR )
37	36	adantr	|- ( ( ph /\ m e. NN ) -> F Fn RR )
38		reex	|- RR e. _V
39	38	a1i	|- ( ( ph /\ m e. NN ) -> RR e. _V )
40		inidm	|- ( RR i^i RR ) = RR
41		eqidd	|- ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> ( ( P ` m ) ` y ) = ( ( P ` m ) ` y ) )
42		eqidd	|- ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> ( F ` y ) = ( F ` y ) )
43	35 37 39 39 40 41 42	ofrfval	|- ( ( ph /\ m e. NN ) -> ( ( P ` m ) oR <_ F <-> A. y e. RR ( ( P ` m ) ` y ) <_ ( F ` y ) ) )
44	34 43	mpbid	|- ( ( ph /\ m e. NN ) -> A. y e. RR ( ( P ` m ) ` y ) <_ ( F ` y ) )
45	44	r19.21bi	|- ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> ( ( P ` m ) ` y ) <_ ( F ` y ) )
46	45	an32s	|- ( ( ( ph /\ y e. RR ) /\ m e. NN ) -> ( ( P ` m ) ` y ) <_ ( F ` y ) )
47	46	ralrimiva	|- ( ( ph /\ y e. RR ) -> A. m e. NN ( ( P ` m ) ` y ) <_ ( F ` y ) )
48		brralrspcev	|- ( ( ( F ` y ) e. RR /\ A. m e. NN ( ( P ` m ) ` y ) <_ ( F ` y ) ) -> E. z e. RR A. m e. NN ( ( P ` m ) ` y ) <_ z )
49	33 47 48	syl2anc	|- ( ( ph /\ y e. RR ) -> E. z e. RR A. m e. NN ( ( P ` m ) ` y ) <_ z )
50	7	fveq2d	|- ( n = m -> ( S.2 ` ( P ` n ) ) = ( S.2 ` ( P ` m ) ) )
51	50	cbvmptv	|- ( n e. NN |-> ( S.2 ` ( P ` n ) ) ) = ( m e. NN |-> ( S.2 ` ( P ` m ) ) )
52	51	rneqi	|- ran ( n e. NN |-> ( S.2 ` ( P ` n ) ) ) = ran ( m e. NN |-> ( S.2 ` ( P ` m ) ) )
53	52	supeq1i	|- sup ( ran ( n e. NN |-> ( S.2 ` ( P ` n ) ) ) , RR* , < ) = sup ( ran ( m e. NN |-> ( S.2 ` ( P ` m ) ) ) , RR* , < )
54	15 18 29 30 49 53	itg2mono	|- ( ph -> ( S.2 ` ( x e. RR |-> sup ( ran ( n e. NN |-> ( ( P ` n ) ` x ) ) , RR , < ) ) ) = sup ( ran ( n e. NN |-> ( S.2 ` ( P ` n ) ) ) , RR* , < ) )
55	2	feqmptd	|- ( ph -> F = ( y e. RR |-> ( F ` y ) ) )
56	7	fveq1d	|- ( n = m -> ( ( P ` n ) ` y ) = ( ( P ` m ) ` y ) )
57	56	cbvmptv	|- ( n e. NN |-> ( ( P ` n ) ` y ) ) = ( m e. NN |-> ( ( P ` m ) ` y ) )
58	57	rneqi	|- ran ( n e. NN |-> ( ( P ` n ) ` y ) ) = ran ( m e. NN |-> ( ( P ` m ) ` y ) )
59	58	supeq1i	|- sup ( ran ( n e. NN |-> ( ( P ` n ) ` y ) ) , RR , < ) = sup ( ran ( m e. NN |-> ( ( P ` m ) ` y ) ) , RR , < )
60		nnuz	|- NN = ( ZZ>= ` 1 )
61		1zzd	|- ( ( ph /\ y e. RR ) -> 1 e. ZZ )
62	20	ffvelrnda	|- ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> ( ( P ` m ) ` y ) e. RR )
63	62	an32s	|- ( ( ( ph /\ y e. RR ) /\ m e. NN ) -> ( ( P ` m ) ` y ) e. RR )
64	63 57	fmptd	|- ( ( ph /\ y e. RR ) -> ( n e. NN |-> ( ( P ` n ) ` y ) ) : NN --> RR )
65		peano2nn	|- ( m e. NN -> ( m + 1 ) e. NN )
66		ffvelrn	|- ( ( P : NN --> dom S.1 /\ ( m + 1 ) e. NN ) -> ( P ` ( m + 1 ) ) e. dom S.1 )
67	3 65 66	syl2an	|- ( ( ph /\ m e. NN ) -> ( P ` ( m + 1 ) ) e. dom S.1 )
68		i1ff	|- ( ( P ` ( m + 1 ) ) e. dom S.1 -> ( P ` ( m + 1 ) ) : RR --> RR )
69	67 68	syl	|- ( ( ph /\ m e. NN ) -> ( P ` ( m + 1 ) ) : RR --> RR )
70	69	ffnd	|- ( ( ph /\ m e. NN ) -> ( P ` ( m + 1 ) ) Fn RR )
71		eqidd	|- ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> ( ( P ` ( m + 1 ) ) ` y ) = ( ( P ` ( m + 1 ) ) ` y ) )
72	35 70 39 39 40 41 71	ofrfval	|- ( ( ph /\ m e. NN ) -> ( ( P ` m ) oR <_ ( P ` ( m + 1 ) ) <-> A. y e. RR ( ( P ` m ) ` y ) <_ ( ( P ` ( m + 1 ) ) ` y ) ) )
73	30 72	mpbid	|- ( ( ph /\ m e. NN ) -> A. y e. RR ( ( P ` m ) ` y ) <_ ( ( P ` ( m + 1 ) ) ` y ) )
74	73	r19.21bi	|- ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> ( ( P ` m ) ` y ) <_ ( ( P ` ( m + 1 ) ) ` y ) )
75	74	an32s	|- ( ( ( ph /\ y e. RR ) /\ m e. NN ) -> ( ( P ` m ) ` y ) <_ ( ( P ` ( m + 1 ) ) ` y ) )
76		eqid	|- ( n e. NN |-> ( ( P ` n ) ` y ) ) = ( n e. NN |-> ( ( P ` n ) ` y ) )
77		fvex	|- ( ( P ` m ) ` y ) e. _V
78	56 76 77	fvmpt	|- ( m e. NN -> ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` m ) = ( ( P ` m ) ` y ) )
79	78	adantl	|- ( ( ( ph /\ y e. RR ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` m ) = ( ( P ` m ) ` y ) )
80		fveq2	|- ( n = ( m + 1 ) -> ( P ` n ) = ( P ` ( m + 1 ) ) )
81	80	fveq1d	|- ( n = ( m + 1 ) -> ( ( P ` n ) ` y ) = ( ( P ` ( m + 1 ) ) ` y ) )
82		fvex	|- ( ( P ` ( m + 1 ) ) ` y ) e. _V
83	81 76 82	fvmpt	|- ( ( m + 1 ) e. NN -> ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` ( m + 1 ) ) = ( ( P ` ( m + 1 ) ) ` y ) )
84	65 83	syl	|- ( m e. NN -> ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` ( m + 1 ) ) = ( ( P ` ( m + 1 ) ) ` y ) )
85	84	adantl	|- ( ( ( ph /\ y e. RR ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` ( m + 1 ) ) = ( ( P ` ( m + 1 ) ) ` y ) )
86	75 79 85	3brtr4d	|- ( ( ( ph /\ y e. RR ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` m ) <_ ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` ( m + 1 ) ) )
87	78	breq1d	|- ( m e. NN -> ( ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` m ) <_ z <-> ( ( P ` m ) ` y ) <_ z ) )
88	87	ralbiia	|- ( A. m e. NN ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` m ) <_ z <-> A. m e. NN ( ( P ` m ) ` y ) <_ z )
89	88	rexbii	|- ( E. z e. RR A. m e. NN ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` m ) <_ z <-> E. z e. RR A. m e. NN ( ( P ` m ) ` y ) <_ z )
90	49 89	sylibr	|- ( ( ph /\ y e. RR ) -> E. z e. RR A. m e. NN ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` m ) <_ z )
91	60 61 64 86 90	climsup	|- ( ( ph /\ y e. RR ) -> ( n e. NN |-> ( ( P ` n ) ` y ) ) ~~> sup ( ran ( n e. NN |-> ( ( P ` n ) ` y ) ) , RR , < ) )
92		fveq2	|- ( x = y -> ( ( P ` n ) ` x ) = ( ( P ` n ) ` y ) )
93	92	mpteq2dv	|- ( x = y -> ( n e. NN |-> ( ( P ` n ) ` x ) ) = ( n e. NN |-> ( ( P ` n ) ` y ) ) )
94		fveq2	|- ( x = y -> ( F ` x ) = ( F ` y ) )
95	93 94	breq12d	|- ( x = y -> ( ( n e. NN |-> ( ( P ` n ) ` x ) ) ~~> ( F ` x ) <-> ( n e. NN |-> ( ( P ` n ) ` y ) ) ~~> ( F ` y ) ) )
96	95	rspccva	|- ( ( A. x e. RR ( n e. NN |-> ( ( P ` n ) ` x ) ) ~~> ( F ` x ) /\ y e. RR ) -> ( n e. NN |-> ( ( P ` n ) ` y ) ) ~~> ( F ` y ) )
97	5 96	sylan	|- ( ( ph /\ y e. RR ) -> ( n e. NN |-> ( ( P ` n ) ` y ) ) ~~> ( F ` y ) )
98		climuni	|- ( ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ~~> sup ( ran ( n e. NN |-> ( ( P ` n ) ` y ) ) , RR , < ) /\ ( n e. NN |-> ( ( P ` n ) ` y ) ) ~~> ( F ` y ) ) -> sup ( ran ( n e. NN |-> ( ( P ` n ) ` y ) ) , RR , < ) = ( F ` y ) )
99	91 97 98	syl2anc	|- ( ( ph /\ y e. RR ) -> sup ( ran ( n e. NN |-> ( ( P ` n ) ` y ) ) , RR , < ) = ( F ` y ) )
100	59 99	eqtr3id	|- ( ( ph /\ y e. RR ) -> sup ( ran ( m e. NN |-> ( ( P ` m ) ` y ) ) , RR , < ) = ( F ` y ) )
101	100	mpteq2dva	|- ( ph -> ( y e. RR |-> sup ( ran ( m e. NN |-> ( ( P ` m ) ` y ) ) , RR , < ) ) = ( y e. RR |-> ( F ` y ) ) )
102	55 101	eqtr4d	|- ( ph -> F = ( y e. RR |-> sup ( ran ( m e. NN |-> ( ( P ` m ) ` y ) ) , RR , < ) ) )
103	102 15	eqtr4di	|- ( ph -> F = ( x e. RR |-> sup ( ran ( n e. NN |-> ( ( P ` n ) ` x ) ) , RR , < ) ) )
104	103	fveq2d	|- ( ph -> ( S.2 ` F ) = ( S.2 ` ( x e. RR |-> sup ( ran ( n e. NN |-> ( ( P ` n ) ` x ) ) , RR , < ) ) ) )
105		itg2itg1	|- ( ( ( P ` m ) e. dom S.1 /\ 0p oR <_ ( P ` m ) ) -> ( S.2 ` ( P ` m ) ) = ( S.1 ` ( P ` m ) ) )
106	16 27 105	syl2anc	|- ( ( ph /\ m e. NN ) -> ( S.2 ` ( P ` m ) ) = ( S.1 ` ( P ` m ) ) )
107	106	mpteq2dva	|- ( ph -> ( m e. NN |-> ( S.2 ` ( P ` m ) ) ) = ( m e. NN |-> ( S.1 ` ( P ` m ) ) ) )
108	6 107	eqtr4id	|- ( ph -> S = ( m e. NN |-> ( S.2 ` ( P ` m ) ) ) )
109	108 51	eqtr4di	|- ( ph -> S = ( n e. NN |-> ( S.2 ` ( P ` n ) ) ) )
110	109	rneqd	|- ( ph -> ran S = ran ( n e. NN |-> ( S.2 ` ( P ` n ) ) ) )
111	110	supeq1d	|- ( ph -> sup ( ran S , RR* , < ) = sup ( ran ( n e. NN |-> ( S.2 ` ( P ` n ) ) ) , RR* , < ) )
112	54 104 111	3eqtr4d	|- ( ph -> ( S.2 ` F ) = sup ( ran S , RR* , < ) )