Metamath Proof Explorer

Theorem gsumbagdiagOLD

Description: Obsolete version of gsumbagdiag as of 6-Aug-2024. (Contributed by Mario Carneiro, 5-Jan-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses psrbag.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
psrbagconf1o.s 
|- S = { y e. D | y oR <_ F }
gsumbagdiagOLD.i 
|- ( ph -> I e. V )
gsumbagdiagOLD.f 
|- ( ph -> F e. D )
gsumbagdiagOLD.b 
|- B = ( Base ` G )
gsumbagdiagOLD.g 
|- ( ph -> G e. CMnd )
gsumbagdiagOLD.x 
|- ( ( ph /\ ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> X e. B )
Assertion gsumbagdiagOLD 
|- ( 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 psrbag.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2 psrbagconf1o.s 
 |-  S = { y e. D | y oR <_ F }
3 gsumbagdiagOLD.i 
 |-  ( ph -> I e. V )
4 gsumbagdiagOLD.f 
 |-  ( ph -> F e. D )
5 gsumbagdiagOLD.b 
 |-  B = ( Base ` G )
6 gsumbagdiagOLD.g 
 |-  ( ph -> G e. CMnd )
7 gsumbagdiagOLD.x 
 |-  ( ( ph /\ ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> X e. B )
8 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
9 1 psrbaglefiOLD 
 |-  ( ( I e. V /\ F e. D ) -> { y e. D | y oR <_ F } e. Fin )
10 3 4 9 syl2anc 
 |-  ( ph -> { y e. D | y oR <_ F } e. Fin )
11 2 10 eqeltrid 
 |-  ( ph -> S e. Fin )
12 ovex 
 |-  ( NN0 ^m I ) e. _V
13 1 12 rab2ex 
 |-  { x e. D | x oR <_ ( F oF - j ) } e. _V
14 13 a1i 
 |-  ( ( ph /\ j e. S ) -> { x e. D | x oR <_ ( F oF - j ) } e. _V )
15 xpfi 
 |-  ( ( S e. Fin /\ S e. Fin ) -> ( S X. S ) e. Fin )
16 11 11 15 syl2anc 
 |-  ( ph -> ( S X. S ) e. Fin )
17 simprl 
 |-  ( ( ph /\ ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> j e. S )
18 1 2 3 4 gsumbagdiaglemOLD 
 |-  ( ( 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 ) } ) )
19 18 simpld 
 |-  ( ( ph /\ ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> k e. S )
20 brxp 
 |-  ( j ( S X. S ) k <-> ( j e. S /\ k e. S ) )
21 17 19 20 sylanbrc 
 |-  ( ( ph /\ ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> j ( S X. S ) k )
22 21 pm2.24d 
 |-  ( ( ph /\ ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> ( -. j ( S X. S ) k -> X = ( 0g ` G ) ) )
23 22 impr 
 |-  ( ( ph /\ ( ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) /\ -. j ( S X. S ) k ) ) -> X = ( 0g ` G ) )
24 1 2 3 4 gsumbagdiaglemOLD 
 |-  ( ( 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 ) } ) )
25 18 24 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 ) } ) ) )
26 5 8 6 11 14 7 16 23 11 25 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 ) ) )