Metamath Proof Explorer


Theorem gsumxp2

Description: Write a group sum over a cartesian product as a double sum in two ways. This corresponds to the first equation in Lang p. 6. (Contributed by AV, 27-Dec-2023)

Ref Expression
Hypotheses gsumxp2.b B=BaseG
gsumxp2.z 0˙=0G
gsumxp2.g φGCMnd
gsumxp2.a φAV
gsumxp2.r φCW
gsumxp2.f φF:A×CB
gsumxp2.w φfinSupp0˙F
Assertion gsumxp2 φGkCGjAjFk=GjAGkCjFk

Proof

Step Hyp Ref Expression
1 gsumxp2.b B=BaseG
2 gsumxp2.z 0˙=0G
3 gsumxp2.g φGCMnd
4 gsumxp2.a φAV
5 gsumxp2.r φCW
6 gsumxp2.f φF:A×CB
7 gsumxp2.w φfinSupp0˙F
8 6 fovrnda φjAkCjFkB
9 7 fsuppimpd φFsupp0˙Fin
10 simpl φjAkCφ
11 opelxpi jAkCjkA×C
12 11 ad2antlr φjAkC¬jksupp0˙FjkA×C
13 simpr φjAkC¬jksupp0˙F¬jksupp0˙F
14 12 13 eldifd φjAkC¬jksupp0˙FjkA×Csupp0˙F
15 ssidd φFsupp0˙Fsupp0˙
16 4 5 xpexd φA×CV
17 2 fvexi 0˙V
18 17 a1i φ0˙V
19 6 15 16 18 suppssr φjkA×Csupp0˙FFjk=0˙
20 10 14 19 syl2an2r φjAkC¬jksupp0˙FFjk=0˙
21 20 ex φjAkC¬jksupp0˙FFjk=0˙
22 df-br jsupp0˙Fkjksupp0˙F
23 22 notbii ¬jsupp0˙Fk¬jksupp0˙F
24 df-ov jFk=Fjk
25 24 eqeq1i jFk=0˙Fjk=0˙
26 21 23 25 3imtr4g φjAkC¬jsupp0˙FkjFk=0˙
27 26 impr φjAkC¬jsupp0˙FkjFk=0˙
28 1 2 3 4 5 8 9 27 gsumcom3 φGjAGkCjFk=GkCGjAjFk
29 28 eqcomd φGkCGjAjFk=GjAGkCjFk