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		coass	|- ( ( H o. `' H ) o. f ) = ( H o. ( `' H o. f ) )
36	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 )
37		f1ococnv2	|- ( H : C -1-1-onto-> A -> ( H o. `' H ) = ( _I |` A ) )
38	36 37	syl	|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( H o. `' H ) = ( _I |` A ) )
39	38	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 ) )
40		f1of1	|- ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> ( F supp .0. ) )
41	40	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. ) )
42		suppssdm	|- ( F supp .0. ) C_ dom F
43	42 6	fssdm	|- ( ph -> ( F supp .0. ) C_ A )
44	43	adantr	|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F supp .0. ) C_ A )
45		f1ss	|- ( ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> ( F supp .0. ) /\ ( F supp .0. ) C_ A ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> A )
46	41 44 45	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 )
47		f1f	|- ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> A -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) --> A )
48		fcoi2	|- ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) --> A -> ( ( _I |` A ) o. f ) = f )
49	46 47 48	3syl	|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( ( _I |` A ) o. f ) = f )
50	39 49	eqtrd	|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( ( H o. `' H ) o. f ) = f )
51	35 50	syl5reqr	|- ( ( 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 46 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 46 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		fex	|- ( ( F : A --> B /\ A e. V ) -> F e. _V )
87	6 5 86	syl2anc	|- ( ph -> F e. _V )
88		suppimacnv	|- ( ( F e. _V /\ .0. e. _V ) -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) )
89	87 20 88	sylancl	|- ( ph -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) )
90	89	eqcomd	|- ( ph -> ( `' F " ( _V \ { .0. } ) ) = ( F supp .0. ) )
91	90	adantr	|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( `' F " ( _V \ { .0. } ) ) = ( F supp .0. ) )
92	85 91 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 )
93		imass2	|- ( ( `' F " ( _V \ { .0. } ) ) C_ ran f -> ( `' H " ( `' F " ( _V \ { .0. } ) ) ) C_ ( `' H " ran f ) )
94	92 93	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 ) )
95		cnvco	|- `' ( F o. H ) = ( `' H o. `' F )
96	95	imaeq1i	|- ( `' ( F o. H ) " ( _V \ { .0. } ) ) = ( ( `' H o. `' F ) " ( _V \ { .0. } ) )
97		imaco	|- ( ( `' H o. `' F ) " ( _V \ { .0. } ) ) = ( `' H " ( `' F " ( _V \ { .0. } ) ) )
98	96 97	eqtri	|- ( `' ( F o. H ) " ( _V \ { .0. } ) ) = ( `' H " ( `' F " ( _V \ { .0. } ) ) )
99		rnco2	|- ran ( `' H o. f ) = ( `' H " ran f )
100	94 98 99	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 ) )
101		f1oexrnex	|- ( ( H : C -1-1-onto-> A /\ A e. V ) -> H e. _V )
102	9 5 101	syl2anc	|- ( ph -> H e. _V )
103		coexg	|- ( ( F e. _V /\ H e. _V ) -> ( F o. H ) e. _V )
104	87 102 103	syl2anc	|- ( ph -> ( F o. H ) e. _V )
105		suppimacnv	|- ( ( ( F o. H ) e. _V /\ .0. e. _V ) -> ( ( F o. H ) supp .0. ) = ( `' ( F o. H ) " ( _V \ { .0. } ) ) )
106	104 20 105	sylancl	|- ( ph -> ( ( F o. H ) supp .0. ) = ( `' ( F o. H ) " ( _V \ { .0. } ) ) )
107	106	sseq1d	|- ( ph -> ( ( ( F o. H ) supp .0. ) C_ ran ( `' H o. f ) <-> ( `' ( F o. H ) " ( _V \ { .0. } ) ) C_ ran ( `' H o. f ) ) )
108	107	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 ) ) )
109	100 108	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 ) )
110		eqid	|- ( ( ( F o. H ) o. ( `' H o. f ) ) supp .0. ) = ( ( ( F o. H ) o. ( `' H o. f ) ) supp .0. )
111	1 2 57 3 58 71 74 78 62 84 109 110	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. ) ) ) )
112	56 70 111	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 ) ) )
113	112	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 ) ) ) )
114	113	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 ) ) ) )
115	114	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 ) ) ) )
116		fsuppimp	|- ( F finSupp .0. -> ( Fun F /\ ( F supp .0. ) e. Fin ) )
117	116	simprd	|- ( F finSupp .0. -> ( F supp .0. ) e. Fin )
118		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. ) ) ) )
119	8 117 118	3syl	|- ( ph -> ( ( F supp .0. ) = (/) \/ ( ( # ` ( F supp .0. ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) )
120	34 115 119	mpjaod	|- ( ph -> ( G gsum F ) = ( G gsum ( F o. H ) ) )