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 ) ) )