MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gsum2d Unicode version

Theorem gsum2d 16355
Description: Write a sum over a two-dimensional region as a double sum. (Contributed by Mario Carneiro, 28-Dec-2014.)
Hypotheses
Ref Expression
gsum2d.b
gsum2d.z
gsum2d.g
gsum2d.a
gsum2d.r
gsum2d.d
gsum2d.s
gsum2d.f
gsum2d.w
Assertion
Ref Expression
gsum2d
Distinct variable groups:   , ,   , ,   , ,   , ,   , ,   , ,   , ,

Proof of Theorem gsum2d
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gsum2d.w . . . 4
2 dmfi 7553 . . . 4
31, 2syl 16 . . 3
4 reseq2 5076 . . . . . . . . . 10
5 res0 5086 . . . . . . . . . 10
64, 5syl6eq 2470 . . . . . . . . 9
76reseq2d 5081 . . . . . . . 8
8 res0 5086 . . . . . . . 8
97, 8syl6eq 2470 . . . . . . 7
109oveq2d 6077 . . . . . 6
11 mpteq1 4347 . . . . . . . 8
12 mpt0 5508 . . . . . . . 8
1311, 12syl6eq 2470 . . . . . . 7
1413oveq2d 6077 . . . . . 6
1510, 14eqeq12d 2436 . . . . 5
1615imbi2d 310 . . . 4
17 reseq2 5076 . . . . . . . 8
1817reseq2d 5081 . . . . . . 7
1918oveq2d 6077 . . . . . 6
20 mpteq1 4347 . . . . . . 7
2120oveq2d 6077 . . . . . 6
2219, 21eqeq12d 2436 . . . . 5
2322imbi2d 310 . . . 4
24 reseq2 5076 . . . . . . . 8
2524reseq2d 5081 . . . . . . 7
2625oveq2d 6077 . . . . . 6
27 mpteq1 4347 . . . . . . 7
2827oveq2d 6077 . . . . . 6
2926, 28eqeq12d 2436 . . . . 5
3029imbi2d 310 . . . 4
31 reseq2 5076 . . . . . . . 8
3231reseq2d 5081 . . . . . . 7
3332oveq2d 6077 . . . . . 6
34 mpteq1 4347 . . . . . . 7
3534oveq2d 6077 . . . . . 6
3633, 35eqeq12d 2436 . . . . 5
3736imbi2d 310 . . . 4
38 eqidd 2423 . . . 4
39 oveq1 6068 . . . . . . 7
40 gsum2d.b . . . . . . . . . 10
41 gsum2d.z . . . . . . . . . 10
42 eqid 2422 . . . . . . . . . 10
43 gsum2d.g . . . . . . . . . . 11
4443adantr 455 . . . . . . . . . 10
45 gsum2d.a . . . . . . . . . . . 12
46 resexg 5121 . . . . . . . . . . . 12
4745, 46syl 16 . . . . . . . . . . 11
4847adantr 455 . . . . . . . . . 10
49 gsum2d.f . . . . . . . . . . . 12
50 resss 5106 . . . . . . . . . . . 12
51 fssres 5548 . . . . . . . . . . . 12
5249, 50, 51sylancl 647 . . . . . . . . . . 11
5352adantr 455 . . . . . . . . . 10
54 resss 5106 . . . . . . . . . . . . 13
55 cnvss 4983 . . . . . . . . . . . . 13
56 imass1 5175 . . . . . . . . . . . . 13
5754, 55, 56mp2b 10 . . . . . . . . . . . 12
58 ssfi 7492 . . . . . . . . . . . 12
591, 57, 58sylancl 647 . . . . . . . . . . 11
6059adantr 455 . . . . . . . . . 10
61 simprr 741 . . . . . . . . . . . . 13
62 disjsn 3913 . . . . . . . . . . . . 13
6361, 62sylibr 206 . . . . . . . . . . . 12
6463reseq2d 5081 . . . . . . . . . . 11
65 resindi 5098 . . . . . . . . . . 11
6664, 65, 53eqtr3g 2477 . . . . . . . . . 10
67 resundi 5096 . . . . . . . . . . 11
6867a1i 11 . . . . . . . . . 10
6940, 41, 42, 44, 48, 53, 60, 66, 68gsumsplit 16334 . . . . . . . . 9
70 ssun1 3496 . . . . . . . . . . . 12
71 ssres2 5109 . . . . . . . . . . . 12
72 resabs1 5111 . . . . . . . . . . . 12
7370, 71, 72mp2b 10 . . . . . . . . . . 11
7473oveq2i 6072 . . . . . . . . . 10
75 ssun2 3497 . . . . . . . . . . . 12
76 ssres2 5109 . . . . . . . . . . . 12
77 resabs1 5111 . . . . . . . . . . . 12
7875, 76, 77mp2b 10 . . . . . . . . . . 11
7978oveq2i 6072 . . . . . . . . . 10
8074, 79oveq12i 6073 . . . . . . . . 9
8169, 80syl6eq 2470 . . . . . . . 8
82 simprl 740 . . . . . . . . . 10
83 imaexg 6485 . . . . . . . . . . . . 13
8445, 83syl 16 . . . . . . . . . . . 12
85 vex 2954 . . . . . . . . . . . . . . 15
86 vex 2954 . . . . . . . . . . . . . . 15
8785, 86elimasn 5166 . . . . . . . . . . . . . 14
88 df-ov 6064 . . . . . . . . . . . . . . 15
8949ffvelrnda 5813 . . . . . . . . . . . . . . 15
9088, 89syl5eqel 2506 . . . . . . . . . . . . . 14
9187, 90sylan2b 465 . . . . . . . . . . . . 13
92 eqid 2422 . . . . . . . . . . . . 13
9391, 92fmptd 5837 . . . . . . . . . . . 12
94 rnfi 7555 . . . . . . . . . . . . . 14
951, 94syl 16 . . . . . . . . . . . . 13
9687biimpi 188 . . . . . . . . . . . . . . . . 17
9785, 86opelrn 5042 . . . . . . . . . . . . . . . . . 18
9897con3i 130 . . . . . . . . . . . . . . . . 17
9996, 98anim12i 553 . . . . . . . . . . . . . . . 16
100 eldif 3315 . . . . . . . . . . . . . . . 16
101 eldif 3315 . . . . . . . . . . . . . . . 16
10299, 100, 1013imtr4i 260 . . . . . . . . . . . . . . 15
103 ssid 3352 . . . . . . . . . . . . . . . . . 18
104103a1i 11 . . . . . . . . . . . . . . . . 17
10549, 104suppssrOLD 5807 . . . . . . . . . . . . . . . 16
10688, 105syl5eq 2466 . . . . . . . . . . . . . . 15
107102, 106sylan2 464 . . . . . . . . . . . . . 14
108107suppss2OLD 6285 . . . . . . . . . . . . 13
109 ssfi 7492 . . . . . . . . . . . . 13
11095, 108, 109syl2anc 646 . . . . . . . . . . . 12
11140, 41, 43, 84, 93, 110gsumcl 16324 . . . . . . . . . . 11
112111ad2antrr 710 . . . . . . . . . 10
113 vex 2954 . . . . . . . . . . 11
114113a1i 11 . . . . . . . . . 10
115 sneq 3864 . . . . . . . . . . . . . . . . 17
116115imaeq2d 5141 . . . . . . . . . . . . . . . 16
117 oveq1 6068 . . . . . . . . . . . . . . . 16
118116, 117mpteq12dv 4345 . . . . . . . . . . . . . . 15
119118oveq2d 6077 . . . . . . . . . . . . . 14
120119eleq1d 2488 . . . . . . . . . . . . 13
121120imbi2d 310 . . . . . . . . . . . 12
122121, 111chvarv 1949 . . . . . . . . . . 11
123122adantr 455 . . . . . . . . . 10
12440, 42, 44, 82, 112, 114, 61, 123, 119gsumunsn 16350 . . . . . . . . 9
125115reseq2d 5081 . . . . . . . . . . . . . . . 16
126125reseq2d 5081 . . . . . . . . . . . . . . 15
127126oveq2d 6077 . . . . . . . . . . . . . 14
128119, 127eqeq12d 2436 . . . . . . . . . . . . 13
129128imbi2d 310 . . . . . . . . . . . 12
130 2ndconst 6631 . . . . . . . . . . . . . . 15
13185, 130mp1i 12 . . . . . . . . . . . . . 14
13240, 41, 43, 84, 93, 110, 131gsumf1o 16325 . . . . . . . . . . . . 13
133 1st2nd2 6582 . . . . . . . . . . . . . . . . . . 19
134 xp1st 6575 . . . . . . . . . . . . . . . . . . . . 21
135 elsni 3879 . . . . . . . . . . . . . . . . . . . . 21
136134, 135syl 16 . . . . . . . . . . . . . . . . . . . 20
137136opeq1d 4040 . . . . . . . . . . . . . . . . . . 19
138133, 137eqtrd 2454 . . . . . . . . . . . . . . . . . 18
139138fveq2d 5665 . . . . . . . . . . . . . . . . 17
140 df-ov 6064 . . . . . . . . . . . . . . . . 17
141139, 140syl6eqr 2472 . . . . . . . . . . . . . . . 16
142141mpteq2ia 4349 . . . . . . . . . . . . . . 15
14349feqmptd 5714 . . . . . . . . . . . . . . . . 17
144143reseq1d 5080 . . . . . . . . . . . . . . . 16
145 resss 5106 . . . . . . . . . . . . . . . . . 18
146 resmpt 5128 . . . . . . . . . . . . . . . . . 18
147145, 146ax-mp 5 . . . . . . . . . . . . . . . . 17
148 ressn 5345 . . . . . . . . . . . . . . . . . 18
149 mpteq1 4347 . . . . . . . . . . . . . . . . . 18
150148, 149ax-mp 5 . . . . . . . . . . . . . . . . 17
151147, 150eqtri 2442 . . . . . . . . . . . . . . . 16
152144, 151syl6eq 2470 . . . . . . . . . . . . . . 15
153 xp2nd 6576 . . . . . . . . . . . . . . . . 17
154153adantl 456 . . . . . . . . . . . . . . . 16
155 fo2nd 6566 . . . . . . . . . . . . . . . . . . . 20
156 fof 5590 . . . . . . . . . . . . . . . . . . . 20
157155, 156mp1i 12 . . . . . . . . . . . . . . . . . . 19
158157feqmptd 5714 . . . . . . . . . . . . . . . . . 18
159158reseq1d 5080 . . . . . . . . . . . . . . . . 17
160 ssv 3353 . . . . . . . . . . . . . . . . . 18
161 resmpt 5128 . . . . . . . . . . . . . . . . . 18
162160, 161ax-mp 5 . . . . . . . . . . . . . . . . 17
163159, 162syl6eq 2470 . . . . . . . . . . . . . . . 16
164 eqidd 2423 . . . . . . . . . . . . . . . 16
165 oveq2 6069 . . . . . . . . . . . . . . . 16
166154, 163, 164, 165fmptco 5845 . . . . . . . . . . . . . . 15
167142, 152, 1663eqtr4a 2480 . . . . . . . . . . . . . 14
168167oveq2d 6077 . . . . . . . . . . . . 13
169132, 168eqtr4d 2457 . . . . . . . . . . . 12
170129, 169chvarv 1949 . . . . . . . . . . 11
171170adantr 455 . . . . . . . . . 10
172171oveq2d 6077 . . . . . . . . 9
173124, 172eqtrd 2454 . . . . . . . 8
17481, 173eqeq12d 2436 . . . . . . 7
17539, 174syl5ibr 215 . . . . . 6
176175expcom 428 . . . . 5