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 ffvelcdmd 
 |-  ( ( 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 zred 
 |-  ( i e. ( M ..^ N ) -> M e. RR )
96 94 zred 
 |-  ( i e. ( M ..^ N ) -> ( i + 1 ) e. RR )
97 93 zred 
 |-  ( i e. ( M ..^ N ) -> i e. RR )
98 elfzole1 
 |-  ( i e. ( M ..^ N ) -> M <_ i )
99 97 ltp1d 
 |-  ( i e. ( M ..^ N ) -> i < ( i + 1 ) )
100 95 97 96 98 99 lelttrd 
 |-  ( i e. ( M ..^ N ) -> M < ( i + 1 ) )
101 95 96 100 ltled 
 |-  ( i e. ( M ..^ N ) -> M <_ ( i + 1 ) )
102 leid 
 |-  ( ( i + 1 ) e. RR -> ( i + 1 ) <_ ( i + 1 ) )
103 96 102 syl 
 |-  ( i e. ( M ..^ N ) -> ( i + 1 ) <_ ( i + 1 ) )
104 92 94 94 101 103 elfzd 
 |-  ( i e. ( M ..^ N ) -> ( i + 1 ) e. ( M ... ( i + 1 ) ) )
105 104 adantl 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( i + 1 ) e. ( M ... ( i + 1 ) ) )
106 fveq2 
 |-  ( j = ( i + 1 ) -> ( E ` j ) = ( E ` ( i + 1 ) ) )
107 106 ssiun2s 
 |-  ( ( i + 1 ) e. ( M ... ( i + 1 ) ) -> ( E ` ( i + 1 ) ) C_ U_ j e. ( M ... ( i + 1 ) ) ( E ` j ) )
108 105 107 syl 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( E ` ( i + 1 ) ) C_ U_ j e. ( M ... ( i + 1 ) ) ( E ` j ) )
109 fveq2 
 |-  ( i = j -> ( E ` i ) = ( E ` j ) )
110 109 cbviunv 
 |-  U_ i e. ( M ... n ) ( E ` i ) = U_ j e. ( M ... n ) ( E ` j )
111 110 mpteq2i 
 |-  ( n e. Z |-> U_ i e. ( M ... n ) ( E ` i ) ) = ( n e. Z |-> U_ j e. ( M ... n ) ( E ` j ) )
112 6 111 eqtri 
 |-  G = ( n e. Z |-> U_ j e. ( M ... n ) ( E ` j ) )
113 oveq2 
 |-  ( n = ( i + 1 ) -> ( M ... n ) = ( M ... ( i + 1 ) ) )
114 113 iuneq1d 
 |-  ( n = ( i + 1 ) -> U_ j e. ( M ... n ) ( E ` j ) = U_ j e. ( M ... ( i + 1 ) ) ( E ` j ) )
115 36 adantr 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> M e. ZZ )
116 93 adantl 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> i e. ZZ )
117 116 peano2zd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( i + 1 ) e. ZZ )
118 115 zred 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> M e. RR )
119 117 zred 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( i + 1 ) e. RR )
120 116 zred 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> i e. RR )
121 98 adantl 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> M <_ i )
122 120 ltp1d 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> i < ( i + 1 ) )
123 118 120 119 121 122 lelttrd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> M < ( i + 1 ) )
124 118 119 123 ltled 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> M <_ ( i + 1 ) )
125 115 117 124 3jca 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( M e. ZZ /\ ( i + 1 ) e. ZZ /\ M <_ ( i + 1 ) ) )
126 eluz2 
 |-  ( ( i + 1 ) e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ ( i + 1 ) e. ZZ /\ M <_ ( i + 1 ) ) )
127 125 126 sylibr 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( i + 1 ) e. ( ZZ>= ` M ) )
128 3 eqcomi 
 |-  ( ZZ>= ` M ) = Z
129 127 128 eleqtrdi 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( i + 1 ) e. Z )
130 ovex 
 |-  ( M ... ( i + 1 ) ) e. _V
131 fvex 
 |-  ( E ` j ) e. _V
132 130 131 iunex 
 |-  U_ j e. ( M ... ( i + 1 ) ) ( E ` j ) e. _V
133 132 a1i 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> U_ j e. ( M ... ( i + 1 ) ) ( E ` j ) e. _V )
134 112 114 129 133 fvmptd3 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( G ` ( i + 1 ) ) = U_ j e. ( M ... ( i + 1 ) ) ( E ` j ) )
135 134 eqcomd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> U_ j e. ( M ... ( i + 1 ) ) ( E ` j ) = ( G ` ( i + 1 ) ) )
136 108 135 sseqtrd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( E ` ( i + 1 ) ) C_ ( G ` ( i + 1 ) ) )
137 sseqin2 
 |-  ( ( E ` ( i + 1 ) ) C_ ( G ` ( i + 1 ) ) <-> ( ( G ` ( i + 1 ) ) i^i ( E ` ( i + 1 ) ) ) = ( E ` ( i + 1 ) ) )
138 137 biimpi 
 |-  ( ( E ` ( i + 1 ) ) C_ ( G ` ( i + 1 ) ) -> ( ( G ` ( i + 1 ) ) i^i ( E ` ( i + 1 ) ) ) = ( E ` ( i + 1 ) ) )
139 136 138 syl 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( ( G ` ( i + 1 ) ) i^i ( E ` ( i + 1 ) ) ) = ( E ` ( i + 1 ) ) )
140 139 fveq2d 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( O ` ( ( G ` ( i + 1 ) ) i^i ( E ` ( i + 1 ) ) ) ) = ( O ` ( E ` ( i + 1 ) ) ) )
141 nfcv 
 |-  F/_ j ( E ` ( i + 1 ) )
142 elfzouz 
 |-  ( i e. ( M ..^ N ) -> i e. ( ZZ>= ` M ) )
143 142 adantl 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> i e. ( ZZ>= ` M ) )
144 141 143 106 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 ) ) ) )
145 134 144 eqtrd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( G ` ( i + 1 ) ) = ( U_ j e. ( M ... i ) ( E ` j ) u. ( E ` ( i + 1 ) ) ) )
146 145 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 ) ) ) )
147 fveq2 
 |-  ( n = j -> ( E ` n ) = ( E ` j ) )
148 147 cbvdisjv 
 |-  ( Disj_ n e. Z ( E ` n ) <-> Disj_ j e. Z ( E ` j ) )
149 5 148 sylib 
 |-  ( ph -> Disj_ j e. Z ( E ` j ) )
150 149 adantr 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> Disj_ j e. Z ( E ` j ) )
151 fzssuz 
 |-  ( M ... i ) C_ ( ZZ>= ` M )
152 151 128 sseqtri 
 |-  ( M ... i ) C_ Z
153 152 a1i 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( M ... i ) C_ Z )
154 fzp1nel 
 |-  -. ( i + 1 ) e. ( M ... i )
155 154 a1i 
 |-  ( i e. ( M ..^ N ) -> -. ( i + 1 ) e. ( M ... i ) )
156 155 adantl 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> -. ( i + 1 ) e. ( M ... i ) )
157 129 156 eldifd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( i + 1 ) e. ( Z \ ( M ... i ) ) )
158 150 153 157 106 disjiun2 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( U_ j e. ( M ... i ) ( E ` j ) i^i ( E ` ( i + 1 ) ) ) = (/) )
159 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 ) ) ) )
160 158 159 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 ) ) ) )
161 160 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 ) ) ) ) )
162 simpl 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ph )
163 143 128 eleqtrdi 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> i e. Z )
164 112 a1i 
 |-  ( ( ph /\ i e. Z ) -> G = ( n e. Z |-> U_ j e. ( M ... n ) ( E ` j ) ) )
165 simpr 
 |-  ( ( ( ph /\ i e. Z ) /\ n = i ) -> n = i )
166 165 oveq2d 
 |-  ( ( ( ph /\ i e. Z ) /\ n = i ) -> ( M ... n ) = ( M ... i ) )
167 166 iuneq1d 
 |-  ( ( ( ph /\ i e. Z ) /\ n = i ) -> U_ j e. ( M ... n ) ( E ` j ) = U_ j e. ( M ... i ) ( E ` j ) )
168 simpr 
 |-  ( ( ph /\ i e. Z ) -> i e. Z )
169 ovex 
 |-  ( M ... i ) e. _V
170 169 131 iunex 
 |-  U_ j e. ( M ... i ) ( E ` j ) e. _V
171 170 a1i 
 |-  ( ( ph /\ i e. Z ) -> U_ j e. ( M ... i ) ( E ` j ) e. _V )
172 164 167 168 171 fvmptd 
 |-  ( ( ph /\ i e. Z ) -> ( G ` i ) = U_ j e. ( M ... i ) ( E ` j ) )
173 162 163 172 syl2anc 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( G ` i ) = U_ j e. ( M ... i ) ( E ` j ) )
174 173 eqcomd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> U_ j e. ( M ... i ) ( E ` j ) = ( G ` i ) )
175 difid 
 |-  ( ( E ` ( i + 1 ) ) \ ( E ` ( i + 1 ) ) ) = (/)
176 175 a1i 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( ( E ` ( i + 1 ) ) \ ( E ` ( i + 1 ) ) ) = (/) )
177 174 176 uneq12d 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( U_ j e. ( M ... i ) ( E ` j ) u. ( ( E ` ( i + 1 ) ) \ ( E ` ( i + 1 ) ) ) ) = ( ( G ` i ) u. (/) ) )
178 un0 
 |-  ( ( G ` i ) u. (/) ) = ( G ` i )
179 178 a1i 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( ( G ` i ) u. (/) ) = ( G ` i ) )
180 177 179 eqtrd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( U_ j e. ( M ... i ) ( E ` j ) u. ( ( E ` ( i + 1 ) ) \ ( E ` ( i + 1 ) ) ) ) = ( G ` i ) )
181 146 161 180 3eqtrd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( ( G ` ( i + 1 ) ) \ ( E ` ( i + 1 ) ) ) = ( G ` i ) )
182 181 fveq2d 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( O ` ( ( G ` ( i + 1 ) ) \ ( E ` ( i + 1 ) ) ) ) = ( O ` ( G ` i ) ) )
183 140 182 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 ) ) ) )
184 183 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 ) ) ) )
185 1 adantr 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> O e. OutMeas )
186 4 adantr 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> E : Z --> S )
187 186 129 ffvelcdmd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( E ` ( i + 1 ) ) e. S )
188 simpll 
 |-  ( ( ( ph /\ i e. ( M ..^ N ) ) /\ j e. ( M ... ( i + 1 ) ) ) -> ph )
189 92 adantr 
 |-  ( ( i e. ( M ..^ N ) /\ j e. ( M ... ( i + 1 ) ) ) -> M e. ZZ )
190 elfzelz 
 |-  ( j e. ( M ... ( i + 1 ) ) -> j e. ZZ )
191 190 adantl 
 |-  ( ( i e. ( M ..^ N ) /\ j e. ( M ... ( i + 1 ) ) ) -> j e. ZZ )
192 elfzle1 
 |-  ( j e. ( M ... ( i + 1 ) ) -> M <_ j )
193 192 adantl 
 |-  ( ( i e. ( M ..^ N ) /\ j e. ( M ... ( i + 1 ) ) ) -> M <_ j )
194 189 191 193 3jca 
 |-  ( ( i e. ( M ..^ N ) /\ j e. ( M ... ( i + 1 ) ) ) -> ( M e. ZZ /\ j e. ZZ /\ M <_ j ) )
195 eluz2 
 |-  ( j e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ j e. ZZ /\ M <_ j ) )
196 194 195 sylibr 
 |-  ( ( i e. ( M ..^ N ) /\ j e. ( M ... ( i + 1 ) ) ) -> j e. ( ZZ>= ` M ) )
197 196 128 eleqtrdi 
 |-  ( ( i e. ( M ..^ N ) /\ j e. ( M ... ( i + 1 ) ) ) -> j e. Z )
198 197 adantll 
 |-  ( ( ( ph /\ i e. ( M ..^ N ) ) /\ j e. ( M ... ( i + 1 ) ) ) -> j e. Z )
199 1 43 syl 
 |-  ( ph -> S C_ dom O )
200 199 adantr 
 |-  ( ( ph /\ j e. Z ) -> S C_ dom O )
201 4 ffvelcdmda 
 |-  ( ( ph /\ j e. Z ) -> ( E ` j ) e. S )
202 200 201 sseldd 
 |-  ( ( ph /\ j e. Z ) -> ( E ` j ) e. dom O )
203 elssuni 
 |-  ( ( E ` j ) e. dom O -> ( E ` j ) C_ U. dom O )
204 202 203 syl 
 |-  ( ( ph /\ j e. Z ) -> ( E ` j ) C_ U. dom O )
205 188 198 204 syl2anc 
 |-  ( ( ( ph /\ i e. ( M ..^ N ) ) /\ j e. ( M ... ( i + 1 ) ) ) -> ( E ` j ) C_ U. dom O )
206 205 ralrimiva 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> A. j e. ( M ... ( i + 1 ) ) ( E ` j ) C_ U. dom O )
207 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 )
208 206 207 sylibr 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> U_ j e. ( M ... ( i + 1 ) ) ( E ` j ) C_ U. dom O )
209 134 208 eqsstrd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( G ` ( i + 1 ) ) C_ U. dom O )
210 185 2 42 187 209 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 ) ) ) )
211 210 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 ) ) ) ) ) )
212 211 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 ) ) ) ) ) )
213 185 adantr 
 |-  ( ( ( ph /\ i e. ( M ..^ N ) ) /\ n e. ( M ... ( i + 1 ) ) ) -> O e. OutMeas )
214 162 adantr 
 |-  ( ( ( ph /\ i e. ( M ..^ N ) ) /\ n e. ( M ... ( i + 1 ) ) ) -> ph )
215 elfzuz 
 |-  ( n e. ( M ... ( i + 1 ) ) -> n e. ( ZZ>= ` M ) )
216 215 128 eleqtrdi 
 |-  ( n e. ( M ... ( i + 1 ) ) -> n e. Z )
217 216 adantl 
 |-  ( ( ( ph /\ i e. ( M ..^ N ) ) /\ n e. ( M ... ( i + 1 ) ) ) -> n e. Z )
218 4 199 fssd 
 |-  ( ph -> E : Z --> dom O )
219 218 ffvelcdmda 
 |-  ( ( ph /\ n e. Z ) -> ( E ` n ) e. dom O )
220 219 55 syl 
 |-  ( ( ph /\ n e. Z ) -> ( E ` n ) C_ U. dom O )
221 214 217 220 syl2anc 
 |-  ( ( ( ph /\ i e. ( M ..^ N ) ) /\ n e. ( M ... ( i + 1 ) ) ) -> ( E ` n ) C_ U. dom O )
222 213 42 221 omecl 
 |-  ( ( ( ph /\ i e. ( M ..^ N ) ) /\ n e. ( M ... ( i + 1 ) ) ) -> ( O ` ( E ` n ) ) e. ( 0 [,] +oo ) )
223 2fveq3 
 |-  ( n = ( i + 1 ) -> ( O ` ( E ` n ) ) = ( O ` ( E ` ( i + 1 ) ) ) )
224 143 222 223 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 ) ) ) ) )
225 224 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 ) ) ) ) )
226 id 
 |-  ( ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) -> ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) )
227 226 eqcomd 
 |-  ( ( O ` ( G ` i ) ) = ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) -> ( sum^ ` ( n e. ( M ... i ) |-> ( O ` ( E ` n ) ) ) ) = ( O ` ( G ` i ) ) )
228 227 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 ) ) ) ) )
229 228 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 ) ) ) ) )
230 simpl 
 |-  ( ( ph /\ j e. ( M ... i ) ) -> ph )
231 152 sseli 
 |-  ( j e. ( M ... i ) -> j e. Z )
232 231 adantl 
 |-  ( ( ph /\ j e. ( M ... i ) ) -> j e. Z )
233 230 232 204 syl2anc 
 |-  ( ( ph /\ j e. ( M ... i ) ) -> ( E ` j ) C_ U. dom O )
234 233 adantlr 
 |-  ( ( ( ph /\ i e. Z ) /\ j e. ( M ... i ) ) -> ( E ` j ) C_ U. dom O )
235 234 ralrimiva 
 |-  ( ( ph /\ i e. Z ) -> A. j e. ( M ... i ) ( E ` j ) C_ U. dom O )
236 iunss 
 |-  ( U_ j e. ( M ... i ) ( E ` j ) C_ U. dom O <-> A. j e. ( M ... i ) ( E ` j ) C_ U. dom O )
237 235 236 sylibr 
 |-  ( ( ph /\ i e. Z ) -> U_ j e. ( M ... i ) ( E ` j ) C_ U. dom O )
238 172 237 eqsstrd 
 |-  ( ( ph /\ i e. Z ) -> ( G ` i ) C_ U. dom O )
239 162 163 238 syl2anc 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( G ` i ) C_ U. dom O )
240 185 42 239 omexrcl 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( O ` ( G ` i ) ) e. RR* )
241 108 208 sstrd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( E ` ( i + 1 ) ) C_ U. dom O )
242 185 42 241 omexrcl 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( O ` ( E ` ( i + 1 ) ) ) e. RR* )
243 240 242 xaddcomd 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( ( O ` ( G ` i ) ) +e ( O ` ( E ` ( i + 1 ) ) ) ) = ( ( O ` ( E ` ( i + 1 ) ) ) +e ( O ` ( G ` i ) ) ) )
244 243 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 ) ) ) )
245 225 229 244 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 ) ) ) )
246 184 212 245 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 ) ) ) ) )
247 87 88 91 246 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 ) ) ) ) )
248 247 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 ) ) ) ) ) ) )
249 16 22 28 34 86 248 fzind2 
 |-  ( N e. ( M ... N ) -> ( ph -> ( O ` ( G ` N ) ) = ( sum^ ` ( n e. ( M ... N ) |-> ( O ` ( E ` n ) ) ) ) ) )
250 9 10 249 sylc 
 |-  ( ph -> ( O ` ( G ` N ) ) = ( sum^ ` ( n e. ( M ... N ) |-> ( O ` ( E ` n ) ) ) ) )