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 = ( Base ` G )
gsumxp2.z 
|- .0. = ( 0g ` G )
gsumxp2.g 
|- ( ph -> G e. CMnd )
gsumxp2.a 
|- ( ph -> A e. V )
gsumxp2.r 
|- ( ph -> C e. W )
gsumxp2.f 
|- ( ph -> F : ( A X. C ) --> B )
gsumxp2.w 
|- ( ph -> F finSupp .0. )
Assertion gsumxp2 
|- ( ph -> ( G gsum ( k e. C |-> ( G gsum ( j e. A |-> ( j F k ) ) ) ) ) = ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> ( j F k ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumxp2.b 
 |-  B = ( Base ` G )
2 gsumxp2.z 
 |-  .0. = ( 0g ` G )
3 gsumxp2.g 
 |-  ( ph -> G e. CMnd )
4 gsumxp2.a 
 |-  ( ph -> A e. V )
5 gsumxp2.r 
 |-  ( ph -> C e. W )
6 gsumxp2.f 
 |-  ( ph -> F : ( A X. C ) --> B )
7 gsumxp2.w 
 |-  ( ph -> F finSupp .0. )
8 6 fovrnda 
 |-  ( ( ph /\ ( j e. A /\ k e. C ) ) -> ( j F k ) e. B )
9 7 fsuppimpd 
 |-  ( ph -> ( F supp .0. ) e. Fin )
10 simpl 
 |-  ( ( ph /\ ( j e. A /\ k e. C ) ) -> ph )
11 opelxpi 
 |-  ( ( j e. A /\ k e. C ) -> <. j , k >. e. ( A X. C ) )
12 11 ad2antlr 
 |-  ( ( ( ph /\ ( j e. A /\ k e. C ) ) /\ -. <. j , k >. e. ( F supp .0. ) ) -> <. j , k >. e. ( A X. C ) )
13 simpr 
 |-  ( ( ( ph /\ ( j e. A /\ k e. C ) ) /\ -. <. j , k >. e. ( F supp .0. ) ) -> -. <. j , k >. e. ( F supp .0. ) )
14 12 13 eldifd 
 |-  ( ( ( ph /\ ( j e. A /\ k e. C ) ) /\ -. <. j , k >. e. ( F supp .0. ) ) -> <. j , k >. e. ( ( A X. C ) \ ( F supp .0. ) ) )
15 ssidd 
 |-  ( ph -> ( F supp .0. ) C_ ( F supp .0. ) )
16 4 5 xpexd 
 |-  ( ph -> ( A X. C ) e. _V )
17 2 fvexi 
 |-  .0. e. _V
18 17 a1i 
 |-  ( ph -> .0. e. _V )
19 6 15 16 18 suppssr 
 |-  ( ( ph /\ <. j , k >. e. ( ( A X. C ) \ ( F supp .0. ) ) ) -> ( F ` <. j , k >. ) = .0. )
20 10 14 19 syl2an2r 
 |-  ( ( ( ph /\ ( j e. A /\ k e. C ) ) /\ -. <. j , k >. e. ( F supp .0. ) ) -> ( F ` <. j , k >. ) = .0. )
21 20 ex 
 |-  ( ( ph /\ ( j e. A /\ k e. C ) ) -> ( -. <. j , k >. e. ( F supp .0. ) -> ( F ` <. j , k >. ) = .0. ) )
22 df-br 
 |-  ( j ( F supp .0. ) k <-> <. j , k >. e. ( F supp .0. ) )
23 22 notbii 
 |-  ( -. j ( F supp .0. ) k <-> -. <. j , k >. e. ( F supp .0. ) )
24 df-ov 
 |-  ( j F k ) = ( F ` <. j , k >. )
25 24 eqeq1i 
 |-  ( ( j F k ) = .0. <-> ( F ` <. j , k >. ) = .0. )
26 21 23 25 3imtr4g 
 |-  ( ( ph /\ ( j e. A /\ k e. C ) ) -> ( -. j ( F supp .0. ) k -> ( j F k ) = .0. ) )
27 26 impr 
 |-  ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j ( F supp .0. ) k ) ) -> ( j F k ) = .0. )
28 1 2 3 4 5 8 9 27 gsumcom3 
 |-  ( ph -> ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> ( j F k ) ) ) ) ) = ( G gsum ( k e. C |-> ( G gsum ( j e. A |-> ( j F k ) ) ) ) ) )
29 28 eqcomd 
 |-  ( ph -> ( G gsum ( k e. C |-> ( G gsum ( j e. A |-> ( j F k ) ) ) ) ) = ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> ( j F k ) ) ) ) ) )