Metamath Proof Explorer


Theorem gsumhashmul

Description: Express a group sum by grouping by nonzero values. (Contributed by Thierry Arnoux, 22-Jun-2024)

Ref Expression
Hypotheses gsumhashmul.b B = Base G
gsumhashmul.z 0 ˙ = 0 G
gsumhashmul.x · ˙ = G
gsumhashmul.g φ G CMnd
gsumhashmul.f φ F : A B
gsumhashmul.1 φ finSupp 0 ˙ F
Assertion gsumhashmul φ G F = G x ran F 0 ˙ F -1 x · ˙ x

Proof

Step Hyp Ref Expression
1 gsumhashmul.b B = Base G
2 gsumhashmul.z 0 ˙ = 0 G
3 gsumhashmul.x · ˙ = G
4 gsumhashmul.g φ G CMnd
5 gsumhashmul.f φ F : A B
6 gsumhashmul.1 φ finSupp 0 ˙ F
7 suppssdm F supp 0 ˙ dom F
8 7 5 fssdm φ F supp 0 ˙ A
9 5 8 feqresmpt φ F supp 0 ˙ F = x supp 0 ˙ F F x
10 9 oveq2d φ G F supp 0 ˙ F = G x F supp 0 ˙ F x
11 relfsupp Rel finSupp
12 11 brrelex1i finSupp 0 ˙ F F V
13 6 12 syl φ F V
14 5 ffnd φ F Fn A
15 13 14 fndmexd φ A V
16 ssidd φ F supp 0 ˙ F supp 0 ˙
17 1 2 4 15 5 16 6 gsumres φ G F supp 0 ˙ F = G F
18 nfcv _ x F 1 st z
19 fveq2 x = 1 st z F x = F 1 st z
20 6 fsuppimpd φ F supp 0 ˙ Fin
21 ssidd φ B B
22 5 adantr φ x supp 0 ˙ F F : A B
23 8 sselda φ x supp 0 ˙ F x A
24 22 23 ffvelrnd φ x supp 0 ˙ F F x B
25 5 ffund φ Fun F
26 funrel Fun F Rel F
27 reldif Rel F Rel F V × 0 ˙
28 25 26 27 3syl φ Rel F V × 0 ˙
29 1stdm Rel F V × 0 ˙ z F V × 0 ˙ 1 st z dom F V × 0 ˙
30 28 29 sylan φ z F V × 0 ˙ 1 st z dom F V × 0 ˙
31 2 fvexi 0 ˙ V
32 31 a1i φ 0 ˙ V
33 fressupp Fun F F V 0 ˙ V F supp 0 ˙ F = F V × 0 ˙
34 25 13 32 33 syl3anc φ F supp 0 ˙ F = F V × 0 ˙
35 34 dmeqd φ dom F supp 0 ˙ F = dom F V × 0 ˙
36 7 a1i φ F supp 0 ˙ dom F
37 ssdmres F supp 0 ˙ dom F dom F supp 0 ˙ F = F supp 0 ˙
38 36 37 sylib φ dom F supp 0 ˙ F = F supp 0 ˙
39 35 38 eqtr3d φ dom F V × 0 ˙ = F supp 0 ˙
40 39 adantr φ z F V × 0 ˙ dom F V × 0 ˙ = F supp 0 ˙
41 30 40 eleqtrd φ z F V × 0 ˙ 1 st z supp 0 ˙ F
42 25 funresd φ Fun F supp 0 ˙ F
43 42 adantr φ x supp 0 ˙ F Fun F supp 0 ˙ F
44 38 eleq2d φ x dom F supp 0 ˙ F x supp 0 ˙ F
45 44 biimpar φ x supp 0 ˙ F x dom F supp 0 ˙ F
46 simpr φ x supp 0 ˙ F x supp 0 ˙ F
47 46 fvresd φ x supp 0 ˙ F F supp 0 ˙ F x = F x
48 funopfvb Fun F supp 0 ˙ F x dom F supp 0 ˙ F F supp 0 ˙ F x = F x x F x F supp 0 ˙ F
49 48 biimpa Fun F supp 0 ˙ F x dom F supp 0 ˙ F F supp 0 ˙ F x = F x x F x F supp 0 ˙ F
50 43 45 47 49 syl21anc φ x supp 0 ˙ F x F x F supp 0 ˙ F
51 34 adantr φ x supp 0 ˙ F F supp 0 ˙ F = F V × 0 ˙
52 50 51 eleqtrd φ x supp 0 ˙ F x F x F V × 0 ˙
53 eqeq2 v = x F x z = v z = x F x
54 53 bibi2d v = x F x x = 1 st z z = v x = 1 st z z = x F x
55 54 ralbidv v = x F x z F V × 0 ˙ x = 1 st z z = v z F V × 0 ˙ x = 1 st z z = x F x
56 55 adantl φ x supp 0 ˙ F v = x F x z F V × 0 ˙ x = 1 st z z = v z F V × 0 ˙ x = 1 st z z = x F x
57 fvexd φ x supp 0 ˙ F z F V × 0 ˙ x = 1 st z 2 nd z V
58 28 ad3antrrr φ x supp 0 ˙ F z F V × 0 ˙ x = 1 st z Rel F V × 0 ˙
59 simplr φ x supp 0 ˙ F z F V × 0 ˙ x = 1 st z z F V × 0 ˙
60 1st2nd Rel F V × 0 ˙ z F V × 0 ˙ z = 1 st z 2 nd z
61 58 59 60 syl2anc φ x supp 0 ˙ F z F V × 0 ˙ x = 1 st z z = 1 st z 2 nd z
62 opeq1 x = 1 st z x 2 nd z = 1 st z 2 nd z
63 62 adantl φ x supp 0 ˙ F z F V × 0 ˙ x = 1 st z x 2 nd z = 1 st z 2 nd z
64 61 63 eqtr4d φ x supp 0 ˙ F z F V × 0 ˙ x = 1 st z z = x 2 nd z
65 difssd φ x supp 0 ˙ F F V × 0 ˙ F
66 65 sselda φ x supp 0 ˙ F z F V × 0 ˙ z F
67 66 adantr φ x supp 0 ˙ F z F V × 0 ˙ x = 1 st z z F
68 64 67 eqeltrrd φ x supp 0 ˙ F z F V × 0 ˙ x = 1 st z x 2 nd z F
69 64 68 jca φ x supp 0 ˙ F z F V × 0 ˙ x = 1 st z z = x 2 nd z x 2 nd z F
70 opeq2 y = 2 nd z x y = x 2 nd z
71 70 eqeq2d y = 2 nd z z = x y z = x 2 nd z
72 70 eleq1d y = 2 nd z x y F x 2 nd z F
73 71 72 anbi12d y = 2 nd z z = x y x y F z = x 2 nd z x 2 nd z F
74 57 69 73 spcedv φ x supp 0 ˙ F z F V × 0 ˙ x = 1 st z y z = x y x y F
75 vex x V
76 75 elsnres z F x y z = x y x y F
77 74 76 sylibr φ x supp 0 ˙ F z F V × 0 ˙ x = 1 st z z F x
78 14 ad3antrrr φ x supp 0 ˙ F z F V × 0 ˙ x = 1 st z F Fn A
79 23 ad2antrr φ x supp 0 ˙ F z F V × 0 ˙ x = 1 st z x A
80 fnressn F Fn A x A F x = x F x
81 78 79 80 syl2anc φ x supp 0 ˙ F z F V × 0 ˙ x = 1 st z F x = x F x
82 77 81 eleqtrd φ x supp 0 ˙ F z F V × 0 ˙ x = 1 st z z x F x
83 elsni z x F x z = x F x
84 82 83 syl φ x supp 0 ˙ F z F V × 0 ˙ x = 1 st z z = x F x
85 simpr φ x supp 0 ˙ F z F V × 0 ˙ z = x F x z = x F x
86 85 fveq2d φ x supp 0 ˙ F z F V × 0 ˙ z = x F x 1 st z = 1 st x F x
87 fvex F x V
88 75 87 op1st 1 st x F x = x
89 86 88 eqtr2di φ x supp 0 ˙ F z F V × 0 ˙ z = x F x x = 1 st z
90 84 89 impbida φ x supp 0 ˙ F z F V × 0 ˙ x = 1 st z z = x F x
91 90 ralrimiva φ x supp 0 ˙ F z F V × 0 ˙ x = 1 st z z = x F x
92 52 56 91 rspcedvd φ x supp 0 ˙ F v F V × 0 ˙ z F V × 0 ˙ x = 1 st z z = v
93 reu6 ∃! z F V × 0 ˙ x = 1 st z v F V × 0 ˙ z F V × 0 ˙ x = 1 st z z = v
94 92 93 sylibr φ x supp 0 ˙ F ∃! z F V × 0 ˙ x = 1 st z
95 18 1 2 19 4 20 21 24 41 94 gsummptf1o φ G x F supp 0 ˙ F x = G z F V × 0 ˙ F 1 st z
96 10 17 95 3eqtr3d φ G F = G z F V × 0 ˙ F 1 st z
97 simpr φ z F V × 0 ˙ z F V × 0 ˙
98 97 eldifad φ z F V × 0 ˙ z F
99 funfv1st2nd Fun F z F F 1 st z = 2 nd z
100 25 98 99 syl2an2r φ z F V × 0 ˙ F 1 st z = 2 nd z
101 100 mpteq2dva φ z F V × 0 ˙ F 1 st z = z F V × 0 ˙ 2 nd z
102 101 oveq2d φ G z F V × 0 ˙ F 1 st z = G z F V × 0 ˙ 2 nd z
103 96 102 eqtrd φ G F = G z F V × 0 ˙ 2 nd z
104 nfcv _ z 1 st t
105 fvex 2 nd t V
106 fvex 1 st t V
107 105 106 op2ndd z = 2 nd t 1 st t 2 nd z = 1 st t
108 resfnfinfin F Fn A F supp 0 ˙ Fin F supp 0 ˙ F Fin
109 14 20 108 syl2anc φ F supp 0 ˙ F Fin
110 34 109 eqeltrrd φ F V × 0 ˙ Fin
111 34 rneqd φ ran F supp 0 ˙ F = ran F V × 0 ˙
112 rnresss ran F supp 0 ˙ F ran F
113 5 frnd φ ran F B
114 112 113 sstrid φ ran F supp 0 ˙ F B
115 111 114 eqsstrrd φ ran F V × 0 ˙ B
116 2ndrn Rel F V × 0 ˙ z F V × 0 ˙ 2 nd z ran F V × 0 ˙
117 28 116 sylan φ z F V × 0 ˙ 2 nd z ran F V × 0 ˙
118 relcnv Rel F -1
119 reldif Rel F -1 Rel F -1 0 ˙ × V
120 118 119 mp1i φ Rel F -1 0 ˙ × V
121 1st2nd Rel F -1 0 ˙ × V t F -1 0 ˙ × V t = 1 st t 2 nd t
122 120 121 sylan φ t F -1 0 ˙ × V t = 1 st t 2 nd t
123 cnvdif F V × 0 ˙ -1 = F -1 V × 0 ˙ -1
124 cnvxp V × 0 ˙ -1 = 0 ˙ × V
125 124 difeq2i F -1 V × 0 ˙ -1 = F -1 0 ˙ × V
126 123 125 eqtri F V × 0 ˙ -1 = F -1 0 ˙ × V
127 126 eqimss2i F -1 0 ˙ × V F V × 0 ˙ -1
128 127 a1i φ F -1 0 ˙ × V F V × 0 ˙ -1
129 128 sselda φ t F -1 0 ˙ × V t F V × 0 ˙ -1
130 122 129 eqeltrrd φ t F -1 0 ˙ × V 1 st t 2 nd t F V × 0 ˙ -1
131 106 105 opelcnv 1 st t 2 nd t F V × 0 ˙ -1 2 nd t 1 st t F V × 0 ˙
132 130 131 sylib φ t F -1 0 ˙ × V 2 nd t 1 st t F V × 0 ˙
133 28 adantr φ z F V × 0 ˙ Rel F V × 0 ˙
134 eqidd φ z F V × 0 ˙ z -1 = z -1
135 cnvf1olem Rel F V × 0 ˙ z F V × 0 ˙ z -1 = z -1 z -1 F V × 0 ˙ -1 z = z -1 -1
136 135 simpld Rel F V × 0 ˙ z F V × 0 ˙ z -1 = z -1 z -1 F V × 0 ˙ -1
137 133 97 134 136 syl12anc φ z F V × 0 ˙ z -1 F V × 0 ˙ -1
138 137 126 eleqtrdi φ z F V × 0 ˙ z -1 F -1 0 ˙ × V
139 eqeq2 u = z -1 t = u t = z -1
140 139 bibi2d u = z -1 z = 2 nd t 1 st t t = u z = 2 nd t 1 st t t = z -1
141 140 ralbidv u = z -1 t F -1 0 ˙ × V z = 2 nd t 1 st t t = u t F -1 0 ˙ × V z = 2 nd t 1 st t t = z -1
142 141 adantl φ z F V × 0 ˙ u = z -1 t F -1 0 ˙ × V z = 2 nd t 1 st t t = u t F -1 0 ˙ × V z = 2 nd t 1 st t t = z -1
143 118 119 mp1i φ z F V × 0 ˙ t F -1 0 ˙ × V z = 2 nd t 1 st t Rel F -1 0 ˙ × V
144 simplr φ z F V × 0 ˙ t F -1 0 ˙ × V z = 2 nd t 1 st t t F -1 0 ˙ × V
145 simpr φ z F V × 0 ˙ t F -1 0 ˙ × V z = 2 nd t 1 st t z = 2 nd t 1 st t
146 df-rel Rel F -1 0 ˙ × V F -1 0 ˙ × V V × V
147 120 146 sylib φ F -1 0 ˙ × V V × V
148 147 ad3antrrr φ z F V × 0 ˙ t F -1 0 ˙ × V z = 2 nd t 1 st t F -1 0 ˙ × V V × V
149 148 144 sseldd φ z F V × 0 ˙ t F -1 0 ˙ × V z = 2 nd t 1 st t t V × V
150 2nd1st t V × V t -1 = 2 nd t 1 st t
151 149 150 syl φ z F V × 0 ˙ t F -1 0 ˙ × V z = 2 nd t 1 st t t -1 = 2 nd t 1 st t
152 145 151 eqtr4d φ z F V × 0 ˙ t F -1 0 ˙ × V z = 2 nd t 1 st t z = t -1
153 cnvf1olem Rel F -1 0 ˙ × V t F -1 0 ˙ × V z = t -1 z F -1 0 ˙ × V -1 t = z -1
154 153 simprd Rel F -1 0 ˙ × V t F -1 0 ˙ × V z = t -1 t = z -1
155 143 144 152 154 syl12anc φ z F V × 0 ˙ t F -1 0 ˙ × V z = 2 nd t 1 st t t = z -1
156 28 ad3antrrr φ z F V × 0 ˙ t F -1 0 ˙ × V t = z -1 Rel F V × 0 ˙
157 97 ad2antrr φ z F V × 0 ˙ t F -1 0 ˙ × V t = z -1 z F V × 0 ˙
158 simpr φ z F V × 0 ˙ t F -1 0 ˙ × V t = z -1 t = z -1
159 cnvf1olem Rel F V × 0 ˙ z F V × 0 ˙ t = z -1 t F V × 0 ˙ -1 z = t -1
160 159 simprd Rel F V × 0 ˙ z F V × 0 ˙ t = z -1 z = t -1
161 156 157 158 160 syl12anc φ z F V × 0 ˙ t F -1 0 ˙ × V t = z -1 z = t -1
162 147 ad3antrrr φ z F V × 0 ˙ t F -1 0 ˙ × V t = z -1 F -1 0 ˙ × V V × V
163 simplr φ z F V × 0 ˙ t F -1 0 ˙ × V t = z -1 t F -1 0 ˙ × V
164 162 163 sseldd φ z F V × 0 ˙ t F -1 0 ˙ × V t = z -1 t V × V
165 164 150 syl φ z F V × 0 ˙ t F -1 0 ˙ × V t = z -1 t -1 = 2 nd t 1 st t
166 161 165 eqtrd φ z F V × 0 ˙ t F -1 0 ˙ × V t = z -1 z = 2 nd t 1 st t
167 155 166 impbida φ z F V × 0 ˙ t F -1 0 ˙ × V z = 2 nd t 1 st t t = z -1
168 167 ralrimiva φ z F V × 0 ˙ t F -1 0 ˙ × V z = 2 nd t 1 st t t = z -1
169 138 142 168 rspcedvd φ z F V × 0 ˙ u F -1 0 ˙ × V t F -1 0 ˙ × V z = 2 nd t 1 st t t = u
170 reu6 ∃! t F -1 0 ˙ × V z = 2 nd t 1 st t u F -1 0 ˙ × V t F -1 0 ˙ × V z = 2 nd t 1 st t t = u
171 169 170 sylibr φ z F V × 0 ˙ ∃! t F -1 0 ˙ × V z = 2 nd t 1 st t
172 104 1 2 107 4 110 115 117 132 171 gsummptf1o φ G z F V × 0 ˙ 2 nd z = G t F -1 0 ˙ × V 1 st t
173 fveq2 t = z 1 st t = 1 st z
174 173 cbvmptv t F -1 0 ˙ × V 1 st t = z F -1 0 ˙ × V 1 st z
175 34 cnveqd φ F supp 0 ˙ F -1 = F V × 0 ˙ -1
176 175 126 eqtr2di φ F -1 0 ˙ × V = F supp 0 ˙ F -1
177 176 mpteq1d φ z F -1 0 ˙ × V 1 st z = z F supp 0 ˙ F -1 1 st z
178 174 177 syl5eq φ t F -1 0 ˙ × V 1 st t = z F supp 0 ˙ F -1 1 st z
179 178 oveq2d φ G t F -1 0 ˙ × V 1 st t = G z F supp 0 ˙ F -1 1 st z
180 103 172 179 3eqtrd φ G F = G z F supp 0 ˙ F -1 1 st z
181 nfcv _ y 1 st z
182 nfv x φ
183 vex y V
184 75 183 op1std z = x y 1 st z = x
185 relcnv Rel F supp 0 ˙ F -1
186 185 a1i φ Rel F supp 0 ˙ F -1
187 cnvfi F supp 0 ˙ F Fin F supp 0 ˙ F -1 Fin
188 109 187 syl φ F supp 0 ˙ F -1 Fin
189 113 adantr φ z F supp 0 ˙ F -1 ran F B
190 185 a1i φ z F supp 0 ˙ F -1 Rel F supp 0 ˙ F -1
191 simpr φ z F supp 0 ˙ F -1 z F supp 0 ˙ F -1
192 1stdm Rel F supp 0 ˙ F -1 z F supp 0 ˙ F -1 1 st z dom F supp 0 ˙ F -1
193 190 191 192 syl2anc φ z F supp 0 ˙ F -1 1 st z dom F supp 0 ˙ F -1
194 df-rn ran F supp 0 ˙ F = dom F supp 0 ˙ F -1
195 193 194 eleqtrrdi φ z F supp 0 ˙ F -1 1 st z ran F supp 0 ˙ F
196 112 195 sselid φ z F supp 0 ˙ F -1 1 st z ran F
197 189 196 sseldd φ z F supp 0 ˙ F -1 1 st z B
198 181 182 1 184 186 188 4 197 gsummpt2d φ G z F supp 0 ˙ F -1 1 st z = G x dom F supp 0 ˙ F -1 G y F supp 0 ˙ F -1 x x
199 df-ima F F supp 0 ˙ = ran F supp 0 ˙ F
200 supppreima Fun F F V 0 ˙ V F supp 0 ˙ = F -1 ran F 0 ˙
201 25 13 32 200 syl3anc φ F supp 0 ˙ = F -1 ran F 0 ˙
202 201 imaeq2d φ F F supp 0 ˙ = F F -1 ran F 0 ˙
203 199 202 eqtr3id φ ran F supp 0 ˙ F = F F -1 ran F 0 ˙
204 funimacnv Fun F F F -1 ran F 0 ˙ = ran F 0 ˙ ran F
205 25 204 syl φ F F -1 ran F 0 ˙ = ran F 0 ˙ ran F
206 difssd φ ran F 0 ˙ ran F
207 df-ss ran F 0 ˙ ran F ran F 0 ˙ ran F = ran F 0 ˙
208 206 207 sylib φ ran F 0 ˙ ran F = ran F 0 ˙
209 203 205 208 3eqtrd φ ran F supp 0 ˙ F = ran F 0 ˙
210 194 209 eqtr3id φ dom F supp 0 ˙ F -1 = ran F 0 ˙
211 4 cmnmndd φ G Mnd
212 211 adantr φ x dom F supp 0 ˙ F -1 G Mnd
213 109 adantr φ x dom F supp 0 ˙ F -1 F supp 0 ˙ F Fin
214 imafi2 F supp 0 ˙ F -1 Fin F supp 0 ˙ F -1 x Fin
215 213 187 214 3syl φ x dom F supp 0 ˙ F -1 F supp 0 ˙ F -1 x Fin
216 194 114 eqsstrrid φ dom F supp 0 ˙ F -1 B
217 216 sselda φ x dom F supp 0 ˙ F -1 x B
218 1 3 gsumconst G Mnd F supp 0 ˙ F -1 x Fin x B G y F supp 0 ˙ F -1 x x = F supp 0 ˙ F -1 x · ˙ x
219 212 215 217 218 syl3anc φ x dom F supp 0 ˙ F -1 G y F supp 0 ˙ F -1 x x = F supp 0 ˙ F -1 x · ˙ x
220 cnvresima F supp 0 ˙ F -1 x = F -1 x supp 0 ˙ F
221 210 eleq2d φ x dom F supp 0 ˙ F -1 x ran F 0 ˙
222 221 biimpa φ x dom F supp 0 ˙ F -1 x ran F 0 ˙
223 222 snssd φ x dom F supp 0 ˙ F -1 x ran F 0 ˙
224 sspreima Fun F x ran F 0 ˙ F -1 x F -1 ran F 0 ˙
225 25 223 224 syl2an2r φ x dom F supp 0 ˙ F -1 F -1 x F -1 ran F 0 ˙
226 201 adantr φ x dom F supp 0 ˙ F -1 F supp 0 ˙ = F -1 ran F 0 ˙
227 225 226 sseqtrrd φ x dom F supp 0 ˙ F -1 F -1 x F supp 0 ˙
228 df-ss F -1 x F supp 0 ˙ F -1 x supp 0 ˙ F = F -1 x
229 227 228 sylib φ x dom F supp 0 ˙ F -1 F -1 x supp 0 ˙ F = F -1 x
230 220 229 eqtr2id φ x dom F supp 0 ˙ F -1 F -1 x = F supp 0 ˙ F -1 x
231 230 fveq2d φ x dom F supp 0 ˙ F -1 F -1 x = F supp 0 ˙ F -1 x
232 231 oveq1d φ x dom F supp 0 ˙ F -1 F -1 x · ˙ x = F supp 0 ˙ F -1 x · ˙ x
233 219 232 eqtr4d φ x dom F supp 0 ˙ F -1 G y F supp 0 ˙ F -1 x x = F -1 x · ˙ x
234 210 233 mpteq12dva φ x dom F supp 0 ˙ F -1 G y F supp 0 ˙ F -1 x x = x ran F 0 ˙ F -1 x · ˙ x
235 234 oveq2d φ G x dom F supp 0 ˙ F -1 G y F supp 0 ˙ F -1 x x = G x ran F 0 ˙ F -1 x · ˙ x
236 180 198 235 3eqtrd φ G F = G x ran F 0 ˙ F -1 x · ˙ x