Metamath Proof Explorer


Theorem gsumbagdiag

Description: Two-dimensional commutation of a group sum over a "triangular" region. fsum0diag analogue for finite bags. (Contributed by Mario Carneiro, 5-Jan-2015) Remove a sethood hypothesis. (Revised by SN, 6-Aug-2024)

Ref Expression
Hypotheses gsumbagdiag.d D = f 0 I | f -1 Fin
gsumbagdiag.s S = y D | y f F
gsumbagdiag.f φ F D
gsumbagdiag.b B = Base G
gsumbagdiag.g φ G CMnd
gsumbagdiag.x φ j S k x D | x f F f j X B
Assertion gsumbagdiag φ G j S , k x D | x f F f j X = G k S , j x D | x f F f k X

Proof

Step Hyp Ref Expression
1 gsumbagdiag.d D = f 0 I | f -1 Fin
2 gsumbagdiag.s S = y D | y f F
3 gsumbagdiag.f φ F D
4 gsumbagdiag.b B = Base G
5 gsumbagdiag.g φ G CMnd
6 gsumbagdiag.x φ j S k x D | x f F f j X B
7 eqid 0 G = 0 G
8 1 psrbaglefi F D y D | y f F Fin
9 3 8 syl φ y D | y f F Fin
10 2 9 eqeltrid φ S Fin
11 ovex 0 I V
12 1 11 rab2ex x D | x f F f j V
13 12 a1i φ j S x D | x f F f j V
14 xpfi S Fin S Fin S × S Fin
15 10 10 14 syl2anc φ S × S Fin
16 simprl φ j S k x D | x f F f j j S
17 1 2 3 gsumbagdiaglem φ j S k x D | x f F f j k S j x D | x f F f k
18 17 simpld φ j S k x D | x f F f j k S
19 brxp j S × S k j S k S
20 16 18 19 sylanbrc φ j S k x D | x f F f j j S × S k
21 20 pm2.24d φ j S k x D | x f F f j ¬ j S × S k X = 0 G
22 21 impr φ j S k x D | x f F f j ¬ j S × S k X = 0 G
23 1 2 3 gsumbagdiaglem φ k S j x D | x f F f k j S k x D | x f F f j
24 17 23 impbida φ j S k x D | x f F f j k S j x D | x f F f k
25 4 7 5 10 13 6 15 22 10 24 gsumcom2 φ G j S , k x D | x f F f j X = G k S , j x D | x f F f k X