Metamath Proof Explorer

Theorem caratheodorylem1

Description: Lemma used to prove that Caratheodory's construction is sigma-additive. This is the proof of the statement in the middle of Step (e) in the proof of Theorem 113C of Fremlin1 p. 21. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses caratheodorylem1.o 
|- ( ph -> O e. OutMeas )
caratheodorylem1.s 
|- S = ( CaraGen ` O )
caratheodorylem1.z 
|- Z = ( ZZ>= ` M )
caratheodorylem1.e 
|- ( ph -> E : Z --> S )
caratheodorylem1.dj 
|- ( ph -> Disj_ n e. Z ( E ` n ) )
caratheodorylem1.g 
|- G = ( n e. Z |-> U_ i e. ( M ... n ) ( E ` i ) )
caratheodorylem1.n 
|- ( ph -> N e. ( ZZ>= ` M ) )
Assertion caratheodorylem1 
|- ( ph -> ( O ` ( G ` N ) ) = ( sum^ ` ( n e. ( M ... N ) |-> ( O ` ( E ` n ) ) ) ) )

Proof

Step Hyp Ref Expression
1 caratheodorylem1.o 
 |-  ( ph -> O e. OutMeas )
2 caratheodorylem1.s 
 |-  S = ( CaraGen ` O )
3 caratheodorylem1.z 
 |-  Z = ( ZZ>= ` M )
4 caratheodorylem1.e 
 |-  ( ph -> E : Z --> S )
5 caratheodorylem1.dj 
 |-  ( ph -> Disj_ n e. Z ( E ` n ) )
6 caratheodorylem1.g 
 |-  G = ( n e. Z |-> U_ i e. ( M ... n ) ( E ` i ) )
7 caratheodorylem1.n 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
8 eluzfz2 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
9 7 8 syl 
 |-  ( ph -> N e. ( M ... N ) )
10 id 
 |-  ( ph -> ph )
11 2fveq3 
 |-  ( j = M -> ( O ` ( G ` j ) ) = ( O ` ( G ` M ) ) )
12 oveq2 
 |-  ( j = M -> ( M ... j ) = ( M ... M ) )
13 12 mpteq1d 
 |-  ( j = M -> ( n e. ( M ... j ) |-> ( O ` ( E ` n ) ) ) = ( n e. ( M ... M ) |-> ( O ` ( E ` n ) ) ) )
14 13 fveq2d 
 |-  ( j = M -> ( sum^ ` ( n e. ( M ... j ) |-> ( O ` ( E ` n ) ) ) ) = ( sum^ ` ( n e. ( M ... M ) |-> ( O ` ( E ` n ) ) ) ) )
15 11 14 eqeq12d 
 |-  ( j = M -> ( ( O ` ( G ` j ) ) = ( sum^ ` ( n e. ( M ... j ) |-> ( O ` ( E ` n ) ) ) ) <-> ( O ` ( G ` M ) ) = ( sum^ ` ( n e. ( M ... M ) |-> ( O ` ( E ` n ) ) ) ) ) )
16 15 imbi2d 
 |-  ( j = M -> ( ( ph -> ( O ` ( G ` j ) ) = ( sum^ ` ( n e. ( M ... j ) |-> ( O ` ( E ` n ) ) ) ) ) <-> ( ph -> ( O ` ( G ` M ) ) = ( sum^ ` ( n e. ( M ... M ) |-> ( O ` ( E ` n ) ) ) ) ) ) )
17 2fveq3 
 |-  ( j = i -> ( O ` ( G ` j ) ) = ( O ` ( G ` i ) ) )
18 oveq2 
 |-  ( j = i -> ( M ... j ) = ( M ... i ) )
19 18 mpteq1d 
 |-  ( j = i -> ( n e. ( M ... j ) |-> ( O ` ( E ` n ) ) ) = ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) )
20 19 fveq2d 
 |-  ( j = i -> ( sum^ ` ( n e. ( M ... j ) |-> ( O ` ( E ` n ) ) ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) )
21 17 20 eqeq12d 
 |-  ( j = i -> ( ( O ` ( G ` j ) ) = ( sum^ ` ( n e. ( M ... j ) |-> ( O ` ( E ` n ) ) ) ) <-> ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) ) )
22 21 imbi2d 
 |-  ( j = i -> ( ( ph -> ( O ` ( G ` j ) ) = ( sum^ ` ( n e. ( M ... j ) |-> ( O ` ( E ` n ) ) ) ) ) <-> ( ph -> ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) ) ) )
23 2fveq3 
 |-  ( j = ( i + 1 ) -> ( O ` ( G ` j ) ) = ( O ` ( G ` ( i + 1 ) ) ) )
24 oveq2 
 |-  ( j = ( i + 1 ) -> ( M ... j ) = ( M ... ( i + 1 ) ) )
25 24 mpteq1d 
 |-  ( j = ( i + 1 ) -> ( n e. ( M ... j ) |-> ( O ` ( E ` n ) ) ) = ( n e. ( M ... ( i + 1 ) ) |-> ( O ` ( E ` n ) ) ) )
26 25 fveq2d 
 |-  ( j = ( i + 1 ) -> ( sum^ ` ( n e. ( M ... j ) |-> ( O ` ( E ` n ) ) ) ) = ( sum^ ` ( n e. ( M ... ( i + 1 ) ) |-> ( O ` ( E ` n ) ) ) ) )
27 23 26 eqeq12d 
 |-  ( j = ( i + 1 ) -> ( ( O ` ( G ` j ) ) = ( sum^ ` ( n e. ( M ... j ) |-> ( O ` ( E ` n ) ) ) ) <-> ( O ` ( G ` ( i + 1 ) ) ) = ( sum^ ` ( n e. ( M ... ( i + 1 ) ) |-> ( O ` ( E ` n ) ) ) ) ) )
28 27 imbi2d 
 |-  ( j = ( i + 1 ) -> ( ( ph -> ( O ` ( G ` j ) ) = ( sum^ ` ( n e. ( M ... j ) |-> ( O ` ( E ` n ) ) ) ) ) <-> ( ph -> ( O ` ( G ` ( i + 1 ) ) ) = ( sum^ ` ( n e. ( M ... ( i + 1 ) ) |-> ( O ` ( E ` n ) ) ) ) ) ) )
29 2fveq3 
 |-  ( j = N -> ( O ` ( G ` j ) ) = ( O ` ( G ` N ) ) )
30 oveq2 
 |-  ( j = N -> ( M ... j ) = ( M ... N ) )
31 30 mpteq1d 
 |-  ( j = N -> ( n e. ( M ... j ) |-> ( O ` ( E ` n ) ) ) = ( n e. ( M ... N ) |-> ( O ` ( E ` n ) ) ) )
32 31 fveq2d 
 |-  ( j = N -> ( sum^ ` ( n e. ( M ... j ) |-> ( O ` ( E ` n ) ) ) ) = ( sum^ ` ( n e. ( M ... N ) |-> ( O ` ( E ` n ) ) ) ) )
33 29 32 eqeq12d 
 |-  ( j = N -> ( ( O ` ( G ` j ) ) = ( sum^ ` ( n e. ( M ... j ) |-> ( O ` ( E ` n ) ) ) ) <-> ( O ` ( G ` N ) ) = ( sum^ ` ( n e. ( M ... N ) |-> ( O ` ( E ` n ) ) ) ) ) )
34 33 imbi2d 
 |-  ( j = N -> ( ( ph -> ( O ` ( G ` j ) ) = ( sum^ ` ( n e. ( M ... j ) |-> ( O ` ( E ` n ) ) ) ) ) <-> ( ph -> ( O ` ( G ` N ) ) = ( sum^ ` ( n e. ( M ... N ) |-> ( O ` ( E ` n ) ) ) ) ) ) )
35 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
36 7 35 syl 
 |-  ( ph -> M e. ZZ )
37 fzsn 
 |-  ( M e. ZZ -> ( M ... M ) = { M } )
38 36 37 syl 
 |-  ( ph -> ( M ... M ) = { M } )
39 38 mpteq1d 
 |-  ( ph -> ( n e. ( M ... M ) |-> ( O ` ( E ` n ) ) ) = ( n e. { M } |-> ( O ` ( E ` n ) ) ) )
40 39 fveq2d 
 |-  ( ph -> ( sum^ ` ( n e. ( M ... M ) |-> ( O ` ( E ` n ) ) ) ) = ( sum^ ` ( n e. { M } |-> ( O ` ( E ` n ) ) ) ) )
41 1 adantr 
 |-  ( ( ph /\ n e. { M } ) -> O e. OutMeas )
42 eqid 
 |-  U. dom O = U. dom O
43 2 caragenss 
 |-  ( O e. OutMeas -> S C_ dom O )
44 41 43 syl 
 |-  ( ( ph /\ n e. { M } ) -> S C_ dom O )
45 4 adantr 
 |-  ( ( ph /\ n e. { M } ) -> E : Z --> S )
46 elsni 
 |-  ( n e. { M } -> n = M )
47 46 adantl 
 |-  ( ( ph /\ n e. { M } ) -> n = M )
48 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
49 36 48 syl 
 |-  ( ph -> M e. ( ZZ>= ` M ) )
50 49 3 eleqtrrdi 
 |-  ( ph -> M e. Z )
51 50 adantr 
 |-  ( ( ph /\ n e. { M } ) -> M e. Z )
52 47 51 eqeltrd 
 |-  ( ( ph /\ n e. { M } ) -> n e. Z )
53 45 52 ffvelrnd 
 |-  ( ( ph /\ n e. { M } ) -> ( E ` n ) e. S )
54 44 53 sseldd 
 |-  ( ( ph /\ n e. { M } ) -> ( E ` n ) e. dom O )
55 elssuni 
 |-  ( ( E ` n ) e. dom O -> ( E ` n ) C_ U. dom O )
56 54 55 syl 
 |-  ( ( ph /\ n e. { M } ) -> ( E ` n ) C_ U. dom O )
57 41 42 56 omecl 
 |-  ( ( ph /\ n e. { M } ) -> ( O ` ( E ` n ) ) e. ( 0 [,] +oo ) )
58 eqid 
 |-  ( n e. { M } |-> ( O ` ( E ` n ) ) ) = ( n e. { M } |-> ( O ` ( E ` n ) ) )
59 57 58 fmptd 
 |-  ( ph -> ( n e. { M } |-> ( O ` ( E ` n ) ) ) : { M } --> ( 0 [,] +oo ) )
60 36 59 sge0sn 
 |-  ( ph -> ( sum^ ` ( n e. { M } |-> ( O ` ( E ` n ) ) ) ) = ( ( n e. { M } |-> ( O ` ( E ` n ) ) ) ` M ) )
61 eqidd 
 |-  ( ph -> ( n e. { M } |-> ( O ` ( E ` n ) ) ) = ( n e. { M } |-> ( O ` ( E ` n ) ) ) )
62 38 iuneq1d 
 |-  ( ph -> U_ i e. ( M ... M ) ( E ` i ) = U_ i e. { M } ( E ` i ) )
63 fveq2 
 |-  ( i = M -> ( E ` i ) = ( E ` M ) )
64 63 iunxsng 
 |-  ( M e. Z -> U_ i e. { M } ( E ` i ) = ( E ` M ) )
65 50 64 syl 
 |-  ( ph -> U_ i e. { M } ( E ` i ) = ( E ` M ) )
66 eqidd 
 |-  ( ph -> ( E ` M ) = ( E ` M ) )
67 62 65 66 3eqtrrd 
 |-  ( ph -> ( E ` M ) = U_ i e. ( M ... M ) ( E ` i ) )
68 67 adantr 
 |-  ( ( ph /\ n = M ) -> ( E ` M ) = U_ i e. ( M ... M ) ( E ` i ) )
69 fveq2 
 |-  ( n = M -> ( E ` n ) = ( E ` M ) )
70 69 adantl 
 |-  ( ( ph /\ n = M ) -> ( E ` n ) = ( E ` M ) )
71 oveq2 
 |-  ( n = M -> ( M ... n ) = ( M ... M ) )
72 71 iuneq1d 
 |-  ( n = M -> U_ i e. ( M ... n ) ( E ` i ) = U_ i e. ( M ... M ) ( E ` i ) )
73 ovex 
 |-  ( M ... M ) e. _V
74 fvex 
 |-  ( E ` i ) e. _V
75 73 74 iunex 
 |-  U_ i e. ( M ... M ) ( E ` i ) e. _V
76 75 a1i 
 |-  ( ph -> U_ i e. ( M ... M ) ( E ` i ) e. _V )
77 6 72 50 76 fvmptd3 
 |-  ( ph -> ( G ` M ) = U_ i e. ( M ... M ) ( E ` i ) )
78 77 adantr 
 |-  ( ( ph /\ n = M ) -> ( G ` M ) = U_ i e. ( M ... M ) ( E ` i ) )
79 68 70 78 3eqtr4d 
 |-  ( ( ph /\ n = M ) -> ( E ` n ) = ( G ` M ) )
80 79 fveq2d 
 |-  ( ( ph /\ n = M ) -> ( O ` ( E ` n ) ) = ( O ` ( G ` M ) ) )
81 snidg 
 |-  ( M e. Z -> M e. { M } )
82 50 81 syl 
 |-  ( ph -> M e. { M } )
83 fvexd 
 |-  ( ph -> ( O ` ( G ` M ) ) e. _V )
84 61 80 82 83 fvmptd 
 |-  ( ph -> ( ( n e. { M } |-> ( O ` ( E ` n ) ) ) ` M ) = ( O ` ( G ` M ) ) )
85 40 60 84 3eqtrrd 
 |-  ( ph -> ( O ` ( G ` M ) ) = ( sum^ ` ( n e. ( M ... M ) |-> ( O ` ( E ` n ) ) ) ) )
86 85 a1i 
 |-  ( N e. ( ZZ>= ` M ) -> ( ph -> ( O ` ( G ` M ) ) = ( sum^ ` ( n e. ( M ... M ) |-> ( O ` ( E ` n ) ) ) ) ) )
87 simp3 
 |-  ( ( i e. ( M ..^ N ) /\ ( ph -> ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) ) /\ ph ) -> ph )
88 simp1 
 |-  ( ( i e. ( M ..^ N ) /\ ( ph -> ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) ) /\ ph ) -> i e. ( M ..^ N ) )
89 id 
 |-  ( ( ph -> ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) ) -> ( ph -> ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) ) )
90 89 imp 
 |-  ( ( ( ph -> ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) ) /\ ph ) -> ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) )
91 90 3adant1 
 |-  ( ( i e. ( M ..^ N ) /\ ( ph -> ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) ) /\ ph ) -> ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) )
92 elfzoel1 
 |-  ( i e. ( M ..^ N ) -> M e. ZZ )
93 elfzoelz 
 |-  ( i e. ( M ..^ N ) -> i e. ZZ )
94 93 peano2zd 
 |-  ( i e. ( M ..^ N ) -> ( i + 1 ) e. ZZ )
95 92 94 94 3jca 
 |-  ( i e. ( M ..^ N ) -> ( M e. ZZ /\ ( i + 1 ) e. ZZ /\ ( i + 1 ) e. ZZ ) )
96 92 zred 
 |-  ( i e. ( M ..^ N ) -> M e. RR )
97 94 zred 
 |-  ( i e. ( M ..^ N ) -> ( i + 1 ) e. RR )
98 93 zred 
 |-  ( i e. ( M ..^ N ) -> i e. RR )
99 elfzole1 
 |-  ( i e. ( M ..^ N ) -> M <_ i )
100 98 ltp1d 
 |-  ( i e. ( M ..^ N ) -> i < ( i + 1 ) )
101 96 98 97 99 100 lelttrd 
 |-  ( i e. ( M ..^ N ) -> M < ( i + 1 ) )
102 96 97 101 ltled 
 |-  ( i e. ( M ..^ N ) -> M <_ ( i + 1 ) )
103 leid 
 |-  ( ( i + 1 ) e. RR -> ( i + 1 ) <_ ( i + 1 ) )
104 97 103 syl 
 |-  ( i e. ( M ..^ N ) -> ( i + 1 ) <_ ( i + 1 ) )
105 95 102 104 jca32 
 |-  ( i e. ( M ..^ N ) -> ( ( M e. ZZ /\ ( i + 1 ) e. ZZ /\ ( i + 1 ) e. ZZ ) /\ ( M <_ ( i + 1 ) /\ ( i + 1 ) <_ ( i + 1 ) ) ) )
106 elfz2 
 |-  ( ( i + 1 ) e. ( M ... ( i + 1 ) ) <-> ( ( M e. ZZ /\ ( i + 1 ) e. ZZ /\ ( i + 1 ) e. ZZ ) /\ ( M <_ ( i + 1 ) /\ ( i + 1 ) <_ ( i + 1 ) ) ) )
107 105 106 sylibr 
 |-  ( i e. ( M ..^ N ) -> ( i + 1 ) e. ( M ... ( i + 1 ) ) )
108 107 adantl 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( i + 1 ) e. ( M ... ( i + 1 ) ) )
109 fveq2 
 |-  ( j = ( i + 1 ) -> ( E ` j ) = ( E ` ( i + 1 ) ) )
110 109 ssiun2s 
 |-  ( ( i + 1 ) e. ( M ... ( i + 1 ) ) -> ( E ` ( i + 1 ) ) C_ U_ j e. ( M ... ( i + 1 ) ) ( E ` j ) )
111 108 110 syl 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( E ` ( i + 1 ) ) C_ U_ j e. ( M ... ( i + 1 ) ) ( E ` j ) )
112 fveq2 
 |-  ( i = j -> ( E ` i ) = ( E ` j ) )
113 112 cbviunv 
 |-  U_ i e. ( M ... n ) ( E ` i ) = U_ j e. ( M ... n ) ( E ` j )
114 113 mpteq2i 
 |-  ( n e. Z |-> U_ i e. ( M ... n ) ( E ` i ) ) = ( n e. Z |-> U_ j e. ( M ... n ) ( E ` j ) )
115 6 114 eqtri 
 |-  G = ( n e. Z |-> U_ j e. ( M ... n ) ( E ` j ) )
116 oveq2 
 |-  ( n = ( i + 1 ) -> ( M ... n ) = ( M ... ( i + 1 ) ) )
117 116 iuneq1d 
 |-  ( n = ( i + 1 ) -> U_ j e. ( M ... n ) ( E ` j ) = U_ j e. ( M ... ( i + 1 ) ) ( E ` j ) )
118 36 adantr 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> M e. ZZ )
119 93 adantl 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> i e. ZZ )
120 119 peano2zd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( i + 1 ) e. ZZ )
121 118 zred 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> M e. RR )
122 120 zred 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( i + 1 ) e. RR )
123 119 zred 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> i e. RR )
124 99 adantl 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> M <_ i )
125 123 ltp1d 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> i < ( i + 1 ) )
126 121 123 122 124 125 lelttrd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> M < ( i + 1 ) )
127 121 122 126 ltled 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> M <_ ( i + 1 ) )
128 118 120 127 3jca 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( M e. ZZ /\ ( i + 1 ) e. ZZ /\ M <_ ( i + 1 ) ) )
129 eluz2 
 |-  ( ( i + 1 ) e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ ( i + 1 ) e. ZZ /\ M <_ ( i + 1 ) ) )
130 128 129 sylibr 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( i + 1 ) e. ( ZZ>= ` M ) )
131 3 eqcomi 
 |-  ( ZZ>= ` M ) = Z
132 130 131 eleqtrdi 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( i + 1 ) e. Z )
133 ovex 
 |-  ( M ... ( i + 1 ) ) e. _V
134 fvex 
 |-  ( E ` j ) e. _V
135 133 134 iunex 
 |-  U_ j e. ( M ... ( i + 1 ) ) ( E ` j ) e. _V
136 135 a1i 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> U_ j e. ( M ... ( i + 1 ) ) ( E ` j ) e. _V )
137 115 117 132 136 fvmptd3 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( G ` ( i + 1 ) ) = U_ j e. ( M ... ( i + 1 ) ) ( E ` j ) )
138 137 eqcomd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> U_ j e. ( M ... ( i + 1 ) ) ( E ` j ) = ( G ` ( i + 1 ) ) )
139 111 138 sseqtrd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( E ` ( i + 1 ) ) C_ ( G ` ( i + 1 ) ) )
140 sseqin2 
 |-  ( ( E ` ( i + 1 ) ) C_ ( G ` ( i + 1 ) ) <-> ( ( G ` ( i + 1 ) ) i^i ( E ` ( i + 1 ) ) ) = ( E ` ( i + 1 ) ) )
141 140 biimpi 
 |-  ( ( E ` ( i + 1 ) ) C_ ( G ` ( i + 1 ) ) -> ( ( G ` ( i + 1 ) ) i^i ( E ` ( i + 1 ) ) ) = ( E ` ( i + 1 ) ) )
142 139 141 syl 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( ( G ` ( i + 1 ) ) i^i ( E ` ( i + 1 ) ) ) = ( E ` ( i + 1 ) ) )
143 142 fveq2d 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( O ` ( ( G ` ( i + 1 ) ) i^i ( E ` ( i + 1 ) ) ) ) = ( O ` ( E ` ( i + 1 ) ) ) )
144 nfcv 
 |-  F/_ j ( E ` ( i + 1 ) )
145 elfzouz 
 |-  ( i e. ( M ..^ N ) -> i e. ( ZZ>= ` M ) )
146 145 adantl 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> i e. ( ZZ>= ` M ) )
147 144 146 109 iunp1 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> U_ j e. ( M ... ( i + 1 ) ) ( E ` j ) = ( U_ j e. ( M ... i ) ( E ` j ) u. ( E ` ( i + 1 ) ) ) )
148 137 147 eqtrd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( G ` ( i + 1 ) ) = ( U_ j e. ( M ... i ) ( E ` j ) u. ( E ` ( i + 1 ) ) ) )
149 148 difeq1d 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( ( G ` ( i + 1 ) ) \ ( E ` ( i + 1 ) ) ) = ( ( U_ j e. ( M ... i ) ( E ` j ) u. ( E ` ( i + 1 ) ) ) \ ( E ` ( i + 1 ) ) ) )
150 fveq2 
 |-  ( n = j -> ( E ` n ) = ( E ` j ) )
151 150 cbvdisjv 
 |-  ( Disj_ n e. Z ( E ` n ) <-> Disj_ j e. Z ( E ` j ) )
152 5 151 sylib 
 |-  ( ph -> Disj_ j e. Z ( E ` j ) )
153 152 adantr 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> Disj_ j e. Z ( E ` j ) )
154 fzssuz 
 |-  ( M ... i ) C_ ( ZZ>= ` M )
155 154 131 sseqtri 
 |-  ( M ... i ) C_ Z
156 155 a1i 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( M ... i ) C_ Z )
157 fzp1nel 
 |-  -. ( i + 1 ) e. ( M ... i )
158 157 a1i 
 |-  ( i e. ( M ..^ N ) -> -. ( i + 1 ) e. ( M ... i ) )
159 158 adantl 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> -. ( i + 1 ) e. ( M ... i ) )
160 132 159 eldifd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( i + 1 ) e. ( Z \ ( M ... i ) ) )
161 153 156 160 109 disjiun2 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( U_ j e. ( M ... i ) ( E ` j ) i^i ( E ` ( i + 1 ) ) ) = (/) )
162 undif4 
 |-  ( ( U_ j e. ( M ... i ) ( E ` j ) i^i ( E ` ( i + 1 ) ) ) = (/) -> ( U_ j e. ( M ... i ) ( E ` j ) u. ( ( E ` ( i + 1 ) ) \ ( E ` ( i + 1 ) ) ) ) = ( ( U_ j e. ( M ... i ) ( E ` j ) u. ( E ` ( i + 1 ) ) ) \ ( E ` ( i + 1 ) ) ) )
163 161 162 syl 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( U_ j e. ( M ... i ) ( E ` j ) u. ( ( E ` ( i + 1 ) ) \ ( E ` ( i + 1 ) ) ) ) = ( ( U_ j e. ( M ... i ) ( E ` j ) u. ( E ` ( i + 1 ) ) ) \ ( E ` ( i + 1 ) ) ) )
164 163 eqcomd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( ( U_ j e. ( M ... i ) ( E ` j ) u. ( E ` ( i + 1 ) ) ) \ ( E ` ( i + 1 ) ) ) = ( U_ j e. ( M ... i ) ( E ` j ) u. ( ( E ` ( i + 1 ) ) \ ( E ` ( i + 1 ) ) ) ) )
165 simpl 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ph )
166 146 131 eleqtrdi 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> i e. Z )
167 115 a1i 
 |-  ( ( ph /\ i e. Z ) -> G = ( n e. Z |-> U_ j e. ( M ... n ) ( E ` j ) ) )
168 simpr 
 |-  ( ( ( ph /\ i e. Z ) /\ n = i ) -> n = i )
169 168 oveq2d 
 |-  ( ( ( ph /\ i e. Z ) /\ n = i ) -> ( M ... n ) = ( M ... i ) )
170 169 iuneq1d 
 |-  ( ( ( ph /\ i e. Z ) /\ n = i ) -> U_ j e. ( M ... n ) ( E ` j ) = U_ j e. ( M ... i ) ( E ` j ) )
171 simpr 
 |-  ( ( ph /\ i e. Z ) -> i e. Z )
172 ovex 
 |-  ( M ... i ) e. _V
173 172 134 iunex 
 |-  U_ j e. ( M ... i ) ( E ` j ) e. _V
174 173 a1i 
 |-  ( ( ph /\ i e. Z ) -> U_ j e. ( M ... i ) ( E ` j ) e. _V )
175 167 170 171 174 fvmptd 
 |-  ( ( ph /\ i e. Z ) -> ( G ` i ) = U_ j e. ( M ... i ) ( E ` j ) )
176 165 166 175 syl2anc 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( G ` i ) = U_ j e. ( M ... i ) ( E ` j ) )
177 176 eqcomd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> U_ j e. ( M ... i ) ( E ` j ) = ( G ` i ) )
178 difid 
 |-  ( ( E ` ( i + 1 ) ) \ ( E ` ( i + 1 ) ) ) = (/)
179 178 a1i 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( ( E ` ( i + 1 ) ) \ ( E ` ( i + 1 ) ) ) = (/) )
180 177 179 uneq12d 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( U_ j e. ( M ... i ) ( E ` j ) u. ( ( E ` ( i + 1 ) ) \ ( E ` ( i + 1 ) ) ) ) = ( ( G ` i ) u. (/) ) )
181 un0 
 |-  ( ( G ` i ) u. (/) ) = ( G ` i )
182 181 a1i 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( ( G ` i ) u. (/) ) = ( G ` i ) )
183 180 182 eqtrd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( U_ j e. ( M ... i ) ( E ` j ) u. ( ( E ` ( i + 1 ) ) \ ( E ` ( i + 1 ) ) ) ) = ( G ` i ) )
184 149 164 183 3eqtrd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( ( G ` ( i + 1 ) ) \ ( E ` ( i + 1 ) ) ) = ( G ` i ) )
185 184 fveq2d 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( O ` ( ( G ` ( i + 1 ) ) \ ( E ` ( i + 1 ) ) ) ) = ( O ` ( G ` i ) ) )
186 143 185 oveq12d 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( ( O ` ( ( G ` ( i + 1 ) ) i^i ( E ` ( i + 1 ) ) ) ) +e ( O ` ( ( G ` ( i + 1 ) ) \ ( E ` ( i + 1 ) ) ) ) ) = ( ( O ` ( E ` ( i + 1 ) ) ) +e ( O ` ( G ` i ) ) ) )
187 186 3adant3 
 |-  ( ( ph /\ i e. ( M ..^ N ) /\ ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) ) -> ( ( O ` ( ( G ` ( i + 1 ) ) i^i ( E ` ( i + 1 ) ) ) ) +e ( O ` ( ( G ` ( i + 1 ) ) \ ( E ` ( i + 1 ) ) ) ) ) = ( ( O ` ( E ` ( i + 1 ) ) ) +e ( O ` ( G ` i ) ) ) )
188 1 adantr 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> O e. OutMeas )
189 4 adantr 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> E : Z --> S )
190 189 132 ffvelrnd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( E ` ( i + 1 ) ) e. S )
191 simpll 
 |-  ( ( ( ph /\ i e. ( M ..^ N ) ) /\ j e. ( M ... ( i + 1 ) ) ) -> ph )
192 92 adantr 
 |-  ( ( i e. ( M ..^ N ) /\ j e. ( M ... ( i + 1 ) ) ) -> M e. ZZ )
193 elfzelz 
 |-  ( j e. ( M ... ( i + 1 ) ) -> j e. ZZ )
194 193 adantl 
 |-  ( ( i e. ( M ..^ N ) /\ j e. ( M ... ( i + 1 ) ) ) -> j e. ZZ )
195 elfzle1 
 |-  ( j e. ( M ... ( i + 1 ) ) -> M <_ j )
196 195 adantl 
 |-  ( ( i e. ( M ..^ N ) /\ j e. ( M ... ( i + 1 ) ) ) -> M <_ j )
197 192 194 196 3jca 
 |-  ( ( i e. ( M ..^ N ) /\ j e. ( M ... ( i + 1 ) ) ) -> ( M e. ZZ /\ j e. ZZ /\ M <_ j ) )
198 eluz2 
 |-  ( j e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ j e. ZZ /\ M <_ j ) )
199 197 198 sylibr 
 |-  ( ( i e. ( M ..^ N ) /\ j e. ( M ... ( i + 1 ) ) ) -> j e. ( ZZ>= ` M ) )
200 199 131 eleqtrdi 
 |-  ( ( i e. ( M ..^ N ) /\ j e. ( M ... ( i + 1 ) ) ) -> j e. Z )
201 200 adantll 
 |-  ( ( ( ph /\ i e. ( M ..^ N ) ) /\ j e. ( M ... ( i + 1 ) ) ) -> j e. Z )
202 1 43 syl 
 |-  ( ph -> S C_ dom O )
203 202 adantr 
 |-  ( ( ph /\ j e. Z ) -> S C_ dom O )
204 4 ffvelrnda 
 |-  ( ( ph /\ j e. Z ) -> ( E ` j ) e. S )
205 203 204 sseldd 
 |-  ( ( ph /\ j e. Z ) -> ( E ` j ) e. dom O )
206 elssuni 
 |-  ( ( E ` j ) e. dom O -> ( E ` j ) C_ U. dom O )
207 205 206 syl 
 |-  ( ( ph /\ j e. Z ) -> ( E ` j ) C_ U. dom O )
208 191 201 207 syl2anc 
 |-  ( ( ( ph /\ i e. ( M ..^ N ) ) /\ j e. ( M ... ( i + 1 ) ) ) -> ( E ` j ) C_ U. dom O )
209 208 ralrimiva 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> A. j e. ( M ... ( i + 1 ) ) ( E ` j ) C_ U. dom O )
210 iunss 
 |-  ( U_ j e. ( M ... ( i + 1 ) ) ( E ` j ) C_ U. dom O <-> A. j e. ( M ... ( i + 1 ) ) ( E ` j ) C_ U. dom O )
211 209 210 sylibr 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> U_ j e. ( M ... ( i + 1 ) ) ( E ` j ) C_ U. dom O )
212 137 211 eqsstrd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( G ` ( i + 1 ) ) C_ U. dom O )
213 188 2 42 190 212 caragensplit 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( ( O ` ( ( G ` ( i + 1 ) ) i^i ( E ` ( i + 1 ) ) ) ) +e ( O ` ( ( G ` ( i + 1 ) ) \ ( E ` ( i + 1 ) ) ) ) ) = ( O ` ( G ` ( i + 1 ) ) ) )
214 213 eqcomd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( O ` ( G ` ( i + 1 ) ) ) = ( ( O ` ( ( G ` ( i + 1 ) ) i^i ( E ` ( i + 1 ) ) ) ) +e ( O ` ( ( G ` ( i + 1 ) ) \ ( E ` ( i + 1 ) ) ) ) ) )
215 214 3adant3 
 |-  ( ( ph /\ i e. ( M ..^ N ) /\ ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) ) -> ( O ` ( G ` ( i + 1 ) ) ) = ( ( O ` ( ( G ` ( i + 1 ) ) i^i ( E ` ( i + 1 ) ) ) ) +e ( O ` ( ( G ` ( i + 1 ) ) \ ( E ` ( i + 1 ) ) ) ) ) )
216 188 adantr 
 |-  ( ( ( ph /\ i e. ( M ..^ N ) ) /\ n e. ( M ... ( i + 1 ) ) ) -> O e. OutMeas )
217 165 adantr 
 |-  ( ( ( ph /\ i e. ( M ..^ N ) ) /\ n e. ( M ... ( i + 1 ) ) ) -> ph )
218 elfzuz 
 |-  ( n e. ( M ... ( i + 1 ) ) -> n e. ( ZZ>= ` M ) )
219 218 131 eleqtrdi 
 |-  ( n e. ( M ... ( i + 1 ) ) -> n e. Z )
220 219 adantl 
 |-  ( ( ( ph /\ i e. ( M ..^ N ) ) /\ n e. ( M ... ( i + 1 ) ) ) -> n e. Z )
221 4 202 fssd 
 |-  ( ph -> E : Z --> dom O )
222 221 ffvelrnda 
 |-  ( ( ph /\ n e. Z ) -> ( E ` n ) e. dom O )
223 222 55 syl 
 |-  ( ( ph /\ n e. Z ) -> ( E ` n ) C_ U. dom O )
224 217 220 223 syl2anc 
 |-  ( ( ( ph /\ i e. ( M ..^ N ) ) /\ n e. ( M ... ( i + 1 ) ) ) -> ( E ` n ) C_ U. dom O )
225 216 42 224 omecl 
 |-  ( ( ( ph /\ i e. ( M ..^ N ) ) /\ n e. ( M ... ( i + 1 ) ) ) -> ( O ` ( E ` n ) ) e. ( 0 [,] +oo ) )
226 2fveq3 
 |-  ( n = ( i + 1 ) -> ( O ` ( E ` n ) ) = ( O ` ( E ` ( i + 1 ) ) ) )
227 146 225 226 sge0p1 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( sum^ ` ( n e. ( M ... ( i + 1 ) ) |-> ( O ` ( E ` n ) ) ) ) = ( ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) +e ( O ` ( E ` ( i + 1 ) ) ) ) )
228 227 3adant3 
 |-  ( ( ph /\ i e. ( M ..^ N ) /\ ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) ) -> ( sum^ ` ( n e. ( M ... ( i + 1 ) ) |-> ( O ` ( E ` n ) ) ) ) = ( ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) +e ( O ` ( E ` ( i + 1 ) ) ) ) )
229 id 
 |-  ( ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) -> ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) )
230 229 eqcomd 
 |-  ( ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) -> ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) = ( O ` ( G ` i ) ) )
231 230 oveq1d 
 |-  ( ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) -> ( ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) +e ( O ` ( E ` ( i + 1 ) ) ) ) = ( ( O ` ( G ` i ) ) +e ( O ` ( E ` ( i + 1 ) ) ) ) )
232 231 3ad2ant3 
 |-  ( ( ph /\ i e. ( M ..^ N ) /\ ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) ) -> ( ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) +e ( O ` ( E ` ( i + 1 ) ) ) ) = ( ( O ` ( G ` i ) ) +e ( O ` ( E ` ( i + 1 ) ) ) ) )
233 simpl 
 |-  ( ( ph /\ j e. ( M ... i ) ) -> ph )
234 155 sseli 
 |-  ( j e. ( M ... i ) -> j e. Z )
235 234 adantl 
 |-  ( ( ph /\ j e. ( M ... i ) ) -> j e. Z )
236 233 235 207 syl2anc 
 |-  ( ( ph /\ j e. ( M ... i ) ) -> ( E ` j ) C_ U. dom O )
237 236 adantlr 
 |-  ( ( ( ph /\ i e. Z ) /\ j e. ( M ... i ) ) -> ( E ` j ) C_ U. dom O )
238 237 ralrimiva 
 |-  ( ( ph /\ i e. Z ) -> A. j e. ( M ... i ) ( E ` j ) C_ U. dom O )
239 iunss 
 |-  ( U_ j e. ( M ... i ) ( E ` j ) C_ U. dom O <-> A. j e. ( M ... i ) ( E ` j ) C_ U. dom O )
240 238 239 sylibr 
 |-  ( ( ph /\ i e. Z ) -> U_ j e. ( M ... i ) ( E ` j ) C_ U. dom O )
241 175 240 eqsstrd 
 |-  ( ( ph /\ i e. Z ) -> ( G ` i ) C_ U. dom O )
242 165 166 241 syl2anc 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( G ` i ) C_ U. dom O )
243 188 42 242 omexrcl 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( O ` ( G ` i ) ) e. RR* )
244 111 211 sstrd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( E ` ( i + 1 ) ) C_ U. dom O )
245 188 42 244 omexrcl 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( O ` ( E ` ( i + 1 ) ) ) e. RR* )
246 243 245 xaddcomd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( ( O ` ( G ` i ) ) +e ( O ` ( E ` ( i + 1 ) ) ) ) = ( ( O ` ( E ` ( i + 1 ) ) ) +e ( O ` ( G ` i ) ) ) )
247 246 3adant3 
 |-  ( ( ph /\ i e. ( M ..^ N ) /\ ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) ) -> ( ( O ` ( G ` i ) ) +e ( O ` ( E ` ( i + 1 ) ) ) ) = ( ( O ` ( E ` ( i + 1 ) ) ) +e ( O ` ( G ` i ) ) ) )
248 228 232 247 3eqtrd 
 |-  ( ( ph /\ i e. ( M ..^ N ) /\ ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) ) -> ( sum^ ` ( n e. ( M ... ( i + 1 ) ) |-> ( O ` ( E ` n ) ) ) ) = ( ( O ` ( E ` ( i + 1 ) ) ) +e ( O ` ( G ` i ) ) ) )
249 187 215 248 3eqtr4d 
 |-  ( ( ph /\ i e. ( M ..^ N ) /\ ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) ) -> ( O ` ( G ` ( i + 1 ) ) ) = ( sum^ ` ( n e. ( M ... ( i + 1 ) ) |-> ( O ` ( E ` n ) ) ) ) )
250 87 88 91 249 syl3anc 
 |-  ( ( i e. ( M ..^ N ) /\ ( ph -> ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) ) /\ ph ) -> ( O ` ( G ` ( i + 1 ) ) ) = ( sum^ ` ( n e. ( M ... ( i + 1 ) ) |-> ( O ` ( E ` n ) ) ) ) )
251 250 3exp 
 |-  ( i e. ( M ..^ N ) -> ( ( ph -> ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) ) -> ( ph -> ( O ` ( G ` ( i + 1 ) ) ) = ( sum^ ` ( n e. ( M ... ( i + 1 ) ) |-> ( O ` ( E ` n ) ) ) ) ) ) )
252 16 22 28 34 86 251 fzind2 
 |-  ( N e. ( M ... N ) -> ( ph -> ( O ` ( G ` N ) ) = ( sum^ ` ( n e. ( M ... N ) |-> ( O ` ( E ` n ) ) ) ) ) )
253 9 10 252 sylc 
 |-  ( ph -> ( O ` ( G ` N ) ) = ( sum^ ` ( n e. ( M ... N ) |-> ( O ` ( E ` n ) ) ) ) )