This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid 
 |-  ( 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 ffvelcdmda 
 |-  ( ( 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 ffvelcdmda 
 |-  ( ( 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 ffvelcdmda 
 |-  ( ( ( 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 ffvelcdm 
 |-  ( ( 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* , < ) )