Metamath Proof Explorer


Theorem gsumcom3

Description: A commutative law for finitely supported iterated sums. (Contributed by Stefan O'Rear, 2-Nov-2015)

Ref Expression
Hypotheses gsumcom3.b B=BaseG
gsumcom3.z 0˙=0G
gsumcom3.g φGCMnd
gsumcom3.a φAV
gsumcom3.r φCW
gsumcom3.f φjAkCXB
gsumcom3.u φUFin
gsumcom3.n φjAkC¬jUkX=0˙
Assertion gsumcom3 φGjAGkCX=GkCGjAX

Proof

Step Hyp Ref Expression
1 gsumcom3.b B=BaseG
2 gsumcom3.z 0˙=0G
3 gsumcom3.g φGCMnd
4 gsumcom3.a φAV
5 gsumcom3.r φCW
6 gsumcom3.f φjAkCXB
7 gsumcom3.u φUFin
8 gsumcom3.n φjAkC¬jUkX=0˙
9 1 2 3 4 5 6 7 8 gsumcom φGjA,kCX=GkC,jAX
10 5 adantr φjACW
11 1 2 3 4 10 6 7 8 gsum2d2 φGjA,kCX=GjAGkCX
12 4 adantr φkCAV
13 6 ancom2s φkCjAXB
14 cnvfi UFinU-1Fin
15 7 14 syl φU-1Fin
16 ancom kCjAjAkC
17 vex kV
18 vex jV
19 17 18 brcnv kU-1jjUk
20 19 notbii ¬kU-1j¬jUk
21 16 20 anbi12i kCjA¬kU-1jjAkC¬jUk
22 21 8 sylan2b φkCjA¬kU-1jX=0˙
23 1 2 3 5 12 13 15 22 gsum2d2 φGkC,jAX=GkCGjAX
24 9 11 23 3eqtr3d φGjAGkCX=GkCGjAX