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 0 I | f -1 Fin
psrbagconf1o.s S = y D | y f F
gsumbagdiagOLD.i φ I V
gsumbagdiagOLD.f φ F D
gsumbagdiagOLD.b B = Base G
gsumbagdiagOLD.g φ G CMnd
gsumbagdiagOLD.x φ j S k x D | x f F f j X B
Assertion gsumbagdiagOLD φ 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 psrbag.d D = f 0 I | f -1 Fin
2 psrbagconf1o.s S = y D | y f F
3 gsumbagdiagOLD.i φ I V
4 gsumbagdiagOLD.f φ F D
5 gsumbagdiagOLD.b B = Base G
6 gsumbagdiagOLD.g φ G CMnd
7 gsumbagdiagOLD.x φ j S k x D | x f F f j X B
8 eqid 0 G = 0 G
9 1 psrbaglefiOLD I V F D y D | y f F Fin
10 3 4 9 syl2anc φ y D | y f F Fin
11 2 10 eqeltrid φ S Fin
12 ovex 0 I V
13 1 12 rab2ex x D | x f F f j V
14 13 a1i φ j S x D | x f F f j V
15 xpfi S Fin S Fin S × S Fin
16 11 11 15 syl2anc φ S × S Fin
17 simprl φ j S k x D | x f F f j j S
18 1 2 3 4 gsumbagdiaglemOLD φ j S k x D | x f F f j k S j x D | x f F f k
19 18 simpld φ j S k x D | x f F f j k S
20 brxp j S × S k j S k S
21 17 19 20 sylanbrc φ j S k x D | x f F f j j S × S k
22 21 pm2.24d φ j S k x D | x f F f j ¬ j S × S k X = 0 G
23 22 impr φ j S k x D | x f F f j ¬ j S × S k X = 0 G
24 1 2 3 4 gsumbagdiaglemOLD φ k S j x D | x f F f k j S k x D | x f F f j
25 18 24 impbida φ j S k x D | x f F f j k S j x D | x f F f k
26 5 8 6 11 14 7 16 23 11 25 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