Metamath Proof Explorer


Theorem itg1addlem4OLD

Description: Obsolete version of itg1addlem4 . (Contributed by Mario Carneiro, 28-Jun-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses i1fadd.1 φ F dom 1
i1fadd.2 φ G dom 1
itg1add.3 I = i , j if i = 0 j = 0 0 vol F -1 i G -1 j
itg1add.4 P = + ran F × ran G
Assertion itg1addlem4OLD φ 1 F + f G = y ran F z ran G y + z y I z

Proof

Step Hyp Ref Expression
1 i1fadd.1 φ F dom 1
2 i1fadd.2 φ G dom 1
3 itg1add.3 I = i , j if i = 0 j = 0 0 vol F -1 i G -1 j
4 itg1add.4 P = + ran F × ran G
5 1 2 i1fadd φ F + f G dom 1
6 i1frn F dom 1 ran F Fin
7 1 6 syl φ ran F Fin
8 i1frn G dom 1 ran G Fin
9 2 8 syl φ ran G Fin
10 xpfi ran F Fin ran G Fin ran F × ran G Fin
11 7 9 10 syl2anc φ ran F × ran G Fin
12 ax-addf + : ×
13 ffn + : × + Fn ×
14 12 13 ax-mp + Fn ×
15 i1ff F dom 1 F :
16 1 15 syl φ F :
17 16 frnd φ ran F
18 ax-resscn
19 17 18 sstrdi φ ran F
20 i1ff G dom 1 G :
21 2 20 syl φ G :
22 21 frnd φ ran G
23 22 18 sstrdi φ ran G
24 xpss12 ran F ran G ran F × ran G ×
25 19 23 24 syl2anc φ ran F × ran G ×
26 fnssres + Fn × ran F × ran G × + ran F × ran G Fn ran F × ran G
27 14 25 26 sylancr φ + ran F × ran G Fn ran F × ran G
28 4 fneq1i P Fn ran F × ran G + ran F × ran G Fn ran F × ran G
29 27 28 sylibr φ P Fn ran F × ran G
30 dffn4 P Fn ran F × ran G P : ran F × ran G onto ran P
31 29 30 sylib φ P : ran F × ran G onto ran P
32 fofi ran F × ran G Fin P : ran F × ran G onto ran P ran P Fin
33 11 31 32 syl2anc φ ran P Fin
34 difss ran P 0 ran P
35 ssfi ran P Fin ran P 0 ran P ran P 0 Fin
36 33 34 35 sylancl φ ran P 0 Fin
37 ffun + : × Fun +
38 12 37 ax-mp Fun +
39 12 fdmi dom + = ×
40 25 39 sseqtrrdi φ ran F × ran G dom +
41 funfvima2 Fun + ran F × ran G dom + x y ran F × ran G + x y + ran F × ran G
42 38 40 41 sylancr φ x y ran F × ran G + x y + ran F × ran G
43 opelxpi x ran F y ran G x y ran F × ran G
44 42 43 impel φ x ran F y ran G + x y + ran F × ran G
45 df-ov x + y = + x y
46 4 rneqi ran P = ran + ran F × ran G
47 df-ima + ran F × ran G = ran + ran F × ran G
48 46 47 eqtr4i ran P = + ran F × ran G
49 44 45 48 3eltr4g φ x ran F y ran G x + y ran P
50 16 ffnd φ F Fn
51 dffn3 F Fn F : ran F
52 50 51 sylib φ F : ran F
53 21 ffnd φ G Fn
54 dffn3 G Fn G : ran G
55 53 54 sylib φ G : ran G
56 reex V
57 56 a1i φ V
58 inidm =
59 49 52 55 57 57 58 off φ F + f G : ran P
60 59 frnd φ ran F + f G ran P
61 60 ssdifd φ ran F + f G 0 ran P 0
62 17 sselda φ y ran F y
63 22 sselda φ z ran G z
64 62 63 anim12dan φ y ran F z ran G y z
65 readdcl y z y + z
66 64 65 syl φ y ran F z ran G y + z
67 66 ralrimivva φ y ran F z ran G y + z
68 funimassov Fun + ran F × ran G dom + + ran F × ran G y ran F z ran G y + z
69 38 40 68 sylancr φ + ran F × ran G y ran F z ran G y + z
70 67 69 mpbird φ + ran F × ran G
71 48 70 eqsstrid φ ran P
72 71 ssdifd φ ran P 0 0
73 itg1val2 F + f G dom 1 ran P 0 Fin ran F + f G 0 ran P 0 ran P 0 0 1 F + f G = w ran P 0 w vol F + f G -1 w
74 5 36 61 72 73 syl13anc φ 1 F + f G = w ran P 0 w vol F + f G -1 w
75 21 adantr φ w ran P 0 G :
76 9 adantr φ w ran P 0 ran G Fin
77 inss2 F -1 w z G -1 z G -1 z
78 77 a1i φ w ran P 0 z ran G F -1 w z G -1 z G -1 z
79 i1fima F dom 1 F -1 w z dom vol
80 1 79 syl φ F -1 w z dom vol
81 i1fima G dom 1 G -1 z dom vol
82 2 81 syl φ G -1 z dom vol
83 inmbl F -1 w z dom vol G -1 z dom vol F -1 w z G -1 z dom vol
84 80 82 83 syl2anc φ F -1 w z G -1 z dom vol
85 84 ad2antrr φ w ran P 0 z ran G F -1 w z G -1 z dom vol
86 34 71 sstrid φ ran P 0
87 86 sselda φ w ran P 0 w
88 87 adantr φ w ran P 0 z ran G w
89 63 adantlr φ w ran P 0 z ran G z
90 88 89 resubcld φ w ran P 0 z ran G w z
91 88 recnd φ w ran P 0 z ran G w
92 89 recnd φ w ran P 0 z ran G z
93 91 92 npcand φ w ran P 0 z ran G w - z + z = w
94 eldifsni w ran P 0 w 0
95 94 ad2antlr φ w ran P 0 z ran G w 0
96 93 95 eqnetrd φ w ran P 0 z ran G w - z + z 0
97 oveq12 w z = 0 z = 0 w - z + z = 0 + 0
98 00id 0 + 0 = 0
99 97 98 eqtrdi w z = 0 z = 0 w - z + z = 0
100 99 necon3ai w - z + z 0 ¬ w z = 0 z = 0
101 96 100 syl φ w ran P 0 z ran G ¬ w z = 0 z = 0
102 1 2 3 itg1addlem3 w z z ¬ w z = 0 z = 0 w z I z = vol F -1 w z G -1 z
103 90 89 101 102 syl21anc φ w ran P 0 z ran G w z I z = vol F -1 w z G -1 z
104 1 2 3 itg1addlem2 φ I : 2
105 104 ad2antrr φ w ran P 0 z ran G I : 2
106 105 90 89 fovrnd φ w ran P 0 z ran G w z I z
107 103 106 eqeltrrd φ w ran P 0 z ran G vol F -1 w z G -1 z
108 75 76 78 85 107 itg1addlem1 φ w ran P 0 vol z ran G F -1 w z G -1 z = z ran G vol F -1 w z G -1 z
109 87 recnd φ w ran P 0 w
110 1 2 i1faddlem φ w F + f G -1 w = z ran G F -1 w z G -1 z
111 109 110 syldan φ w ran P 0 F + f G -1 w = z ran G F -1 w z G -1 z
112 111 fveq2d φ w ran P 0 vol F + f G -1 w = vol z ran G F -1 w z G -1 z
113 103 sumeq2dv φ w ran P 0 z ran G w z I z = z ran G vol F -1 w z G -1 z
114 108 112 113 3eqtr4d φ w ran P 0 vol F + f G -1 w = z ran G w z I z
115 114 oveq2d φ w ran P 0 w vol F + f G -1 w = w z ran G w z I z
116 106 recnd φ w ran P 0 z ran G w z I z
117 76 109 116 fsummulc2 φ w ran P 0 w z ran G w z I z = z ran G w w z I z
118 115 117 eqtrd φ w ran P 0 w vol F + f G -1 w = z ran G w w z I z
119 118 sumeq2dv φ w ran P 0 w vol F + f G -1 w = w ran P 0 z ran G w w z I z
120 91 116 mulcld φ w ran P 0 z ran G w w z I z
121 120 anasss φ w ran P 0 z ran G w w z I z
122 36 9 121 fsumcom φ w ran P 0 z ran G w w z I z = z ran G w ran P 0 w w z I z
123 74 119 122 3eqtrd φ 1 F + f G = z ran G w ran P 0 w w z I z
124 oveq1 y = w z y + z = w - z + z
125 oveq1 y = w z y I z = w z I z
126 124 125 oveq12d y = w z y + z y I z = w - z + z w z I z
127 33 adantr φ z ran G ran P Fin
128 71 adantr φ z ran G ran P
129 128 sselda φ z ran G v ran P v
130 63 adantr φ z ran G v ran P z
131 129 130 resubcld φ z ran G v ran P v z
132 131 ex φ z ran G v ran P v z
133 129 recnd φ z ran G v ran P v
134 133 adantrr φ z ran G v ran P y ran P v
135 71 sselda φ y ran P y
136 135 ad2ant2rl φ z ran G v ran P y ran P y
137 136 recnd φ z ran G v ran P y ran P y
138 63 recnd φ z ran G z
139 138 adantr φ z ran G v ran P y ran P z
140 134 137 139 subcan2ad φ z ran G v ran P y ran P v z = y z v = y
141 140 ex φ z ran G v ran P y ran P v z = y z v = y
142 132 141 dom2lem φ z ran G v ran P v z : ran P 1-1
143 f1f1orn v ran P v z : ran P 1-1 v ran P v z : ran P 1-1 onto ran v ran P v z
144 142 143 syl φ z ran G v ran P v z : ran P 1-1 onto ran v ran P v z
145 oveq1 v = w v z = w z
146 eqid v ran P v z = v ran P v z
147 ovex w z V
148 145 146 147 fvmpt w ran P v ran P v z w = w z
149 148 adantl φ z ran G w ran P v ran P v z w = w z
150 f1f v ran P v z : ran P 1-1 v ran P v z : ran P
151 frn v ran P v z : ran P ran v ran P v z
152 142 150 151 3syl φ z ran G ran v ran P v z
153 152 sselda φ z ran G y ran v ran P v z y
154 63 adantr φ z ran G y ran v ran P v z z
155 153 154 readdcld φ z ran G y ran v ran P v z y + z
156 104 ad2antrr φ z ran G y ran v ran P v z I : 2
157 156 153 154 fovrnd φ z ran G y ran v ran P v z y I z
158 155 157 remulcld φ z ran G y ran v ran P v z y + z y I z
159 158 recnd φ z ran G y ran v ran P v z y + z y I z
160 126 127 144 149 159 fsumf1o φ z ran G y ran v ran P v z y + z y I z = w ran P w - z + z w z I z
161 128 sselda φ z ran G w ran P w
162 161 recnd φ z ran G w ran P w
163 138 adantr φ z ran G w ran P z
164 162 163 npcand φ z ran G w ran P w - z + z = w
165 164 oveq1d φ z ran G w ran P w - z + z w z I z = w w z I z
166 165 sumeq2dv φ z ran G w ran P w - z + z w z I z = w ran P w w z I z
167 160 166 eqtrd φ z ran G y ran v ran P v z y + z y I z = w ran P w w z I z
168 40 ad2antrr φ z ran G y ran F ran F × ran G dom +
169 simpr φ z ran G y ran F y ran F
170 simplr φ z ran G y ran F z ran G
171 169 170 opelxpd φ z ran G y ran F y z ran F × ran G
172 funfvima2 Fun + ran F × ran G dom + y z ran F × ran G + y z + ran F × ran G
173 38 172 mpan ran F × ran G dom + y z ran F × ran G + y z + ran F × ran G
174 168 171 173 sylc φ z ran G y ran F + y z + ran F × ran G
175 df-ov y + z = + y z
176 174 175 48 3eltr4g φ z ran G y ran F y + z ran P
177 62 adantlr φ z ran G y ran F y
178 177 recnd φ z ran G y ran F y
179 138 adantr φ z ran G y ran F z
180 178 179 pncand φ z ran G y ran F y + z - z = y
181 180 eqcomd φ z ran G y ran F y = y + z - z
182 oveq1 v = y + z v z = y + z - z
183 182 rspceeqv y + z ran P y = y + z - z v ran P y = v z
184 176 181 183 syl2anc φ z ran G y ran F v ran P y = v z
185 184 ralrimiva φ z ran G y ran F v ran P y = v z
186 ssabral ran F y | v ran P y = v z y ran F v ran P y = v z
187 185 186 sylibr φ z ran G ran F y | v ran P y = v z
188 146 rnmpt ran v ran P v z = y | v ran P y = v z
189 187 188 sseqtrrdi φ z ran G ran F ran v ran P v z
190 63 adantr φ z ran G y ran F z
191 177 190 readdcld φ z ran G y ran F y + z
192 104 ad2antrr φ z ran G y ran F I : 2
193 192 177 190 fovrnd φ z ran G y ran F y I z
194 191 193 remulcld φ z ran G y ran F y + z y I z
195 194 recnd φ z ran G y ran F y + z y I z
196 152 ssdifd φ z ran G ran v ran P v z ran F ran F
197 196 sselda φ z ran G y ran v ran P v z ran F y ran F
198 eldifi y ran F y
199 198 ad2antrl φ z ran G y ran F ¬ y = 0 z = 0 y
200 63 adantr φ z ran G y ran F ¬ y = 0 z = 0 z
201 simprr φ z ran G y ran F ¬ y = 0 z = 0 ¬ y = 0 z = 0
202 1 2 3 itg1addlem3 y z ¬ y = 0 z = 0 y I z = vol F -1 y G -1 z
203 199 200 201 202 syl21anc φ z ran G y ran F ¬ y = 0 z = 0 y I z = vol F -1 y G -1 z
204 inss1 F -1 y G -1 z F -1 y
205 eldifn y ran F ¬ y ran F
206 205 ad2antrl φ z ran G y ran F ¬ y = 0 z = 0 ¬ y ran F
207 vex v V
208 207 eliniseg y V v F -1 y v F y
209 208 elv v F -1 y v F y
210 vex y V
211 207 210 brelrn v F y y ran F
212 209 211 sylbi v F -1 y y ran F
213 206 212 nsyl φ z ran G y ran F ¬ y = 0 z = 0 ¬ v F -1 y
214 213 pm2.21d φ z ran G y ran F ¬ y = 0 z = 0 v F -1 y v
215 214 ssrdv φ z ran G y ran F ¬ y = 0 z = 0 F -1 y
216 204 215 sstrid φ z ran G y ran F ¬ y = 0 z = 0 F -1 y G -1 z
217 ss0 F -1 y G -1 z F -1 y G -1 z =
218 216 217 syl φ z ran G y ran F ¬ y = 0 z = 0 F -1 y G -1 z =
219 218 fveq2d φ z ran G y ran F ¬ y = 0 z = 0 vol F -1 y G -1 z = vol
220 0mbl dom vol
221 mblvol dom vol vol = vol *
222 220 221 ax-mp vol = vol *
223 ovol0 vol * = 0
224 222 223 eqtri vol = 0
225 219 224 eqtrdi φ z ran G y ran F ¬ y = 0 z = 0 vol F -1 y G -1 z = 0
226 203 225 eqtrd φ z ran G y ran F ¬ y = 0 z = 0 y I z = 0
227 226 oveq2d φ z ran G y ran F ¬ y = 0 z = 0 y + z y I z = y + z 0
228 199 200 readdcld φ z ran G y ran F ¬ y = 0 z = 0 y + z
229 228 recnd φ z ran G y ran F ¬ y = 0 z = 0 y + z
230 229 mul01d φ z ran G y ran F ¬ y = 0 z = 0 y + z 0 = 0
231 227 230 eqtrd φ z ran G y ran F ¬ y = 0 z = 0 y + z y I z = 0
232 231 expr φ z ran G y ran F ¬ y = 0 z = 0 y + z y I z = 0
233 oveq12 y = 0 z = 0 y + z = 0 + 0
234 233 98 eqtrdi y = 0 z = 0 y + z = 0
235 oveq12 y = 0 z = 0 y I z = 0 I 0
236 0re 0
237 iftrue i = 0 j = 0 if i = 0 j = 0 0 vol F -1 i G -1 j = 0
238 c0ex 0 V
239 237 3 238 ovmpoa 0 0 0 I 0 = 0
240 236 236 239 mp2an 0 I 0 = 0
241 235 240 eqtrdi y = 0 z = 0 y I z = 0
242 234 241 oveq12d y = 0 z = 0 y + z y I z = 0 0
243 0cn 0
244 243 mul01i 0 0 = 0
245 242 244 eqtrdi y = 0 z = 0 y + z y I z = 0
246 232 245 pm2.61d2 φ z ran G y ran F y + z y I z = 0
247 197 246 syldan φ z ran G y ran v ran P v z ran F y + z y I z = 0
248 f1ofo v ran P v z : ran P 1-1 onto ran v ran P v z v ran P v z : ran P onto ran v ran P v z
249 144 248 syl φ z ran G v ran P v z : ran P onto ran v ran P v z
250 fofi ran P Fin v ran P v z : ran P onto ran v ran P v z ran v ran P v z Fin
251 127 249 250 syl2anc φ z ran G ran v ran P v z Fin
252 189 195 247 251 fsumss φ z ran G y ran F y + z y I z = y ran v ran P v z y + z y I z
253 34 a1i φ z ran G ran P 0 ran P
254 120 an32s φ z ran G w ran P 0 w w z I z
255 dfin4 ran P 0 = ran P ran P 0
256 inss2 ran P 0 0
257 255 256 eqsstrri ran P ran P 0 0
258 257 sseli w ran P ran P 0 w 0
259 elsni w 0 w = 0
260 259 adantl φ z ran G w 0 w = 0
261 260 oveq1d φ z ran G w 0 w w z I z = 0 w z I z
262 104 ad2antrr φ z ran G w 0 I : 2
263 260 236 eqeltrdi φ z ran G w 0 w
264 63 adantr φ z ran G w 0 z
265 263 264 resubcld φ z ran G w 0 w z
266 262 265 264 fovrnd φ z ran G w 0 w z I z
267 266 recnd φ z ran G w 0 w z I z
268 267 mul02d φ z ran G w 0 0 w z I z = 0
269 261 268 eqtrd φ z ran G w 0 w w z I z = 0
270 258 269 sylan2 φ z ran G w ran P ran P 0 w w z I z = 0
271 253 254 270 127 fsumss φ z ran G w ran P 0 w w z I z = w ran P w w z I z
272 167 252 271 3eqtr4d φ z ran G y ran F y + z y I z = w ran P 0 w w z I z
273 272 sumeq2dv φ z ran G y ran F y + z y I z = z ran G w ran P 0 w w z I z
274 195 anasss φ z ran G y ran F y + z y I z
275 9 7 274 fsumcom φ z ran G y ran F y + z y I z = y ran F z ran G y + z y I z
276 123 273 275 3eqtr2d φ 1 F + f G = y ran F z ran G y + z y I z