Metamath Proof Explorer


Theorem gsumzf1o

Description: Re-index a finite group sum using a bijection. (Contributed by Mario Carneiro, 24-Apr-2016) (Revised by AV, 2-Jun-2019)

Ref Expression
Hypotheses gsumzcl.b
|- B = ( Base ` G )
gsumzcl.0
|- .0. = ( 0g ` G )
gsumzcl.z
|- Z = ( Cntz ` G )
gsumzcl.g
|- ( ph -> G e. Mnd )
gsumzcl.a
|- ( ph -> A e. V )
gsumzcl.f
|- ( ph -> F : A --> B )
gsumzcl.c
|- ( ph -> ran F C_ ( Z ` ran F ) )
gsumzcl.w
|- ( ph -> F finSupp .0. )
gsumzf1o.h
|- ( ph -> H : C -1-1-onto-> A )
Assertion gsumzf1o
|- ( ph -> ( G gsum F ) = ( G gsum ( F o. H ) ) )

Proof

Step Hyp Ref Expression
1 gsumzcl.b
 |-  B = ( Base ` G )
2 gsumzcl.0
 |-  .0. = ( 0g ` G )
3 gsumzcl.z
 |-  Z = ( Cntz ` G )
4 gsumzcl.g
 |-  ( ph -> G e. Mnd )
5 gsumzcl.a
 |-  ( ph -> A e. V )
6 gsumzcl.f
 |-  ( ph -> F : A --> B )
7 gsumzcl.c
 |-  ( ph -> ran F C_ ( Z ` ran F ) )
8 gsumzcl.w
 |-  ( ph -> F finSupp .0. )
9 gsumzf1o.h
 |-  ( ph -> H : C -1-1-onto-> A )
10 2 gsumz
 |-  ( ( G e. Mnd /\ A e. V ) -> ( G gsum ( k e. A |-> .0. ) ) = .0. )
11 4 5 10 syl2anc
 |-  ( ph -> ( G gsum ( k e. A |-> .0. ) ) = .0. )
12 f1of1
 |-  ( H : C -1-1-onto-> A -> H : C -1-1-> A )
13 9 12 syl
 |-  ( ph -> H : C -1-1-> A )
14 f1dmex
 |-  ( ( H : C -1-1-> A /\ A e. V ) -> C e. _V )
15 13 5 14 syl2anc
 |-  ( ph -> C e. _V )
16 2 gsumz
 |-  ( ( G e. Mnd /\ C e. _V ) -> ( G gsum ( x e. C |-> .0. ) ) = .0. )
17 4 15 16 syl2anc
 |-  ( ph -> ( G gsum ( x e. C |-> .0. ) ) = .0. )
18 11 17 eqtr4d
 |-  ( ph -> ( G gsum ( k e. A |-> .0. ) ) = ( G gsum ( x e. C |-> .0. ) ) )
19 18 adantr
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> ( G gsum ( k e. A |-> .0. ) ) = ( G gsum ( x e. C |-> .0. ) ) )
20 2 fvexi
 |-  .0. e. _V
21 20 a1i
 |-  ( ph -> .0. e. _V )
22 ssidd
 |-  ( ph -> ( F supp .0. ) C_ ( F supp .0. ) )
23 6 5 21 22 gsumcllem
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> F = ( k e. A |-> .0. ) )
24 23 oveq2d
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> ( G gsum F ) = ( G gsum ( k e. A |-> .0. ) ) )
25 f1of
 |-  ( H : C -1-1-onto-> A -> H : C --> A )
26 9 25 syl
 |-  ( ph -> H : C --> A )
27 26 adantr
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> H : C --> A )
28 27 ffvelrnda
 |-  ( ( ( ph /\ ( F supp .0. ) = (/) ) /\ x e. C ) -> ( H ` x ) e. A )
29 27 feqmptd
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> H = ( x e. C |-> ( H ` x ) ) )
30 eqidd
 |-  ( k = ( H ` x ) -> .0. = .0. )
31 28 29 23 30 fmptco
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> ( F o. H ) = ( x e. C |-> .0. ) )
32 31 oveq2d
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> ( G gsum ( F o. H ) ) = ( G gsum ( x e. C |-> .0. ) ) )
33 19 24 32 3eqtr4d
 |-  ( ( ph /\ ( F supp .0. ) = (/) ) -> ( G gsum F ) = ( G gsum ( F o. H ) ) )
34 33 ex
 |-  ( ph -> ( ( F supp .0. ) = (/) -> ( G gsum F ) = ( G gsum ( F o. H ) ) ) )
35 9 adantr
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> H : C -1-1-onto-> A )
36 f1ococnv2
 |-  ( H : C -1-1-onto-> A -> ( H o. `' H ) = ( _I |` A ) )
37 35 36 syl
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( H o. `' H ) = ( _I |` A ) )
38 37 coeq1d
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( ( H o. `' H ) o. f ) = ( ( _I |` A ) o. f ) )
39 f1of1
 |-  ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> ( F supp .0. ) )
40 39 ad2antll
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> ( F supp .0. ) )
41 suppssdm
 |-  ( F supp .0. ) C_ dom F
42 41 6 fssdm
 |-  ( ph -> ( F supp .0. ) C_ A )
43 42 adantr
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F supp .0. ) C_ A )
44 f1ss
 |-  ( ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> ( F supp .0. ) /\ ( F supp .0. ) C_ A ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> A )
45 40 43 44 syl2anc
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> A )
46 f1f
 |-  ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> A -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) --> A )
47 fcoi2
 |-  ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) --> A -> ( ( _I |` A ) o. f ) = f )
48 45 46 47 3syl
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( ( _I |` A ) o. f ) = f )
49 38 48 eqtrd
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( ( H o. `' H ) o. f ) = f )
50 coass
 |-  ( ( H o. `' H ) o. f ) = ( H o. ( `' H o. f ) )
51 49 50 eqtr3di
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> f = ( H o. ( `' H o. f ) ) )
52 51 coeq2d
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F o. f ) = ( F o. ( H o. ( `' H o. f ) ) ) )
53 coass
 |-  ( ( F o. H ) o. ( `' H o. f ) ) = ( F o. ( H o. ( `' H o. f ) ) )
54 52 53 eqtr4di
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F o. f ) = ( ( F o. H ) o. ( `' H o. f ) ) )
55 54 seqeq3d
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> seq 1 ( ( +g ` G ) , ( F o. f ) ) = seq 1 ( ( +g ` G ) , ( ( F o. H ) o. ( `' H o. f ) ) ) )
56 55 fveq1d
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( F supp .0. ) ) ) = ( seq 1 ( ( +g ` G ) , ( ( F o. H ) o. ( `' H o. f ) ) ) ` ( # ` ( F supp .0. ) ) ) )
57 eqid
 |-  ( +g ` G ) = ( +g ` G )
58 4 adantr
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> G e. Mnd )
59 5 adantr
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> A e. V )
60 6 adantr
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> F : A --> B )
61 7 adantr
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ran F C_ ( Z ` ran F ) )
62 simprl
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( # ` ( F supp .0. ) ) e. NN )
63 ssid
 |-  ( F supp .0. ) C_ ( F supp .0. )
64 f1ofo
 |-  ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -onto-> ( F supp .0. ) )
65 forn
 |-  ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -onto-> ( F supp .0. ) -> ran f = ( F supp .0. ) )
66 64 65 syl
 |-  ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> ran f = ( F supp .0. ) )
67 66 ad2antll
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ran f = ( F supp .0. ) )
68 63 67 sseqtrrid
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F supp .0. ) C_ ran f )
69 eqid
 |-  ( ( F o. f ) supp .0. ) = ( ( F o. f ) supp .0. )
70 1 2 57 3 58 59 60 61 62 45 68 69 gsumval3
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( G gsum F ) = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( F supp .0. ) ) ) )
71 15 adantr
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> C e. _V )
72 fco
 |-  ( ( F : A --> B /\ H : C --> A ) -> ( F o. H ) : C --> B )
73 6 26 72 syl2anc
 |-  ( ph -> ( F o. H ) : C --> B )
74 73 adantr
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F o. H ) : C --> B )
75 rncoss
 |-  ran ( F o. H ) C_ ran F
76 3 cntzidss
 |-  ( ( ran F C_ ( Z ` ran F ) /\ ran ( F o. H ) C_ ran F ) -> ran ( F o. H ) C_ ( Z ` ran ( F o. H ) ) )
77 7 75 76 sylancl
 |-  ( ph -> ran ( F o. H ) C_ ( Z ` ran ( F o. H ) ) )
78 77 adantr
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ran ( F o. H ) C_ ( Z ` ran ( F o. H ) ) )
79 f1ocnv
 |-  ( H : C -1-1-onto-> A -> `' H : A -1-1-onto-> C )
80 f1of1
 |-  ( `' H : A -1-1-onto-> C -> `' H : A -1-1-> C )
81 9 79 80 3syl
 |-  ( ph -> `' H : A -1-1-> C )
82 81 adantr
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> `' H : A -1-1-> C )
83 f1co
 |-  ( ( `' H : A -1-1-> C /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> A ) -> ( `' H o. f ) : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> C )
84 82 45 83 syl2anc
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( `' H o. f ) : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> C )
85 ssidd
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F supp .0. ) C_ ( F supp .0. ) )
86 6 5 fexd
 |-  ( ph -> F e. _V )
87 suppimacnv
 |-  ( ( F e. _V /\ .0. e. _V ) -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) )
88 86 20 87 sylancl
 |-  ( ph -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) )
89 88 eqcomd
 |-  ( ph -> ( `' F " ( _V \ { .0. } ) ) = ( F supp .0. ) )
90 89 adantr
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( `' F " ( _V \ { .0. } ) ) = ( F supp .0. ) )
91 85 90 67 3sstr4d
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( `' F " ( _V \ { .0. } ) ) C_ ran f )
92 imass2
 |-  ( ( `' F " ( _V \ { .0. } ) ) C_ ran f -> ( `' H " ( `' F " ( _V \ { .0. } ) ) ) C_ ( `' H " ran f ) )
93 91 92 syl
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( `' H " ( `' F " ( _V \ { .0. } ) ) ) C_ ( `' H " ran f ) )
94 cnvco
 |-  `' ( F o. H ) = ( `' H o. `' F )
95 94 imaeq1i
 |-  ( `' ( F o. H ) " ( _V \ { .0. } ) ) = ( ( `' H o. `' F ) " ( _V \ { .0. } ) )
96 imaco
 |-  ( ( `' H o. `' F ) " ( _V \ { .0. } ) ) = ( `' H " ( `' F " ( _V \ { .0. } ) ) )
97 95 96 eqtri
 |-  ( `' ( F o. H ) " ( _V \ { .0. } ) ) = ( `' H " ( `' F " ( _V \ { .0. } ) ) )
98 rnco2
 |-  ran ( `' H o. f ) = ( `' H " ran f )
99 93 97 98 3sstr4g
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( `' ( F o. H ) " ( _V \ { .0. } ) ) C_ ran ( `' H o. f ) )
100 f1oexrnex
 |-  ( ( H : C -1-1-onto-> A /\ A e. V ) -> H e. _V )
101 9 5 100 syl2anc
 |-  ( ph -> H e. _V )
102 coexg
 |-  ( ( F e. _V /\ H e. _V ) -> ( F o. H ) e. _V )
103 86 101 102 syl2anc
 |-  ( ph -> ( F o. H ) e. _V )
104 suppimacnv
 |-  ( ( ( F o. H ) e. _V /\ .0. e. _V ) -> ( ( F o. H ) supp .0. ) = ( `' ( F o. H ) " ( _V \ { .0. } ) ) )
105 103 20 104 sylancl
 |-  ( ph -> ( ( F o. H ) supp .0. ) = ( `' ( F o. H ) " ( _V \ { .0. } ) ) )
106 105 sseq1d
 |-  ( ph -> ( ( ( F o. H ) supp .0. ) C_ ran ( `' H o. f ) <-> ( `' ( F o. H ) " ( _V \ { .0. } ) ) C_ ran ( `' H o. f ) ) )
107 106 adantr
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( ( ( F o. H ) supp .0. ) C_ ran ( `' H o. f ) <-> ( `' ( F o. H ) " ( _V \ { .0. } ) ) C_ ran ( `' H o. f ) ) )
108 99 107 mpbird
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( ( F o. H ) supp .0. ) C_ ran ( `' H o. f ) )
109 eqid
 |-  ( ( ( F o. H ) o. ( `' H o. f ) ) supp .0. ) = ( ( ( F o. H ) o. ( `' H o. f ) ) supp .0. )
110 1 2 57 3 58 71 74 78 62 84 108 109 gsumval3
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( G gsum ( F o. H ) ) = ( seq 1 ( ( +g ` G ) , ( ( F o. H ) o. ( `' H o. f ) ) ) ` ( # ` ( F supp .0. ) ) ) )
111 56 70 110 3eqtr4d
 |-  ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( G gsum F ) = ( G gsum ( F o. H ) ) )
112 111 expr
 |-  ( ( ph /\ ( # ` ( F supp .0. ) ) e. NN ) -> ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> ( G gsum F ) = ( G gsum ( F o. H ) ) ) )
113 112 exlimdv
 |-  ( ( ph /\ ( # ` ( F supp .0. ) ) e. NN ) -> ( E. f f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> ( G gsum F ) = ( G gsum ( F o. H ) ) ) )
114 113 expimpd
 |-  ( ph -> ( ( ( # ` ( F supp .0. ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) -> ( G gsum F ) = ( G gsum ( F o. H ) ) ) )
115 fsuppimp
 |-  ( F finSupp .0. -> ( Fun F /\ ( F supp .0. ) e. Fin ) )
116 115 simprd
 |-  ( F finSupp .0. -> ( F supp .0. ) e. Fin )
117 fz1f1o
 |-  ( ( F supp .0. ) e. Fin -> ( ( F supp .0. ) = (/) \/ ( ( # ` ( F supp .0. ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) )
118 8 116 117 3syl
 |-  ( ph -> ( ( F supp .0. ) = (/) \/ ( ( # ` ( F supp .0. ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) )
119 34 114 118 mpjaod
 |-  ( ph -> ( G gsum F ) = ( G gsum ( F o. H ) ) )