Theorem gsumzf1o 15474

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

Hypotheses

Ref	Expression
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 " ( _V \ { .0. } ) ) e. Fin )
gsumzf1o.h	|- ( ph -> H : C -1-1-onto-> A )

Assertion

Ref	Expression
gsumzf1o	|- ( ph -> ( G gsumg F ) = ( G gsumg ( F o. H ) ) )

Proof of Theorem gsumzf1o

Dummy variables f k x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gsumzcl.g	. . . . . . 7 |- ( ph -> G e. Mnd )
2		gsumzcl.a	. . . . . . 7 |- ( ph -> A e. V )
3		gsumzcl.0	. . . . . . . 8 |- .0. = ( 0g ` G )
4	3	gsumz 14736	. . . . . . 7 |- ( ( G e. Mnd /\ A e. V ) -> ( G gsumg ( k e. A |-> .0. ) ) = .0. )
5	1, 2, 4	syl2anc 643	. . . . . 6 |- ( ph -> ( G gsumg ( k e. A |-> .0. ) ) = .0. )
6		gsumzf1o.h	. . . . . . . . 9 |- ( ph -> H : C -1-1-onto-> A )
7		f1of1 5632	. . . . . . . . 9 |- ( H : C -1-1-onto-> A -> H : C -1-1-> A )
8	6, 7	syl 16	. . . . . . . 8 |- ( ph -> H : C -1-1-> A )
9		f1dmex 5930	. . . . . . . 8 |- ( ( H : C -1-1-> A /\ A e. V ) -> C e. _V )
10	8, 2, 9	syl2anc 643	. . . . . . 7 |- ( ph -> C e. _V )
11	3	gsumz 14736	. . . . . . 7 |- ( ( G e. Mnd /\ C e. _V ) -> ( G gsumg ( x e. C |-> .0. ) ) = .0. )
12	1, 10, 11	syl2anc 643	. . . . . 6 |- ( ph -> ( G gsumg ( x e. C |-> .0. ) ) = .0. )
13	5, 12	eqtr4d 2439	. . . . 5 |- ( ph -> ( G gsumg ( k e. A |-> .0. ) ) = ( G gsumg ( x e. C |-> .0. ) ) )
14	13	adantr 452	. . . 4 |- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( G gsumg ( k e. A |-> .0. ) ) = ( G gsumg ( x e. C |-> .0. ) ) )
15		gsumzcl.f	. . . . . 6 |- ( ph -> F : A --> B )
16		ssid 3327	. . . . . . 7 |- ( `' F " ( _V \ { .0. } ) ) C_ ( `' F " ( _V \ { .0. } ) )
17	16	a1i 11	. . . . . 6 |- ( ph -> ( `' F " ( _V \ { .0. } ) ) C_ ( `' F " ( _V \ { .0. } ) ) )
18	15, 17	gsumcllem 15471	. . . . 5 |- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> F = ( k e. A |-> .0. ) )
19	18	oveq2d 6056	. . . 4 |- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( G gsumg F ) = ( G gsumg ( k e. A |-> .0. ) ) )
20		f1of 5633	. . . . . . . . 9 |- ( H : C -1-1-onto-> A -> H : C --> A )
21	6, 20	syl 16	. . . . . . . 8 |- ( ph -> H : C --> A )
22	21	adantr 452	. . . . . . 7 |- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> H : C --> A )
23	22	ffvelrnda 5829	. . . . . 6 |- ( ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) /\ x e. C ) -> ( H ` x ) e. A )
24	22	feqmptd 5738	. . . . . 6 |- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> H = ( x e. C |-> ( H ` x ) ) )
25		eqidd 2405	. . . . . 6 |- ( k = ( H ` x ) -> .0. = .0. )
26	23, 24, 18, 25	fmptco 5860	. . . . 5 |- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( F o. H ) = ( x e. C |-> .0. ) )
27	26	oveq2d 6056	. . . 4 |- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( G gsumg ( F o. H ) ) = ( G gsumg ( x e. C |-> .0. ) ) )
28	14, 19, 27	3eqtr4d 2446	. . 3 |- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( G gsumg F ) = ( G gsumg ( F o. H ) ) )
29	28	ex 424	. 2 |- ( ph -> ( ( `' F " ( _V \ { .0. } ) ) = (/) -> ( G gsumg F ) = ( G gsumg ( F o. H ) ) ) )
30		coass 5347	. . . . . . . . . . 11 |- ( ( H o. `' H ) o. f ) = ( H o. ( `' H o. f ) )
31	6	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> H : C -1-1-onto-> A )
32		f1ococnv2 5661	. . . . . . . . . . . . . 14 |- ( H : C -1-1-onto-> A -> ( H o. `' H ) = ( _I |` A ) )
33	31, 32	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( H o. `' H ) = ( _I |` A ) )
34	33	coeq1d 4993	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( ( H o. `' H ) o. f ) = ( ( _I |` A ) o. f ) )
35		f1of1 5632	. . . . . . . . . . . . . . 15 |- ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> ( `' F " ( _V \ { .0. } ) ) )
36	35	ad2antll 710	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> ( `' F " ( _V \ { .0. } ) ) )
37		cnvimass 5183	. . . . . . . . . . . . . . . 16 |- ( `' F " ( _V \ { .0. } ) ) C_ dom F
38		fdm 5554	. . . . . . . . . . . . . . . . 17 |- ( F : A --> B -> dom F = A )
39	15, 38	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> dom F = A )
40	37, 39	syl5sseq 3356	. . . . . . . . . . . . . . 15 |- ( ph -> ( `' F " ( _V \ { .0. } ) ) C_ A )
41	40	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( `' F " ( _V \ { .0. } ) ) C_ A )
42		f1ss 5603	. . . . . . . . . . . . . 14 |- ( ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> ( `' F " ( _V \ { .0. } ) ) /\ ( `' F " ( _V \ { .0. } ) ) C_ A ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> A )
43	36, 41, 42	syl2anc 643	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> A )
44		f1f 5598	. . . . . . . . . . . . 13 |- ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> A -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) --> A )
45		fcoi2 5577	. . . . . . . . . . . . 13 |- ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) --> A -> ( ( _I |` A ) o. f ) = f )
46	43, 44, 45	3syl 19	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( ( _I |` A ) o. f ) = f )
47	34, 46	eqtrd 2436	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( ( H o. `' H ) o. f ) = f )
48	30, 47	syl5reqr 2451	. . . . . . . . . 10 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> f = ( H o. ( `' H o. f ) ) )
49	48	coeq2d 4994	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( F o. f ) = ( F o. ( H o. ( `' H o. f ) ) ) )
50		coass 5347	. . . . . . . . 9 |- ( ( F o. H ) o. ( `' H o. f ) ) = ( F o. ( H o. ( `' H o. f ) ) )
51	49, 50	syl6eqr 2454	. . . . . . . 8 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( F o. f ) = ( ( F o. H ) o. ( `' H o. f ) ) )
52	51	seqeq3d 11286	. . . . . . 7 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> seq 1 ( ( +g ` G ) , ( F o. f ) ) = seq 1 ( ( +g ` G ) , ( ( F o. H ) o. ( `' H o. f ) ) ) )
53	52	fveq1d 5689	. . . . . 6 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) = ( seq 1 ( ( +g ` G ) , ( ( F o. H ) o. ( `' H o. f ) ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) )
54		gsumzcl.b	. . . . . . 7 |- B = ( Base ` G )
55		eqid 2404	. . . . . . 7 |- ( +g ` G ) = ( +g ` G )
56		gsumzcl.z	. . . . . . 7 |- Z = (Cntz ` G )
57	1	adantr 452	. . . . . . 7 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> G e. Mnd )
58	2	adantr 452	. . . . . . 7 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> A e. V )
59	15	adantr 452	. . . . . . 7 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> F : A --> B )
60		gsumzcl.c	. . . . . . . 8 |- ( ph -> ran F C_ ( Z ` ran F ) )
61	60	adantr 452	. . . . . . 7 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ran F C_ ( Z ` ran F ) )
62		simprl 733	. . . . . . 7 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN )
63		f1ofo 5640	. . . . . . . . . 10 |- ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -onto-> ( `' F " ( _V \ { .0. } ) ) )
64		forn 5615	. . . . . . . . . 10 |- ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -onto-> ( `' F " ( _V \ { .0. } ) ) -> ran f = ( `' F " ( _V \ { .0. } ) ) )
65	63, 64	syl 16	. . . . . . . . 9 |- ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> ran f = ( `' F " ( _V \ { .0. } ) ) )
66	65	ad2antll 710	. . . . . . . 8 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ran f = ( `' F " ( _V \ { .0. } ) ) )
67	16, 66	syl5sseqr 3357	. . . . . . 7 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( `' F " ( _V \ { .0. } ) ) C_ ran f )
68		eqid 2404	. . . . . . 7 |- ( `' ( F o. f ) " ( _V \ { .0. } ) ) = ( `' ( F o. f ) " ( _V \ { .0. } ) )
69	54, 3, 55, 56, 57, 58, 59, 61, 62, 43, 67, 68	gsumval3 15469	. . . . . 6 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( G gsumg F ) = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) )
70	10	adantr 452	. . . . . . 7 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> C e. _V )
71		fco 5559	. . . . . . . . 9 |- ( ( F : A --> B /\ H : C --> A ) -> ( F o. H ) : C --> B )
72	15, 21, 71	syl2anc 643	. . . . . . . 8 |- ( ph -> ( F o. H ) : C --> B )
73	72	adantr 452	. . . . . . 7 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( F o. H ) : C --> B )
74		rncoss 5095	. . . . . . . . 9 |- ran ( F o. H ) C_ ran F
75	56	cntzidss 15091	. . . . . . . . 9 |- ( ( ran F C_ ( Z ` ran F ) /\ ran ( F o. H ) C_ ran F ) -> ran ( F o. H ) C_ ( Z ` ran ( F o. H ) ) )
76	60, 74, 75	sylancl 644	. . . . . . . 8 |- ( ph -> ran ( F o. H ) C_ ( Z ` ran ( F o. H ) ) )
77	76	adantr 452	. . . . . . 7 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ran ( F o. H ) C_ ( Z ` ran ( F o. H ) ) )
78		f1ocnv 5646	. . . . . . . . . 10 |- ( H : C -1-1-onto-> A -> `' H : A -1-1-onto-> C )
79		f1of1 5632	. . . . . . . . . 10 |- ( `' H : A -1-1-onto-> C -> `' H : A -1-1-> C )
80	6, 78, 79	3syl 19	. . . . . . . . 9 |- ( ph -> `' H : A -1-1-> C )
81	80	adantr 452	. . . . . . . 8 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> `' H : A -1-1-> C )
82		f1co 5607	. . . . . . . 8 |- ( ( `' H : A -1-1-> C /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> A ) -> ( `' H o. f ) : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> C )
83	81, 43, 82	syl2anc 643	. . . . . . 7 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( `' H o. f ) : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> C )
84		imass2 5199	. . . . . . . . 9 |- ( ( `' F " ( _V \ { .0. } ) ) C_ ran f -> ( `' H " ( `' F " ( _V \ { .0. } ) ) ) C_ ( `' H " ran f ) )
85	67, 84	syl 16	. . . . . . . 8 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( `' H " ( `' F " ( _V \ { .0. } ) ) ) C_ ( `' H " ran f ) )
86		cnvco 5015	. . . . . . . . . 10 |- `' ( F o. H ) = ( `' H o. `' F )
87	86	imaeq1i 5159	. . . . . . . . 9 |- ( `' ( F o. H ) " ( _V \ { .0. } ) ) = ( ( `' H o. `' F ) " ( _V \ { .0. } ) )
88		imaco 5334	. . . . . . . . 9 |- ( ( `' H o. `' F ) " ( _V \ { .0. } ) ) = ( `' H " ( `' F " ( _V \ { .0. } ) ) )
89	87, 88	eqtri 2424	. . . . . . . 8 |- ( `' ( F o. H ) " ( _V \ { .0. } ) ) = ( `' H " ( `' F " ( _V \ { .0. } ) ) )
90		rnco2 5336	. . . . . . . 8 |- ran ( `' H o. f ) = ( `' H " ran f )
91	85, 89, 90	3sstr4g 3349	. . . . . . 7 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( `' ( F o. H ) " ( _V \ { .0. } ) ) C_ ran ( `' H o. f ) )
92		eqid 2404	. . . . . . 7 |- ( `' ( ( F o. H ) o. ( `' H o. f ) ) " ( _V \ { .0. } ) ) = ( `' ( ( F o. H ) o. ( `' H o. f ) ) " ( _V \ { .0. } ) )
93	54, 3, 55, 56, 57, 70, 73, 77, 62, 83, 91, 92	gsumval3 15469	. . . . . 6 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( G gsumg ( F o. H ) ) = ( seq 1 ( ( +g ` G ) , ( ( F o. H ) o. ( `' H o. f ) ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) )
94	53, 69, 93	3eqtr4d 2446	. . . . 5 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( G gsumg F ) = ( G gsumg ( F o. H ) ) )
95	94	expr 599	. . . 4 |- ( ( ph /\ ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN ) -> ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> ( G gsumg F ) = ( G gsumg ( F o. H ) ) ) )
96	95	exlimdv 1643	. . 3 |- ( ( ph /\ ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN ) -> ( E. f f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> ( G gsumg F ) = ( G gsumg ( F o. H ) ) ) )
97	96	expimpd 587	. 2 |- ( ph -> ( ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) -> ( G gsumg F ) = ( G gsumg ( F o. H ) ) ) )
98		gsumzcl.w	. . 3 |- ( ph -> ( `' F " ( _V \ { .0. } ) ) e. Fin )
99		fz1f1o 12459	. . 3 |- ( ( `' F " ( _V \ { .0. } ) ) e. Fin -> ( ( `' F " ( _V \ { .0. } ) ) = (/) \/ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) )
100	98, 99	syl 16	. 2 |- ( ph -> ( ( `' F " ( _V \ { .0. } ) ) = (/) \/ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) )
101	29, 97, 100	mpjaod 371	1 |- ( ph -> ( G gsumg F ) = ( G gsumg ( F o. H ) ) )

Syntax hints:   -> wi 4   \/ wo 358   /\ wa 359   E.wex 1547   = wceq 1649   e. wcel 1721   _Vcvv 2916   \ cdif 3277   C_ wss 3280   (/)c0 3588   {csn 3774   e. cmpt 4226   _I cid 4453   `'ccnv 4836   dom cdm 4837   ran crn 4838   |` cres 4839   "cima 4840   o. ccom 4841   -->wf 5409   -1-1->wf1 5410   -onto->wfo 5411   -1-1-onto->wf1o 5412   ` cfv 5413  (class class class)co 6040   Fincfn 7068   1c1 8947   NNcn 9956   ...cfz 10999   seq cseq 11278   #chash 11573   Basecbs 13424   +g cplusg 13484   0gc0g 13678   gsum_g cgsu 13679   Mndcmnd 14639  Cntzccntz 15069

This theorem is referenced by:  gsumf1o  15477

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-oi 7435  df-card 7782  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-nn 9957  df-n0 10178  df-z 10239  df-uz 10445  df-fz 11000  df-fzo 11091  df-seq 11279  df-hash 11574  df-0g 13682  df-gsum 13683  df-mnd 14645  df-cntz 15071