Description: A commutative law for finitely supported iterated sums. (Contributed by Stefan O'Rear, 2-Nov-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | gsumcom3.b | |
|
gsumcom3.z | |
||
gsumcom3.g | |
||
gsumcom3.a | |
||
gsumcom3.r | |
||
gsumcom3.f | |
||
gsumcom3.u | |
||
gsumcom3.n | |
||
Assertion | gsumcom3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gsumcom3.b | |
|
2 | gsumcom3.z | |
|
3 | gsumcom3.g | |
|
4 | gsumcom3.a | |
|
5 | gsumcom3.r | |
|
6 | gsumcom3.f | |
|
7 | gsumcom3.u | |
|
8 | gsumcom3.n | |
|
9 | 1 2 3 4 5 6 7 8 | gsumcom | |
10 | 5 | adantr | |
11 | 1 2 3 4 10 6 7 8 | gsum2d2 | |
12 | 4 | adantr | |
13 | 6 | ancom2s | |
14 | cnvfi | |
|
15 | 7 14 | syl | |
16 | ancom | |
|
17 | vex | |
|
18 | vex | |
|
19 | 17 18 | brcnv | |
20 | 19 | notbii | |
21 | 16 20 | anbi12i | |
22 | 21 8 | sylan2b | |
23 | 1 2 3 5 12 13 15 22 | gsum2d2 | |
24 | 9 11 23 | 3eqtr3d | |