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 e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
gsumbagdiag.s
|- S = { y e. D | y oR <_ F }
gsumbagdiag.f
|- ( ph -> F e. D )
gsumbagdiag.b
|- B = ( Base ` G )
gsumbagdiag.g
|- ( ph -> G e. CMnd )
gsumbagdiag.x
|- ( ( ph /\ ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> X e. B )
Assertion gsumbagdiag
|- ( ph -> ( G gsum ( j e. S , k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) ) = ( G gsum ( k e. S , j e. { x e. D | x oR <_ ( F oF - k ) } |-> X ) ) )

Proof

Step Hyp Ref Expression
1 gsumbagdiag.d
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2 gsumbagdiag.s
 |-  S = { y e. D | y oR <_ F }
3 gsumbagdiag.f
 |-  ( ph -> F e. D )
4 gsumbagdiag.b
 |-  B = ( Base ` G )
5 gsumbagdiag.g
 |-  ( ph -> G e. CMnd )
6 gsumbagdiag.x
 |-  ( ( ph /\ ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> X e. B )
7 eqid
 |-  ( 0g ` G ) = ( 0g ` G )
8 1 psrbaglefi
 |-  ( F e. D -> { y e. D | y oR <_ F } e. Fin )
9 3 8 syl
 |-  ( ph -> { y e. D | y oR <_ F } e. Fin )
10 2 9 eqeltrid
 |-  ( ph -> S e. Fin )
11 ovex
 |-  ( NN0 ^m I ) e. _V
12 1 11 rab2ex
 |-  { x e. D | x oR <_ ( F oF - j ) } e. _V
13 12 a1i
 |-  ( ( ph /\ j e. S ) -> { x e. D | x oR <_ ( F oF - j ) } e. _V )
14 xpfi
 |-  ( ( S e. Fin /\ S e. Fin ) -> ( S X. S ) e. Fin )
15 10 10 14 syl2anc
 |-  ( ph -> ( S X. S ) e. Fin )
16 simprl
 |-  ( ( ph /\ ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> j e. S )
17 1 2 3 gsumbagdiaglem
 |-  ( ( ph /\ ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> ( k e. S /\ j e. { x e. D | x oR <_ ( F oF - k ) } ) )
18 17 simpld
 |-  ( ( ph /\ ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> k e. S )
19 brxp
 |-  ( j ( S X. S ) k <-> ( j e. S /\ k e. S ) )
20 16 18 19 sylanbrc
 |-  ( ( ph /\ ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> j ( S X. S ) k )
21 20 pm2.24d
 |-  ( ( ph /\ ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> ( -. j ( S X. S ) k -> X = ( 0g ` G ) ) )
22 21 impr
 |-  ( ( ph /\ ( ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) /\ -. j ( S X. S ) k ) ) -> X = ( 0g ` G ) )
23 1 2 3 gsumbagdiaglem
 |-  ( ( ph /\ ( k e. S /\ j e. { x e. D | x oR <_ ( F oF - k ) } ) ) -> ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) )
24 17 23 impbida
 |-  ( ph -> ( ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) <-> ( k e. S /\ j e. { x e. D | x oR <_ ( F oF - k ) } ) ) )
25 4 7 5 10 13 6 15 22 10 24 gsumcom2
 |-  ( ph -> ( G gsum ( j e. S , k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) ) = ( G gsum ( k e. S , j e. { x e. D | x oR <_ ( F oF - k ) } |-> X ) ) )