Metamath Proof Explorer


Theorem gsumpart

Description: Express a group sum as a double sum, grouping along a (possibly infinite) partition. (Contributed by Thierry Arnoux, 22-Jun-2024)

Ref Expression
Hypotheses gsumpart.b B = Base G
gsumpart.z 0 ˙ = 0 G
gsumpart.g φ G CMnd
gsumpart.a φ A V
gsumpart.x φ X W
gsumpart.f φ F : A B
gsumpart.w φ finSupp 0 ˙ F
gsumpart.1 φ Disj x X C
gsumpart.2 φ x X C = A
Assertion gsumpart φ G F = G x X G F C

Proof

Step Hyp Ref Expression
1 gsumpart.b B = Base G
2 gsumpart.z 0 ˙ = 0 G
3 gsumpart.g φ G CMnd
4 gsumpart.a φ A V
5 gsumpart.x φ X W
6 gsumpart.f φ F : A B
7 gsumpart.w φ finSupp 0 ˙ F
8 gsumpart.1 φ Disj x X C
9 gsumpart.2 φ x X C = A
10 eqid x X x × C = x X x × C
11 10 4 5 8 9 2ndresdjuf1o φ 2 nd x X x × C : x X x × C 1-1 onto A
12 1 2 3 4 6 7 11 gsumf1o φ G F = G F 2 nd x X x × C
13 snex x V
14 13 a1i φ x X x V
15 4 adantr φ x X A V
16 ssidd φ A A
17 9 16 eqsstrd φ x X C A
18 iunss x X C A x X C A
19 17 18 sylib φ x X C A
20 19 r19.21bi φ x X C A
21 15 20 ssexd φ x X C V
22 14 21 xpexd φ x X x × C V
23 22 ralrimiva φ x X x × C V
24 iunexg X W x X x × C V x X x × C V
25 5 23 24 syl2anc φ x X x × C V
26 relxp Rel x × C
27 26 a1i φ x X Rel x × C
28 27 ralrimiva φ x X Rel x × C
29 reliun Rel x X x × C x X Rel x × C
30 28 29 sylibr φ Rel x X x × C
31 dmiun dom x X x × C = x X dom x × C
32 dmxpss dom x × C x
33 32 rgenw x X dom x × C x
34 ss2iun x X dom x × C x x X dom x × C x X x
35 33 34 ax-mp x X dom x × C x X x
36 31 35 eqsstri dom x X x × C x X x
37 iunid x X x = X
38 36 37 sseqtri dom x X x × C X
39 38 a1i φ dom x X x × C X
40 fo2nd 2 nd : V onto V
41 fof 2 nd : V onto V 2 nd : V V
42 40 41 ax-mp 2 nd : V V
43 ssv x X x × C V
44 fssres 2 nd : V V x X x × C V 2 nd x X x × C : x X x × C V
45 42 43 44 mp2an 2 nd x X x × C : x X x × C V
46 ffn 2 nd x X x × C : x X x × C V 2 nd x X x × C Fn x X x × C
47 45 46 mp1i φ 2 nd x X x × C Fn x X x × C
48 djussxp2 x X x × C X × x X C
49 imass2 x X x × C X × x X C 2 nd x X x × C 2 nd X × x X C
50 48 49 ax-mp 2 nd x X x × C 2 nd X × x X C
51 ima0 2 nd =
52 xpeq1 X = X × x X C = × x X C
53 0xp × x X C =
54 52 53 eqtrdi X = X × x X C =
55 54 imaeq2d X = 2 nd X × x X C = 2 nd
56 iuneq1 X = x X C = x C
57 0iun x C =
58 56 57 eqtrdi X = x X C =
59 51 55 58 3eqtr4a X = 2 nd X × x X C = x X C
60 59 adantl φ X = 2 nd X × x X C = x X C
61 2ndimaxp X 2 nd X × x X C = x X C
62 61 adantl φ X 2 nd X × x X C = x X C
63 60 62 pm2.61dane φ 2 nd X × x X C = x X C
64 63 9 eqtrd φ 2 nd X × x X C = A
65 50 64 sseqtrid φ 2 nd x X x × C A
66 resssxp 2 nd x X x × C A 2 nd x X x × C x X x × C × A
67 65 66 sylib φ 2 nd x X x × C x X x × C × A
68 dff2 2 nd x X x × C : x X x × C A 2 nd x X x × C Fn x X x × C 2 nd x X x × C x X x × C × A
69 47 67 68 sylanbrc φ 2 nd x X x × C : x X x × C A
70 6 69 fcod φ F 2 nd x X x × C : x X x × C B
71 10 4 5 8 9 2ndresdju φ 2 nd x X x × C : x X x × C 1-1 A
72 2 fvexi 0 ˙ V
73 72 a1i φ 0 ˙ V
74 6 4 fexd φ F V
75 7 71 73 74 fsuppco φ finSupp 0 ˙ F 2 nd x X x × C
76 1 2 3 25 30 5 39 70 75 gsum2d φ G F 2 nd x X x × C = G y X G z x X x × C y y F 2 nd x X x × C z
77 nfcsb1v _ x y / x C
78 csbeq1a x = y C = y / x C
79 5 21 77 78 iunsnima2 φ y X x X x × C y = y / x C
80 df-ov y F 2 nd x X x × C z = F 2 nd x X x × C y z
81 69 ad2antrr φ y X z x X x × C y 2 nd x X x × C : x X x × C A
82 simplr φ y X z x X x × C y y X
83 vsnid y y
84 83 a1i φ y X z x X x × C y y y
85 79 eleq2d φ y X z x X x × C y z y / x C
86 85 biimpa φ y X z x X x × C y z y / x C
87 84 86 opelxpd φ y X z x X x × C y y z y × y / x C
88 nfcv _ x y
89 88 77 nfxp _ x y × y / x C
90 89 nfel2 x y z y × y / x C
91 sneq x = y x = y
92 91 78 xpeq12d x = y x × C = y × y / x C
93 92 eleq2d x = y y z x × C y z y × y / x C
94 90 93 rspce y X y z y × y / x C x X y z x × C
95 82 87 94 syl2anc φ y X z x X x × C y x X y z x × C
96 eliun y z x X x × C x X y z x × C
97 95 96 sylibr φ y X z x X x × C y y z x X x × C
98 81 97 fvco3d φ y X z x X x × C y F 2 nd x X x × C y z = F 2 nd x X x × C y z
99 97 fvresd φ y X z x X x × C y 2 nd x X x × C y z = 2 nd y z
100 vex y V
101 vex z V
102 100 101 op2nd 2 nd y z = z
103 99 102 eqtrdi φ y X z x X x × C y 2 nd x X x × C y z = z
104 103 fveq2d φ y X z x X x × C y F 2 nd x X x × C y z = F z
105 98 104 eqtrd φ y X z x X x × C y F 2 nd x X x × C y z = F z
106 80 105 syl5eq φ y X z x X x × C y y F 2 nd x X x × C z = F z
107 79 106 mpteq12dva φ y X z x X x × C y y F 2 nd x X x × C z = z y / x C F z
108 6 adantr φ y X F : A B
109 imassrn x X x × C y ran x X x × C
110 9 xpeq2d φ X × x X C = X × A
111 48 110 sseqtrid φ x X x × C X × A
112 rnss x X x × C X × A ran x X x × C ran X × A
113 111 112 syl φ ran x X x × C ran X × A
114 113 adantr φ y X ran x X x × C ran X × A
115 rnxpss ran X × A A
116 114 115 sstrdi φ y X ran x X x × C A
117 109 116 sstrid φ y X x X x × C y A
118 79 117 eqsstrrd φ y X y / x C A
119 108 118 feqresmpt φ y X F y / x C = z y / x C F z
120 107 119 eqtr4d φ y X z x X x × C y y F 2 nd x X x × C z = F y / x C
121 120 oveq2d φ y X G z x X x × C y y F 2 nd x X x × C z = G F y / x C
122 121 mpteq2dva φ y X G z x X x × C y y F 2 nd x X x × C z = y X G F y / x C
123 nfcv _ y G F C
124 nfcv _ x G
125 nfcv _ x Σ𝑔
126 nfcv _ x F
127 126 77 nfres _ x F y / x C
128 124 125 127 nfov _ x G F y / x C
129 78 reseq2d x = y F C = F y / x C
130 129 oveq2d x = y G F C = G F y / x C
131 123 128 130 cbvmpt x X G F C = y X G F y / x C
132 122 131 eqtr4di φ y X G z x X x × C y y F 2 nd x X x × C z = x X G F C
133 132 oveq2d φ G y X G z x X x × C y y F 2 nd x X x × C z = G x X G F C
134 12 76 133 3eqtrd φ G F = G x X G F C