Metamath Proof Explorer

Theorem carageniuncllem1

Description: The outer measure of A i^i ( Gn ) is the sum of the outer measures of A i^i ( Fm ) . These are lines 7 to 10 of Step (d) in the proof of Theorem 113C of Fremlin1 p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses carageniuncllem1.o 
|- ( ph -> O e. OutMeas )
carageniuncllem1.s 
|- S = ( CaraGen ` O )
carageniuncllem1.x 
|- X = U. dom O
carageniuncllem1.a 
|- ( ph -> A C_ X )
carageniuncllem1.re 
|- ( ph -> ( O ` A ) e. RR )
carageniuncllem1.z 
|- Z = ( ZZ>= ` M )
carageniuncllem1.e 
|- ( ph -> E : Z --> S )
carageniuncllem1.g 
|- G = ( n e. Z |-> U_ i e. ( M ... n ) ( E ` i ) )
carageniuncllem1.f 
|- F = ( n e. Z |-> ( ( E ` n ) \ U_ i e. ( M ..^ n ) ( E ` i ) ) )
carageniuncllem1.k 
|- ( ph -> K e. Z )
Assertion carageniuncllem1 
|- ( ph -> sum_ n e. ( M ... K ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` K ) ) ) )

Proof

Step Hyp Ref Expression
1 carageniuncllem1.o 
 |-  ( ph -> O e. OutMeas )
2 carageniuncllem1.s 
 |-  S = ( CaraGen ` O )
3 carageniuncllem1.x 
 |-  X = U. dom O
4 carageniuncllem1.a 
 |-  ( ph -> A C_ X )
5 carageniuncllem1.re 
 |-  ( ph -> ( O ` A ) e. RR )
6 carageniuncllem1.z 
 |-  Z = ( ZZ>= ` M )
7 carageniuncllem1.e 
 |-  ( ph -> E : Z --> S )
8 carageniuncllem1.g 
 |-  G = ( n e. Z |-> U_ i e. ( M ... n ) ( E ` i ) )
9 carageniuncllem1.f 
 |-  F = ( n e. Z |-> ( ( E ` n ) \ U_ i e. ( M ..^ n ) ( E ` i ) ) )
10 carageniuncllem1.k 
 |-  ( ph -> K e. Z )
11 10 6 eleqtrdi 
 |-  ( ph -> K e. ( ZZ>= ` M ) )
12 eluzfz2 
 |-  ( K e. ( ZZ>= ` M ) -> K e. ( M ... K ) )
13 11 12 syl 
 |-  ( ph -> K e. ( M ... K ) )
14 id 
 |-  ( ph -> ph )
15 oveq2 
 |-  ( k = M -> ( M ... k ) = ( M ... M ) )
16 15 sumeq1d 
 |-  ( k = M -> sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) = sum_ n e. ( M ... M ) ( O ` ( A i^i ( F ` n ) ) ) )
17 fveq2 
 |-  ( k = M -> ( G ` k ) = ( G ` M ) )
18 17 ineq2d 
 |-  ( k = M -> ( A i^i ( G ` k ) ) = ( A i^i ( G ` M ) ) )
19 18 fveq2d 
 |-  ( k = M -> ( O ` ( A i^i ( G ` k ) ) ) = ( O ` ( A i^i ( G ` M ) ) ) )
20 16 19 eqeq12d 
 |-  ( k = M -> ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` k ) ) ) <-> sum_ n e. ( M ... M ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` M ) ) ) ) )
21 20 imbi2d 
 |-  ( k = M -> ( ( ph -> sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` k ) ) ) ) <-> ( ph -> sum_ n e. ( M ... M ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` M ) ) ) ) ) )
22 oveq2 
 |-  ( k = j -> ( M ... k ) = ( M ... j ) )
23 22 sumeq1d 
 |-  ( k = j -> sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) = sum_ n e. ( M ... j ) ( O ` ( A i^i ( F ` n ) ) ) )
24 fveq2 
 |-  ( k = j -> ( G ` k ) = ( G ` j ) )
25 24 ineq2d 
 |-  ( k = j -> ( A i^i ( G ` k ) ) = ( A i^i ( G ` j ) ) )
26 25 fveq2d 
 |-  ( k = j -> ( O ` ( A i^i ( G ` k ) ) ) = ( O ` ( A i^i ( G ` j ) ) ) )
27 23 26 eqeq12d 
 |-  ( k = j -> ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` k ) ) ) <-> sum_ n e. ( M ... j ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` j ) ) ) ) )
28 27 imbi2d 
 |-  ( k = j -> ( ( ph -> sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` k ) ) ) ) <-> ( ph -> sum_ n e. ( M ... j ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` j ) ) ) ) ) )
29 oveq2 
 |-  ( k = ( j + 1 ) -> ( M ... k ) = ( M ... ( j + 1 ) ) )
30 29 sumeq1d 
 |-  ( k = ( j + 1 ) -> sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) = sum_ n e. ( M ... ( j + 1 ) ) ( O ` ( A i^i ( F ` n ) ) ) )
31 fveq2 
 |-  ( k = ( j + 1 ) -> ( G ` k ) = ( G ` ( j + 1 ) ) )
32 31 ineq2d 
 |-  ( k = ( j + 1 ) -> ( A i^i ( G ` k ) ) = ( A i^i ( G ` ( j + 1 ) ) ) )
33 32 fveq2d 
 |-  ( k = ( j + 1 ) -> ( O ` ( A i^i ( G ` k ) ) ) = ( O ` ( A i^i ( G ` ( j + 1 ) ) ) ) )
34 30 33 eqeq12d 
 |-  ( k = ( j + 1 ) -> ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` k ) ) ) <-> sum_ n e. ( M ... ( j + 1 ) ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` ( j + 1 ) ) ) ) ) )
35 34 imbi2d 
 |-  ( k = ( j + 1 ) -> ( ( ph -> sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` k ) ) ) ) <-> ( ph -> sum_ n e. ( M ... ( j + 1 ) ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` ( j + 1 ) ) ) ) ) ) )
36 oveq2 
 |-  ( k = K -> ( M ... k ) = ( M ... K ) )
37 36 sumeq1d 
 |-  ( k = K -> sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) = sum_ n e. ( M ... K ) ( O ` ( A i^i ( F ` n ) ) ) )
38 fveq2 
 |-  ( k = K -> ( G ` k ) = ( G ` K ) )
39 38 ineq2d 
 |-  ( k = K -> ( A i^i ( G ` k ) ) = ( A i^i ( G ` K ) ) )
40 39 fveq2d 
 |-  ( k = K -> ( O ` ( A i^i ( G ` k ) ) ) = ( O ` ( A i^i ( G ` K ) ) ) )
41 37 40 eqeq12d 
 |-  ( k = K -> ( sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` k ) ) ) <-> sum_ n e. ( M ... K ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` K ) ) ) ) )
42 41 imbi2d 
 |-  ( k = K -> ( ( ph -> sum_ n e. ( M ... k ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` k ) ) ) ) <-> ( ph -> sum_ n e. ( M ... K ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` K ) ) ) ) ) )
43 eluzel2 
 |-  ( K e. ( ZZ>= ` M ) -> M e. ZZ )
44 11 43 syl 
 |-  ( ph -> M e. ZZ )
45 fzsn 
 |-  ( M e. ZZ -> ( M ... M ) = { M } )
46 44 45 syl 
 |-  ( ph -> ( M ... M ) = { M } )
47 46 sumeq1d 
 |-  ( ph -> sum_ n e. ( M ... M ) ( O ` ( A i^i ( F ` n ) ) ) = sum_ n e. { M } ( O ` ( A i^i ( F ` n ) ) ) )
48 inss1 
 |-  ( A i^i ( F ` M ) ) C_ A
49 48 a1i 
 |-  ( ph -> ( A i^i ( F ` M ) ) C_ A )
50 1 3 4 5 49 omessre 
 |-  ( ph -> ( O ` ( A i^i ( F ` M ) ) ) e. RR )
51 50 recnd 
 |-  ( ph -> ( O ` ( A i^i ( F ` M ) ) ) e. CC )
52 fveq2 
 |-  ( n = M -> ( F ` n ) = ( F ` M ) )
53 52 ineq2d 
 |-  ( n = M -> ( A i^i ( F ` n ) ) = ( A i^i ( F ` M ) ) )
54 53 fveq2d 
 |-  ( n = M -> ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( F ` M ) ) ) )
55 54 sumsn 
 |-  ( ( M e. ZZ /\ ( O ` ( A i^i ( F ` M ) ) ) e. CC ) -> sum_ n e. { M } ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( F ` M ) ) ) )
56 44 51 55 syl2anc 
 |-  ( ph -> sum_ n e. { M } ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( F ` M ) ) ) )
57 eqidd 
 |-  ( ph -> ( O ` ( A i^i ( E ` M ) ) ) = ( O ` ( A i^i ( E ` M ) ) ) )
58 fveq2 
 |-  ( n = M -> ( E ` n ) = ( E ` M ) )
59 oveq2 
 |-  ( n = M -> ( M ..^ n ) = ( M ..^ M ) )
60 59 iuneq1d 
 |-  ( n = M -> U_ i e. ( M ..^ n ) ( E ` i ) = U_ i e. ( M ..^ M ) ( E ` i ) )
61 58 60 difeq12d 
 |-  ( n = M -> ( ( E ` n ) \ U_ i e. ( M ..^ n ) ( E ` i ) ) = ( ( E ` M ) \ U_ i e. ( M ..^ M ) ( E ` i ) ) )
62 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
63 44 62 syl 
 |-  ( ph -> M e. ( ZZ>= ` M ) )
64 6 a1i 
 |-  ( ph -> Z = ( ZZ>= ` M ) )
65 64 eqcomd 
 |-  ( ph -> ( ZZ>= ` M ) = Z )
66 63 65 eleqtrd 
 |-  ( ph -> M e. Z )
67 fvex 
 |-  ( E ` M ) e. _V
68 difexg 
 |-  ( ( E ` M ) e. _V -> ( ( E ` M ) \ U_ i e. ( M ..^ M ) ( E ` i ) ) e. _V )
69 67 68 ax-mp 
 |-  ( ( E ` M ) \ U_ i e. ( M ..^ M ) ( E ` i ) ) e. _V
70 69 a1i 
 |-  ( ph -> ( ( E ` M ) \ U_ i e. ( M ..^ M ) ( E ` i ) ) e. _V )
71 9 61 66 70 fvmptd3 
 |-  ( ph -> ( F ` M ) = ( ( E ` M ) \ U_ i e. ( M ..^ M ) ( E ` i ) ) )
72 fzo0 
 |-  ( M ..^ M ) = (/)
73 iuneq1 
 |-  ( ( M ..^ M ) = (/) -> U_ i e. ( M ..^ M ) ( E ` i ) = U_ i e. (/) ( E ` i ) )
74 72 73 ax-mp 
 |-  U_ i e. ( M ..^ M ) ( E ` i ) = U_ i e. (/) ( E ` i )
75 0iun 
 |-  U_ i e. (/) ( E ` i ) = (/)
76 74 75 eqtri 
 |-  U_ i e. ( M ..^ M ) ( E ` i ) = (/)
77 76 difeq2i 
 |-  ( ( E ` M ) \ U_ i e. ( M ..^ M ) ( E ` i ) ) = ( ( E ` M ) \ (/) )
78 77 a1i 
 |-  ( ph -> ( ( E ` M ) \ U_ i e. ( M ..^ M ) ( E ` i ) ) = ( ( E ` M ) \ (/) ) )
79 dif0 
 |-  ( ( E ` M ) \ (/) ) = ( E ` M )
80 79 a1i 
 |-  ( ph -> ( ( E ` M ) \ (/) ) = ( E ` M ) )
81 71 78 80 3eqtrd 
 |-  ( ph -> ( F ` M ) = ( E ` M ) )
82 81 ineq2d 
 |-  ( ph -> ( A i^i ( F ` M ) ) = ( A i^i ( E ` M ) ) )
83 82 fveq2d 
 |-  ( ph -> ( O ` ( A i^i ( F ` M ) ) ) = ( O ` ( A i^i ( E ` M ) ) ) )
84 oveq2 
 |-  ( n = M -> ( M ... n ) = ( M ... M ) )
85 84 iuneq1d 
 |-  ( n = M -> U_ i e. ( M ... n ) ( E ` i ) = U_ i e. ( M ... M ) ( E ` i ) )
86 ovex 
 |-  ( M ... M ) e. _V
87 fvex 
 |-  ( E ` i ) e. _V
88 86 87 iunex 
 |-  U_ i e. ( M ... M ) ( E ` i ) e. _V
89 88 a1i 
 |-  ( ph -> U_ i e. ( M ... M ) ( E ` i ) e. _V )
90 8 85 66 89 fvmptd3 
 |-  ( ph -> ( G ` M ) = U_ i e. ( M ... M ) ( E ` i ) )
91 46 iuneq1d 
 |-  ( ph -> U_ i e. ( M ... M ) ( E ` i ) = U_ i e. { M } ( E ` i ) )
92 fveq2 
 |-  ( i = M -> ( E ` i ) = ( E ` M ) )
93 92 iunxsng 
 |-  ( M e. ZZ -> U_ i e. { M } ( E ` i ) = ( E ` M ) )
94 44 93 syl 
 |-  ( ph -> U_ i e. { M } ( E ` i ) = ( E ` M ) )
95 90 91 94 3eqtrd 
 |-  ( ph -> ( G ` M ) = ( E ` M ) )
96 95 ineq2d 
 |-  ( ph -> ( A i^i ( G ` M ) ) = ( A i^i ( E ` M ) ) )
97 96 fveq2d 
 |-  ( ph -> ( O ` ( A i^i ( G ` M ) ) ) = ( O ` ( A i^i ( E ` M ) ) ) )
98 57 83 97 3eqtr4d 
 |-  ( ph -> ( O ` ( A i^i ( F ` M ) ) ) = ( O ` ( A i^i ( G ` M ) ) ) )
99 47 56 98 3eqtrd 
 |-  ( ph -> sum_ n e. ( M ... M ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` M ) ) ) )
100 99 a1i 
 |-  ( K e. ( ZZ>= ` M ) -> ( ph -> sum_ n e. ( M ... M ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` M ) ) ) ) )
101 simp3 
 |-  ( ( j e. ( M ..^ K ) /\ ( ph -> sum_ n e. ( M ... j ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` j ) ) ) ) /\ ph ) -> ph )
102 simp1 
 |-  ( ( j e. ( M ..^ K ) /\ ( ph -> sum_ n e. ( M ... j ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` j ) ) ) ) /\ ph ) -> j e. ( M ..^ K ) )
103 id 
 |-  ( ( ph -> sum_ n e. ( M ... j ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` j ) ) ) ) -> ( ph -> sum_ n e. ( M ... j ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` j ) ) ) ) )
104 103 imp 
 |-  ( ( ( ph -> sum_ n e. ( M ... j ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` j ) ) ) ) /\ ph ) -> sum_ n e. ( M ... j ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` j ) ) ) )
105 104 3adant1 
 |-  ( ( j e. ( M ..^ K ) /\ ( ph -> sum_ n e. ( M ... j ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` j ) ) ) ) /\ ph ) -> sum_ n e. ( M ... j ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` j ) ) ) )
106 elfzouz 
 |-  ( j e. ( M ..^ K ) -> j e. ( ZZ>= ` M ) )
107 106 adantl 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> j e. ( ZZ>= ` M ) )
108 1 adantr 
 |-  ( ( ph /\ n e. ( M ... ( j + 1 ) ) ) -> O e. OutMeas )
109 4 adantr 
 |-  ( ( ph /\ n e. ( M ... ( j + 1 ) ) ) -> A C_ X )
110 5 adantr 
 |-  ( ( ph /\ n e. ( M ... ( j + 1 ) ) ) -> ( O ` A ) e. RR )
111 inss1 
 |-  ( A i^i ( F ` n ) ) C_ A
112 111 a1i 
 |-  ( ( ph /\ n e. ( M ... ( j + 1 ) ) ) -> ( A i^i ( F ` n ) ) C_ A )
113 108 3 109 110 112 omessre 
 |-  ( ( ph /\ n e. ( M ... ( j + 1 ) ) ) -> ( O ` ( A i^i ( F ` n ) ) ) e. RR )
114 113 recnd 
 |-  ( ( ph /\ n e. ( M ... ( j + 1 ) ) ) -> ( O ` ( A i^i ( F ` n ) ) ) e. CC )
115 114 adantlr 
 |-  ( ( ( ph /\ j e. ( M ..^ K ) ) /\ n e. ( M ... ( j + 1 ) ) ) -> ( O ` ( A i^i ( F ` n ) ) ) e. CC )
116 fveq2 
 |-  ( n = ( j + 1 ) -> ( F ` n ) = ( F ` ( j + 1 ) ) )
117 116 ineq2d 
 |-  ( n = ( j + 1 ) -> ( A i^i ( F ` n ) ) = ( A i^i ( F ` ( j + 1 ) ) ) )
118 117 fveq2d 
 |-  ( n = ( j + 1 ) -> ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( F ` ( j + 1 ) ) ) ) )
119 107 115 118 fsump1 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> sum_ n e. ( M ... ( j + 1 ) ) ( O ` ( A i^i ( F ` n ) ) ) = ( sum_ n e. ( M ... j ) ( O ` ( A i^i ( F ` n ) ) ) + ( O ` ( A i^i ( F ` ( j + 1 ) ) ) ) ) )
120 119 3adant3 
 |-  ( ( ph /\ j e. ( M ..^ K ) /\ sum_ n e. ( M ... j ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` j ) ) ) ) -> sum_ n e. ( M ... ( j + 1 ) ) ( O ` ( A i^i ( F ` n ) ) ) = ( sum_ n e. ( M ... j ) ( O ` ( A i^i ( F ` n ) ) ) + ( O ` ( A i^i ( F ` ( j + 1 ) ) ) ) ) )
121 oveq1 
 |-  ( sum_ n e. ( M ... j ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` j ) ) ) -> ( sum_ n e. ( M ... j ) ( O ` ( A i^i ( F ` n ) ) ) + ( O ` ( A i^i ( F ` ( j + 1 ) ) ) ) ) = ( ( O ` ( A i^i ( G ` j ) ) ) + ( O ` ( A i^i ( F ` ( j + 1 ) ) ) ) ) )
122 121 3ad2ant3 
 |-  ( ( ph /\ j e. ( M ..^ K ) /\ sum_ n e. ( M ... j ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` j ) ) ) ) -> ( sum_ n e. ( M ... j ) ( O ` ( A i^i ( F ` n ) ) ) + ( O ` ( A i^i ( F ` ( j + 1 ) ) ) ) ) = ( ( O ` ( A i^i ( G ` j ) ) ) + ( O ` ( A i^i ( F ` ( j + 1 ) ) ) ) ) )
123 fzssp1 
 |-  ( M ... j ) C_ ( M ... ( j + 1 ) )
124 iunss1 
 |-  ( ( M ... j ) C_ ( M ... ( j + 1 ) ) -> U_ i e. ( M ... j ) ( E ` i ) C_ U_ i e. ( M ... ( j + 1 ) ) ( E ` i ) )
125 123 124 ax-mp 
 |-  U_ i e. ( M ... j ) ( E ` i ) C_ U_ i e. ( M ... ( j + 1 ) ) ( E ` i )
126 125 a1i 
 |-  ( j e. ( M ..^ K ) -> U_ i e. ( M ... j ) ( E ` i ) C_ U_ i e. ( M ... ( j + 1 ) ) ( E ` i ) )
127 oveq2 
 |-  ( n = j -> ( M ... n ) = ( M ... j ) )
128 127 iuneq1d 
 |-  ( n = j -> U_ i e. ( M ... n ) ( E ` i ) = U_ i e. ( M ... j ) ( E ` i ) )
129 106 6 eleqtrrdi 
 |-  ( j e. ( M ..^ K ) -> j e. Z )
130 ovex 
 |-  ( M ... j ) e. _V
131 130 87 iunex 
 |-  U_ i e. ( M ... j ) ( E ` i ) e. _V
132 131 a1i 
 |-  ( j e. ( M ..^ K ) -> U_ i e. ( M ... j ) ( E ` i ) e. _V )
133 8 128 129 132 fvmptd3 
 |-  ( j e. ( M ..^ K ) -> ( G ` j ) = U_ i e. ( M ... j ) ( E ` i ) )
134 oveq2 
 |-  ( n = ( j + 1 ) -> ( M ... n ) = ( M ... ( j + 1 ) ) )
135 134 iuneq1d 
 |-  ( n = ( j + 1 ) -> U_ i e. ( M ... n ) ( E ` i ) = U_ i e. ( M ... ( j + 1 ) ) ( E ` i ) )
136 peano2uz 
 |-  ( j e. ( ZZ>= ` M ) -> ( j + 1 ) e. ( ZZ>= ` M ) )
137 106 136 syl 
 |-  ( j e. ( M ..^ K ) -> ( j + 1 ) e. ( ZZ>= ` M ) )
138 6 eqcomi 
 |-  ( ZZ>= ` M ) = Z
139 137 138 eleqtrdi 
 |-  ( j e. ( M ..^ K ) -> ( j + 1 ) e. Z )
140 ovex 
 |-  ( M ... ( j + 1 ) ) e. _V
141 140 87 iunex 
 |-  U_ i e. ( M ... ( j + 1 ) ) ( E ` i ) e. _V
142 141 a1i 
 |-  ( j e. ( M ..^ K ) -> U_ i e. ( M ... ( j + 1 ) ) ( E ` i ) e. _V )
143 8 135 139 142 fvmptd3 
 |-  ( j e. ( M ..^ K ) -> ( G ` ( j + 1 ) ) = U_ i e. ( M ... ( j + 1 ) ) ( E ` i ) )
144 133 143 sseq12d 
 |-  ( j e. ( M ..^ K ) -> ( ( G ` j ) C_ ( G ` ( j + 1 ) ) <-> U_ i e. ( M ... j ) ( E ` i ) C_ U_ i e. ( M ... ( j + 1 ) ) ( E ` i ) ) )
145 126 144 mpbird 
 |-  ( j e. ( M ..^ K ) -> ( G ` j ) C_ ( G ` ( j + 1 ) ) )
146 inabs3 
 |-  ( ( G ` j ) C_ ( G ` ( j + 1 ) ) -> ( ( A i^i ( G ` ( j + 1 ) ) ) i^i ( G ` j ) ) = ( A i^i ( G ` j ) ) )
147 145 146 syl 
 |-  ( j e. ( M ..^ K ) -> ( ( A i^i ( G ` ( j + 1 ) ) ) i^i ( G ` j ) ) = ( A i^i ( G ` j ) ) )
148 147 fveq2d 
 |-  ( j e. ( M ..^ K ) -> ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) i^i ( G ` j ) ) ) = ( O ` ( A i^i ( G ` j ) ) ) )
149 148 eqcomd 
 |-  ( j e. ( M ..^ K ) -> ( O ` ( A i^i ( G ` j ) ) ) = ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) i^i ( G ` j ) ) ) )
150 149 adantl 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> ( O ` ( A i^i ( G ` j ) ) ) = ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) i^i ( G ` j ) ) ) )
151 elfzoelz 
 |-  ( j e. ( M ..^ K ) -> j e. ZZ )
152 fzval3 
 |-  ( j e. ZZ -> ( M ... j ) = ( M ..^ ( j + 1 ) ) )
153 151 152 syl 
 |-  ( j e. ( M ..^ K ) -> ( M ... j ) = ( M ..^ ( j + 1 ) ) )
154 153 eqcomd 
 |-  ( j e. ( M ..^ K ) -> ( M ..^ ( j + 1 ) ) = ( M ... j ) )
155 154 iuneq1d 
 |-  ( j e. ( M ..^ K ) -> U_ i e. ( M ..^ ( j + 1 ) ) ( E ` i ) = U_ i e. ( M ... j ) ( E ` i ) )
156 155 difeq2d 
 |-  ( j e. ( M ..^ K ) -> ( ( E ` ( j + 1 ) ) \ U_ i e. ( M ..^ ( j + 1 ) ) ( E ` i ) ) = ( ( E ` ( j + 1 ) ) \ U_ i e. ( M ... j ) ( E ` i ) ) )
157 156 adantl 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> ( ( E ` ( j + 1 ) ) \ U_ i e. ( M ..^ ( j + 1 ) ) ( E ` i ) ) = ( ( E ` ( j + 1 ) ) \ U_ i e. ( M ... j ) ( E ` i ) ) )
158 fveq2 
 |-  ( n = ( j + 1 ) -> ( E ` n ) = ( E ` ( j + 1 ) ) )
159 oveq2 
 |-  ( n = ( j + 1 ) -> ( M ..^ n ) = ( M ..^ ( j + 1 ) ) )
160 159 iuneq1d 
 |-  ( n = ( j + 1 ) -> U_ i e. ( M ..^ n ) ( E ` i ) = U_ i e. ( M ..^ ( j + 1 ) ) ( E ` i ) )
161 158 160 difeq12d 
 |-  ( n = ( j + 1 ) -> ( ( E ` n ) \ U_ i e. ( M ..^ n ) ( E ` i ) ) = ( ( E ` ( j + 1 ) ) \ U_ i e. ( M ..^ ( j + 1 ) ) ( E ` i ) ) )
162 fvex 
 |-  ( E ` ( j + 1 ) ) e. _V
163 difexg 
 |-  ( ( E ` ( j + 1 ) ) e. _V -> ( ( E ` ( j + 1 ) ) \ U_ i e. ( M ..^ ( j + 1 ) ) ( E ` i ) ) e. _V )
164 162 163 ax-mp 
 |-  ( ( E ` ( j + 1 ) ) \ U_ i e. ( M ..^ ( j + 1 ) ) ( E ` i ) ) e. _V
165 164 a1i 
 |-  ( j e. ( M ..^ K ) -> ( ( E ` ( j + 1 ) ) \ U_ i e. ( M ..^ ( j + 1 ) ) ( E ` i ) ) e. _V )
166 9 161 139 165 fvmptd3 
 |-  ( j e. ( M ..^ K ) -> ( F ` ( j + 1 ) ) = ( ( E ` ( j + 1 ) ) \ U_ i e. ( M ..^ ( j + 1 ) ) ( E ` i ) ) )
167 166 adantl 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> ( F ` ( j + 1 ) ) = ( ( E ` ( j + 1 ) ) \ U_ i e. ( M ..^ ( j + 1 ) ) ( E ` i ) ) )
168 nfcv 
 |-  F/_ i ( E ` ( j + 1 ) )
169 fveq2 
 |-  ( i = ( j + 1 ) -> ( E ` i ) = ( E ` ( j + 1 ) ) )
170 168 106 169 iunp1 
 |-  ( j e. ( M ..^ K ) -> U_ i e. ( M ... ( j + 1 ) ) ( E ` i ) = ( U_ i e. ( M ... j ) ( E ` i ) u. ( E ` ( j + 1 ) ) ) )
171 143 170 eqtrd 
 |-  ( j e. ( M ..^ K ) -> ( G ` ( j + 1 ) ) = ( U_ i e. ( M ... j ) ( E ` i ) u. ( E ` ( j + 1 ) ) ) )
172 171 133 difeq12d 
 |-  ( j e. ( M ..^ K ) -> ( ( G ` ( j + 1 ) ) \ ( G ` j ) ) = ( ( U_ i e. ( M ... j ) ( E ` i ) u. ( E ` ( j + 1 ) ) ) \ U_ i e. ( M ... j ) ( E ` i ) ) )
173 difundir 
 |-  ( ( U_ i e. ( M ... j ) ( E ` i ) u. ( E ` ( j + 1 ) ) ) \ U_ i e. ( M ... j ) ( E ` i ) ) = ( ( U_ i e. ( M ... j ) ( E ` i ) \ U_ i e. ( M ... j ) ( E ` i ) ) u. ( ( E ` ( j + 1 ) ) \ U_ i e. ( M ... j ) ( E ` i ) ) )
174 difid 
 |-  ( U_ i e. ( M ... j ) ( E ` i ) \ U_ i e. ( M ... j ) ( E ` i ) ) = (/)
175 174 uneq1i 
 |-  ( ( U_ i e. ( M ... j ) ( E ` i ) \ U_ i e. ( M ... j ) ( E ` i ) ) u. ( ( E ` ( j + 1 ) ) \ U_ i e. ( M ... j ) ( E ` i ) ) ) = ( (/) u. ( ( E ` ( j + 1 ) ) \ U_ i e. ( M ... j ) ( E ` i ) ) )
176 0un 
 |-  ( (/) u. ( ( E ` ( j + 1 ) ) \ U_ i e. ( M ... j ) ( E ` i ) ) ) = ( ( E ` ( j + 1 ) ) \ U_ i e. ( M ... j ) ( E ` i ) )
177 173 175 176 3eqtri 
 |-  ( ( U_ i e. ( M ... j ) ( E ` i ) u. ( E ` ( j + 1 ) ) ) \ U_ i e. ( M ... j ) ( E ` i ) ) = ( ( E ` ( j + 1 ) ) \ U_ i e. ( M ... j ) ( E ` i ) )
178 177 a1i 
 |-  ( j e. ( M ..^ K ) -> ( ( U_ i e. ( M ... j ) ( E ` i ) u. ( E ` ( j + 1 ) ) ) \ U_ i e. ( M ... j ) ( E ` i ) ) = ( ( E ` ( j + 1 ) ) \ U_ i e. ( M ... j ) ( E ` i ) ) )
179 172 178 eqtrd 
 |-  ( j e. ( M ..^ K ) -> ( ( G ` ( j + 1 ) ) \ ( G ` j ) ) = ( ( E ` ( j + 1 ) ) \ U_ i e. ( M ... j ) ( E ` i ) ) )
180 179 adantl 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> ( ( G ` ( j + 1 ) ) \ ( G ` j ) ) = ( ( E ` ( j + 1 ) ) \ U_ i e. ( M ... j ) ( E ` i ) ) )
181 157 167 180 3eqtr4d 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> ( F ` ( j + 1 ) ) = ( ( G ` ( j + 1 ) ) \ ( G ` j ) ) )
182 181 ineq2d 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> ( A i^i ( F ` ( j + 1 ) ) ) = ( A i^i ( ( G ` ( j + 1 ) ) \ ( G ` j ) ) ) )
183 indif2 
 |-  ( A i^i ( ( G ` ( j + 1 ) ) \ ( G ` j ) ) ) = ( ( A i^i ( G ` ( j + 1 ) ) ) \ ( G ` j ) )
184 183 eqcomi 
 |-  ( ( A i^i ( G ` ( j + 1 ) ) ) \ ( G ` j ) ) = ( A i^i ( ( G ` ( j + 1 ) ) \ ( G ` j ) ) )
185 184 a1i 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> ( ( A i^i ( G ` ( j + 1 ) ) ) \ ( G ` j ) ) = ( A i^i ( ( G ` ( j + 1 ) ) \ ( G ` j ) ) ) )
186 182 185 eqtr4d 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> ( A i^i ( F ` ( j + 1 ) ) ) = ( ( A i^i ( G ` ( j + 1 ) ) ) \ ( G ` j ) ) )
187 186 fveq2d 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> ( O ` ( A i^i ( F ` ( j + 1 ) ) ) ) = ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) \ ( G ` j ) ) ) )
188 150 187 oveq12d 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> ( ( O ` ( A i^i ( G ` j ) ) ) + ( O ` ( A i^i ( F ` ( j + 1 ) ) ) ) ) = ( ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) i^i ( G ` j ) ) ) + ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) \ ( G ` j ) ) ) ) )
189 inss1 
 |-  ( ( A i^i ( G ` ( j + 1 ) ) ) i^i ( G ` j ) ) C_ ( A i^i ( G ` ( j + 1 ) ) )
190 inss1 
 |-  ( A i^i ( G ` ( j + 1 ) ) ) C_ A
191 189 190 sstri 
 |-  ( ( A i^i ( G ` ( j + 1 ) ) ) i^i ( G ` j ) ) C_ A
192 191 a1i 
 |-  ( ph -> ( ( A i^i ( G ` ( j + 1 ) ) ) i^i ( G ` j ) ) C_ A )
193 1 3 4 5 192 omessre 
 |-  ( ph -> ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) i^i ( G ` j ) ) ) e. RR )
194 193 adantr 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) i^i ( G ` j ) ) ) e. RR )
195 1 adantr 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> O e. OutMeas )
196 4 adantr 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> A C_ X )
197 5 adantr 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> ( O ` A ) e. RR )
198 difss 
 |-  ( ( A i^i ( G ` ( j + 1 ) ) ) \ ( G ` j ) ) C_ ( A i^i ( G ` ( j + 1 ) ) )
199 198 190 sstri 
 |-  ( ( A i^i ( G ` ( j + 1 ) ) ) \ ( G ` j ) ) C_ A
200 199 a1i 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> ( ( A i^i ( G ` ( j + 1 ) ) ) \ ( G ` j ) ) C_ A )
201 195 3 196 197 200 omessre 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) \ ( G ` j ) ) ) e. RR )
202 rexadd 
 |-  ( ( ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) i^i ( G ` j ) ) ) e. RR /\ ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) \ ( G ` j ) ) ) e. RR ) -> ( ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) i^i ( G ` j ) ) ) +e ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) \ ( G ` j ) ) ) ) = ( ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) i^i ( G ` j ) ) ) + ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) \ ( G ` j ) ) ) ) )
203 194 201 202 syl2anc 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> ( ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) i^i ( G ` j ) ) ) +e ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) \ ( G ` j ) ) ) ) = ( ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) i^i ( G ` j ) ) ) + ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) \ ( G ` j ) ) ) ) )
204 203 eqcomd 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> ( ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) i^i ( G ` j ) ) ) + ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) \ ( G ` j ) ) ) ) = ( ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) i^i ( G ` j ) ) ) +e ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) \ ( G ` j ) ) ) ) )
205 133 adantl 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> ( G ` j ) = U_ i e. ( M ... j ) ( E ` i ) )
206 nfv 
 |-  F/ i ph
207 fzfid 
 |-  ( ph -> ( M ... j ) e. Fin )
208 7 adantr 
 |-  ( ( ph /\ i e. ( M ... j ) ) -> E : Z --> S )
209 elfzuz 
 |-  ( i e. ( M ... j ) -> i e. ( ZZ>= ` M ) )
210 138 a1i 
 |-  ( i e. ( M ... j ) -> ( ZZ>= ` M ) = Z )
211 209 210 eleqtrd 
 |-  ( i e. ( M ... j ) -> i e. Z )
212 211 adantl 
 |-  ( ( ph /\ i e. ( M ... j ) ) -> i e. Z )
213 208 212 ffvelrnd 
 |-  ( ( ph /\ i e. ( M ... j ) ) -> ( E ` i ) e. S )
214 206 1 2 207 213 caragenfiiuncl 
 |-  ( ph -> U_ i e. ( M ... j ) ( E ` i ) e. S )
215 214 adantr 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> U_ i e. ( M ... j ) ( E ` i ) e. S )
216 205 215 eqeltrd 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> ( G ` j ) e. S )
217 4 ssinss1d 
 |-  ( ph -> ( A i^i ( G ` ( j + 1 ) ) ) C_ X )
218 217 adantr 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> ( A i^i ( G ` ( j + 1 ) ) ) C_ X )
219 195 2 3 216 218 caragensplit 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> ( ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) i^i ( G ` j ) ) ) +e ( O ` ( ( A i^i ( G ` ( j + 1 ) ) ) \ ( G ` j ) ) ) ) = ( O ` ( A i^i ( G ` ( j + 1 ) ) ) ) )
220 188 204 219 3eqtrd 
 |-  ( ( ph /\ j e. ( M ..^ K ) ) -> ( ( O ` ( A i^i ( G ` j ) ) ) + ( O ` ( A i^i ( F ` ( j + 1 ) ) ) ) ) = ( O ` ( A i^i ( G ` ( j + 1 ) ) ) ) )
221 220 3adant3 
 |-  ( ( ph /\ j e. ( M ..^ K ) /\ sum_ n e. ( M ... j ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` j ) ) ) ) -> ( ( O ` ( A i^i ( G ` j ) ) ) + ( O ` ( A i^i ( F ` ( j + 1 ) ) ) ) ) = ( O ` ( A i^i ( G ` ( j + 1 ) ) ) ) )
222 120 122 221 3eqtrd 
 |-  ( ( ph /\ j e. ( M ..^ K ) /\ sum_ n e. ( M ... j ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` j ) ) ) ) -> sum_ n e. ( M ... ( j + 1 ) ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` ( j + 1 ) ) ) ) )
223 101 102 105 222 syl3anc 
 |-  ( ( j e. ( M ..^ K ) /\ ( ph -> sum_ n e. ( M ... j ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` j ) ) ) ) /\ ph ) -> sum_ n e. ( M ... ( j + 1 ) ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` ( j + 1 ) ) ) ) )
224 223 3exp 
 |-  ( j e. ( M ..^ K ) -> ( ( ph -> sum_ n e. ( M ... j ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` j ) ) ) ) -> ( ph -> sum_ n e. ( M ... ( j + 1 ) ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` ( j + 1 ) ) ) ) ) ) )
225 21 28 35 42 100 224 fzind2 
 |-  ( K e. ( M ... K ) -> ( ph -> sum_ n e. ( M ... K ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` K ) ) ) ) )
226 13 14 225 sylc 
 |-  ( ph -> sum_ n e. ( M ... K ) ( O ` ( A i^i ( F ` n ) ) ) = ( O ` ( A i^i ( G ` K ) ) ) )