Theorem gsumzaddlem 17542

Description: The sum of two group sums. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 5-Jun-2019.)

Hypotheses

Ref	Expression
gsumzadd.b	|- B = ( Base ` G )
gsumzadd.0	|- .0. = ( 0g ` G )
gsumzadd.p	|- .+ = ( +g ` G )
gsumzadd.z	|- Z = (Cntz ` G )
gsumzadd.g	|- ( ph -> G e. Mnd )
gsumzadd.a	|- ( ph -> A e. V )
gsumzadd.fn	|- ( ph -> F finSupp .0. )
gsumzadd.hn	|- ( ph -> H finSupp .0. )
gsumzaddlem.w	|- W = ( ( F u. H ) supp .0. )
gsumzaddlem.f	|- ( ph -> F : A --> B )
gsumzaddlem.h	|- ( ph -> H : A --> B )
gsumzaddlem.1	|- ( ph -> ran F C_ ( Z ` ran F ) )
gsumzaddlem.2	|- ( ph -> ran H C_ ( Z ` ran H ) )
gsumzaddlem.3	|- ( ph -> ran ( F oF .+ H ) C_ ( Z ` ran ( F oF .+ H ) ) )
gsumzaddlem.4	|- ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) )

Assertion

Ref	Expression
gsumzaddlem	|- ( ph -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )

Distinct variable groups:   x, k, .+   .0. , k, x   k, F, x   k, G, x   A, k, x   B, k, x   k, H, x   ph, k, x   x, V   k, W, x   k, Z, x

Allowed substitution hint:   V( k)

Proof of Theorem gsumzaddlem

Dummy variables f n w y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gsumzadd.g	. . . . . 6 |- ( ph -> G e. Mnd )
2		gsumzadd.b	. . . . . . . 8 |- B = ( Base ` G )
3		gsumzadd.0	. . . . . . . 8 |- .0. = ( 0g ` G )
4	2, 3	mndidcl 16542	. . . . . . 7 |- ( G e. Mnd -> .0. e. B )
5	1, 4	syl 17	. . . . . 6 |- ( ph -> .0. e. B )
6		gsumzadd.p	. . . . . . 7 |- .+ = ( +g ` G )
7	2, 6, 3	mndlid 16545	. . . . . 6 |- ( ( G e. Mnd /\ .0. e. B ) -> ( .0. .+ .0. ) = .0. )
8	1, 5, 7	syl2anc 665	. . . . 5 |- ( ph -> ( .0. .+ .0. ) = .0. )
9	8	adantr 466	. . . 4 |- ( ( ph /\ W = (/) ) -> ( .0. .+ .0. ) = .0. )
10		gsumzaddlem.f	. . . . . . . 8 |- ( ph -> F : A --> B )
11		gsumzadd.a	. . . . . . . 8 |- ( ph -> A e. V )
12		fvex 5888	. . . . . . . . . 10 |- ( 0g ` G ) e. _V
13	3, 12	eqeltri 2506	. . . . . . . . 9 |- .0. e. _V
14	13	a1i 11	. . . . . . . 8 |- ( ph -> .0. e. _V )
15		gsumzaddlem.h	. . . . . . . . . . 11 |- ( ph -> H : A --> B )
16		fex 6150	. . . . . . . . . . 11 |- ( ( H : A --> B /\ A e. V ) -> H e. _V )
17	15, 11, 16	syl2anc 665	. . . . . . . . . 10 |- ( ph -> H e. _V )
18	17	suppun 6943	. . . . . . . . 9 |- ( ph -> ( F supp .0. ) C_ ( ( F u. H ) supp .0. ) )
19		gsumzaddlem.w	. . . . . . . . 9 |- W = ( ( F u. H ) supp .0. )
20	18, 19	syl6sseqr 3511	. . . . . . . 8 |- ( ph -> ( F supp .0. ) C_ W )
21	10, 11, 14, 20	gsumcllem 17530	. . . . . . 7 |- ( ( ph /\ W = (/) ) -> F = ( x e. A |-> .0. ) )
22	21	oveq2d 6318	. . . . . 6 |- ( ( ph /\ W = (/) ) -> ( G gsumg F ) = ( G gsumg ( x e. A |-> .0. ) ) )
23	3	gsumz 16609	. . . . . . . 8 |- ( ( G e. Mnd /\ A e. V ) -> ( G gsumg ( x e. A |-> .0. ) ) = .0. )
24	1, 11, 23	syl2anc 665	. . . . . . 7 |- ( ph -> ( G gsumg ( x e. A |-> .0. ) ) = .0. )
25	24	adantr 466	. . . . . 6 |- ( ( ph /\ W = (/) ) -> ( G gsumg ( x e. A |-> .0. ) ) = .0. )
26	22, 25	eqtrd 2463	. . . . 5 |- ( ( ph /\ W = (/) ) -> ( G gsumg F ) = .0. )
27		fex 6150	. . . . . . . . . . . 12 |- ( ( F : A --> B /\ A e. V ) -> F e. _V )
28	10, 11, 27	syl2anc 665	. . . . . . . . . . 11 |- ( ph -> F e. _V )
29	28	suppun 6943	. . . . . . . . . 10 |- ( ph -> ( H supp .0. ) C_ ( ( H u. F ) supp .0. ) )
30		uncom 3610	. . . . . . . . . . 11 |- ( F u. H ) = ( H u. F )
31	30	oveq1i 6312	. . . . . . . . . 10 |- ( ( F u. H ) supp .0. ) = ( ( H u. F ) supp .0. )
32	29, 31	syl6sseqr 3511	. . . . . . . . 9 |- ( ph -> ( H supp .0. ) C_ ( ( F u. H ) supp .0. ) )
33	32, 19	syl6sseqr 3511	. . . . . . . 8 |- ( ph -> ( H supp .0. ) C_ W )
34	15, 11, 14, 33	gsumcllem 17530	. . . . . . 7 |- ( ( ph /\ W = (/) ) -> H = ( x e. A |-> .0. ) )
35	34	oveq2d 6318	. . . . . 6 |- ( ( ph /\ W = (/) ) -> ( G gsumg H ) = ( G gsumg ( x e. A |-> .0. ) ) )
36	35, 25	eqtrd 2463	. . . . 5 |- ( ( ph /\ W = (/) ) -> ( G gsumg H ) = .0. )
37	26, 36	oveq12d 6320	. . . 4 |- ( ( ph /\ W = (/) ) -> ( ( G gsumg F ) .+ ( G gsumg H ) ) = ( .0. .+ .0. ) )
38	11	adantr 466	. . . . . . . 8 |- ( ( ph /\ W = (/) ) -> A e. V )
39	5	ad2antrr 730	. . . . . . . 8 |- ( ( ( ph /\ W = (/) ) /\ x e. A ) -> .0. e. B )
40	38, 39, 39, 21, 34	offval2 6559	. . . . . . 7 |- ( ( ph /\ W = (/) ) -> ( F oF .+ H ) = ( x e. A |-> ( .0. .+ .0. ) ) )
41	9	mpteq2dv 4508	. . . . . . 7 |- ( ( ph /\ W = (/) ) -> ( x e. A |-> ( .0. .+ .0. ) ) = ( x e. A |-> .0. ) )
42	40, 41	eqtrd 2463	. . . . . 6 |- ( ( ph /\ W = (/) ) -> ( F oF .+ H ) = ( x e. A |-> .0. ) )
43	42	oveq2d 6318	. . . . 5 |- ( ( ph /\ W = (/) ) -> ( G gsumg ( F oF .+ H ) ) = ( G gsumg ( x e. A |-> .0. ) ) )
44	43, 25	eqtrd 2463	. . . 4 |- ( ( ph /\ W = (/) ) -> ( G gsumg ( F oF .+ H ) ) = .0. )
45	9, 37, 44	3eqtr4rd 2474	. . 3 |- ( ( ph /\ W = (/) ) -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )
46	45	ex 435	. 2 |- ( ph -> ( W = (/) -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) ) )
47	1	adantr 466	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> G e. Mnd )
48	2, 6	mndcl 16533	. . . . . . . . . 10 |- ( ( G e. Mnd /\ z e. B /\ w e. B ) -> ( z .+ w ) e. B )
49	48	3expb 1206	. . . . . . . . 9 |- ( ( G e. Mnd /\ ( z e. B /\ w e. B ) ) -> ( z .+ w ) e. B )
50	47, 49	sylan 473	. . . . . . . 8 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ ( z e. B /\ w e. B ) ) -> ( z .+ w ) e. B )
51	50	caovclg 6472	. . . . . . 7 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
52		simprl 762	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( # ` W ) e. NN )
53		nnuz 11195	. . . . . . . 8 |- NN = ( ZZ>= ` 1 )
54	52, 53	syl6eleq 2520	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( # ` W ) e. ( ZZ>= ` 1 ) )
55	10	adantr 466	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> F : A --> B )
56		f1of1 5827	. . . . . . . . . . . 12 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> f : ( 1 ... ( # ` W ) ) -1-1-> W )
57	56	ad2antll 733	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> f : ( 1 ... ( # ` W ) ) -1-1-> W )
58		suppssdm 6935	. . . . . . . . . . . . . 14 |- ( ( F u. H ) supp .0. ) C_ dom ( F u. H )
59	58	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> ( ( F u. H ) supp .0. ) C_ dom ( F u. H ) )
60	19	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> W = ( ( F u. H ) supp .0. ) )
61		dmun 5057	. . . . . . . . . . . . . 14 |- dom ( F u. H ) = ( dom F u. dom H )
62		fdm 5747	. . . . . . . . . . . . . . . . 17 |- ( F : A --> B -> dom F = A )
63	10, 62	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> dom F = A )
64		fdm 5747	. . . . . . . . . . . . . . . . 17 |- ( H : A --> B -> dom H = A )
65	15, 64	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> dom H = A )
66	63, 65	uneq12d 3621	. . . . . . . . . . . . . . 15 |- ( ph -> ( dom F u. dom H ) = ( A u. A ) )
67		unidm 3609	. . . . . . . . . . . . . . 15 |- ( A u. A ) = A
68	66, 67	syl6eq 2479	. . . . . . . . . . . . . 14 |- ( ph -> ( dom F u. dom H ) = A )
69	61, 68	syl5req 2476	. . . . . . . . . . . . 13 |- ( ph -> A = dom ( F u. H ) )
70	59, 60, 69	3sstr4d 3507	. . . . . . . . . . . 12 |- ( ph -> W C_ A )
71	70	adantr 466	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> W C_ A )
72		f1ss 5798	. . . . . . . . . . 11 |- ( ( f : ( 1 ... ( # ` W ) ) -1-1-> W /\ W C_ A ) -> f : ( 1 ... ( # ` W ) ) -1-1-> A )
73	57, 71, 72	syl2anc 665	. . . . . . . . . 10 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> f : ( 1 ... ( # ` W ) ) -1-1-> A )
74		f1f 5793	. . . . . . . . . 10 |- ( f : ( 1 ... ( # ` W ) ) -1-1-> A -> f : ( 1 ... ( # ` W ) ) --> A )
75	73, 74	syl 17	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> f : ( 1 ... ( # ` W ) ) --> A )
76		fco 5753	. . . . . . . . 9 |- ( ( F : A --> B /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( F o. f ) : ( 1 ... ( # ` W ) ) --> B )
77	55, 75, 76	syl2anc 665	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F o. f ) : ( 1 ... ( # ` W ) ) --> B )
78	77	ffvelrnda 6034	. . . . . . 7 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. f ) ` k ) e. B )
79	15	adantr 466	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> H : A --> B )
80		fco 5753	. . . . . . . . 9 |- ( ( H : A --> B /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( H o. f ) : ( 1 ... ( # ` W ) ) --> B )
81	79, 75, 80	syl2anc 665	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H o. f ) : ( 1 ... ( # ` W ) ) --> B )
82	81	ffvelrnda 6034	. . . . . . 7 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( H o. f ) ` k ) e. B )
83		ffn 5743	. . . . . . . . . . . 12 |- ( F : A --> B -> F Fn A )
84	55, 83	syl 17	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> F Fn A )
85		ffn 5743	. . . . . . . . . . . 12 |- ( H : A --> B -> H Fn A )
86	79, 85	syl 17	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> H Fn A )
87	11	adantr 466	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> A e. V )
88		ovex 6330	. . . . . . . . . . . 12 |- ( 1 ... ( # ` W ) ) e. _V
89	88	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( 1 ... ( # ` W ) ) e. _V )
90		inidm 3671	. . . . . . . . . . 11 |- ( A i^i A ) = A
91	84, 86, 75, 87, 87, 89, 90	ofco 6562	. . . . . . . . . 10 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( ( F oF .+ H ) o. f ) = ( ( F o. f ) oF .+ ( H o. f ) ) )
92	91	fveq1d 5880	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( ( ( F oF .+ H ) o. f ) ` k ) = ( ( ( F o. f ) oF .+ ( H o. f ) ) ` k ) )
93	92	adantr 466	. . . . . . . 8 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( ( F oF .+ H ) o. f ) ` k ) = ( ( ( F o. f ) oF .+ ( H o. f ) ) ` k ) )
94		fnfco 5762	. . . . . . . . . 10 |- ( ( F Fn A /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( F o. f ) Fn ( 1 ... ( # ` W ) ) )
95	84, 75, 94	syl2anc 665	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F o. f ) Fn ( 1 ... ( # ` W ) ) )
96		fnfco 5762	. . . . . . . . . 10 |- ( ( H Fn A /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( H o. f ) Fn ( 1 ... ( # ` W ) ) )
97	86, 75, 96	syl2anc 665	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H o. f ) Fn ( 1 ... ( # ` W ) ) )
98		inidm 3671	. . . . . . . . 9 |- ( ( 1 ... ( # ` W ) ) i^i ( 1 ... ( # ` W ) ) ) = ( 1 ... ( # ` W ) )
99		eqidd 2423	. . . . . . . . 9 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. f ) ` k ) = ( ( F o. f ) ` k ) )
100		eqidd 2423	. . . . . . . . 9 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( H o. f ) ` k ) = ( ( H o. f ) ` k ) )
101	95, 97, 89, 89, 98, 99, 100	ofval 6551	. . . . . . . 8 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( ( F o. f ) oF .+ ( H o. f ) ) ` k ) = ( ( ( F o. f ) ` k ) .+ ( ( H o. f ) ` k ) ) )
102	93, 101	eqtrd 2463	. . . . . . 7 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( ( F oF .+ H ) o. f ) ` k ) = ( ( ( F o. f ) ` k ) .+ ( ( H o. f ) ` k ) ) )
103	1	ad2antrr 730	. . . . . . . 8 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> G e. Mnd )
104		elfzouz 11925	. . . . . . . . . 10 |- ( n e. ( 1..^ ( # ` W ) ) -> n e. ( ZZ>= ` 1 ) )
105	104	adantl 467	. . . . . . . . 9 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> n e. ( ZZ>= ` 1 ) )
106		elfzouz2 11935	. . . . . . . . . . . . 13 |- ( n e. ( 1..^ ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` n ) )
107	106	adantl 467	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( # ` W ) e. ( ZZ>= ` n ) )
108		fzss2 11839	. . . . . . . . . . . 12 |- ( ( # ` W ) e. ( ZZ>= ` n ) -> ( 1 ... n ) C_ ( 1 ... ( # ` W ) ) )
109	107, 108	syl 17	. . . . . . . . . . 11 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( 1 ... n ) C_ ( 1 ... ( # ` W ) ) )
110	109	sselda 3464	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) /\ k e. ( 1 ... n ) ) -> k e. ( 1 ... ( # ` W ) ) )
111	78	adantlr 719	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. f ) ` k ) e. B )
112	110, 111	syldan 472	. . . . . . . . 9 |- ( ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) /\ k e. ( 1 ... n ) ) -> ( ( F o. f ) ` k ) e. B )
113	2, 6	mndcl 16533	. . . . . . . . . . 11 |- ( ( G e. Mnd /\ k e. B /\ x e. B ) -> ( k .+ x ) e. B )
114	113	3expb 1206	. . . . . . . . . 10 |- ( ( G e. Mnd /\ ( k e. B /\ x e. B ) ) -> ( k .+ x ) e. B )
115	103, 114	sylan 473	. . . . . . . . 9 |- ( ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) /\ ( k e. B /\ x e. B ) ) -> ( k .+ x ) e. B )
116	105, 112, 115	seqcl 12233	. . . . . . . 8 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( seq 1 ( .+ , ( F o. f ) ) ` n ) e. B )
117	82	adantlr 719	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( H o. f ) ` k ) e. B )
118	110, 117	syldan 472	. . . . . . . . 9 |- ( ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) /\ k e. ( 1 ... n ) ) -> ( ( H o. f ) ` k ) e. B )
119	105, 118, 115	seqcl 12233	. . . . . . . 8 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( seq 1 ( .+ , ( H o. f ) ) ` n ) e. B )
120		fzofzp1 12008	. . . . . . . . 9 |- ( n e. ( 1..^ ( # ` W ) ) -> ( n + 1 ) e. ( 1 ... ( # ` W ) ) )
121		ffvelrn 6032	. . . . . . . . 9 |- ( ( ( F o. f ) : ( 1 ... ( # ` W ) ) --> B /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. f ) ` ( n + 1 ) ) e. B )
122	77, 120, 121	syl2an 479	. . . . . . . 8 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( ( F o. f ) ` ( n + 1 ) ) e. B )
123		ffvelrn 6032	. . . . . . . . 9 |- ( ( ( H o. f ) : ( 1 ... ( # ` W ) ) --> B /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( ( H o. f ) ` ( n + 1 ) ) e. B )
124	81, 120, 123	syl2an 479	. . . . . . . 8 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( ( H o. f ) ` ( n + 1 ) ) e. B )
125		fvco3 5955	. . . . . . . . . . . 12 |- ( ( f : ( 1 ... ( # ` W ) ) --> A /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. f ) ` ( n + 1 ) ) = ( F ` ( f ` ( n + 1 ) ) ) )
126	75, 120, 125	syl2an 479	. . . . . . . . . . 11 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( ( F o. f ) ` ( n + 1 ) ) = ( F ` ( f ` ( n + 1 ) ) ) )
127		ffvelrn 6032	. . . . . . . . . . . . . 14 |- ( ( f : ( 1 ... ( # ` W ) ) --> A /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( f ` ( n + 1 ) ) e. A )
128	75, 120, 127	syl2an 479	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( f ` ( n + 1 ) ) e. A )
129		fzp1disj 11855	. . . . . . . . . . . . . . 15 |- ( ( 1 ... n ) i^i { ( n + 1 ) } ) = (/)
130		disjsn 4057	. . . . . . . . . . . . . . 15 |- ( ( ( 1 ... n ) i^i { ( n + 1 ) } ) = (/) <-> -. ( n + 1 ) e. ( 1 ... n ) )
131	129, 130	mpbi 211	. . . . . . . . . . . . . 14 |- -. ( n + 1 ) e. ( 1 ... n )
132	73	adantr 466	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> f : ( 1 ... ( # ` W ) ) -1-1-> A )
133	120	adantl 467	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( n + 1 ) e. ( 1 ... ( # ` W ) ) )
134		f1elima 6176	. . . . . . . . . . . . . . 15 |- ( ( f : ( 1 ... ( # ` W ) ) -1-1-> A /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) /\ ( 1 ... n ) C_ ( 1 ... ( # ` W ) ) ) -> ( ( f ` ( n + 1 ) ) e. ( f " ( 1 ... n ) ) <-> ( n + 1 ) e. ( 1 ... n ) ) )
135	132, 133, 109, 134	syl3anc 1264	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( ( f ` ( n + 1 ) ) e. ( f " ( 1 ... n ) ) <-> ( n + 1 ) e. ( 1 ... n ) ) )
136	131, 135	mtbiri 304	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> -. ( f ` ( n + 1 ) ) e. ( f " ( 1 ... n ) ) )
137	128, 136	eldifd 3447	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( f ` ( n + 1 ) ) e. ( A \ ( f " ( 1 ... n ) ) ) )
138		gsumzaddlem.4	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) )
139	138	expr 618	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x C_ A ) -> ( k e. ( A \ x ) -> ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) ) )
140	139	ralrimiv 2837	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x C_ A ) -> A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) )
141	140	ex 435	. . . . . . . . . . . . . . 15 |- ( ph -> ( x C_ A -> A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) ) )
142	141	alrimiv 1763	. . . . . . . . . . . . . 14 |- ( ph -> A. x ( x C_ A -> A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) ) )
143	142	ad2antrr 730	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> A. x ( x C_ A -> A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) ) )
144		imassrn 5195	. . . . . . . . . . . . . 14 |- ( f " ( 1 ... n ) ) C_ ran f
145	75	adantr 466	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> f : ( 1 ... ( # ` W ) ) --> A )
146		frn 5749	. . . . . . . . . . . . . . 15 |- ( f : ( 1 ... ( # ` W ) ) --> A -> ran f C_ A )
147	145, 146	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ran f C_ A )
148	144, 147	syl5ss 3475	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( f " ( 1 ... n ) ) C_ A )
149		vex 3084	. . . . . . . . . . . . . . 15 |- f e. _V
150		imaexg 6741	. . . . . . . . . . . . . . 15 |- ( f e. _V -> ( f " ( 1 ... n ) ) e. _V )
151	149, 150	ax-mp 5	. . . . . . . . . . . . . 14 |- ( f " ( 1 ... n ) ) e. _V
152		sseq1 3485	. . . . . . . . . . . . . . 15 |- ( x = ( f " ( 1 ... n ) ) -> ( x C_ A <-> ( f " ( 1 ... n ) ) C_ A ) )
153		difeq2 3577	. . . . . . . . . . . . . . . 16 |- ( x = ( f " ( 1 ... n ) ) -> ( A \ x ) = ( A \ ( f " ( 1 ... n ) ) ) )
154		reseq2 5116	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( f " ( 1 ... n ) ) -> ( H |` x ) = ( H |` ( f " ( 1 ... n ) ) ) )
155	154	oveq2d 6318	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( f " ( 1 ... n ) ) -> ( G gsumg ( H |` x ) ) = ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) )
156	155	sneqd 4008	. . . . . . . . . . . . . . . . . 18 |- ( x = ( f " ( 1 ... n ) ) -> { ( G gsumg ( H |` x ) ) } = { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } )
157	156	fveq2d 5882	. . . . . . . . . . . . . . . . 17 |- ( x = ( f " ( 1 ... n ) ) -> ( Z ` { ( G gsumg ( H |` x ) ) } ) = ( Z ` { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } ) )
158	157	eleq2d 2492	. . . . . . . . . . . . . . . 16 |- ( x = ( f " ( 1 ... n ) ) -> ( ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) <-> ( F ` k ) e. ( Z ` { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } ) ) )
159	153, 158	raleqbidv 3039	. . . . . . . . . . . . . . 15 |- ( x = ( f " ( 1 ... n ) ) -> ( A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) <-> A. k e. ( A \ ( f " ( 1 ... n ) ) ) ( F ` k ) e. ( Z ` { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } ) ) )
160	152, 159	imbi12d 321	. . . . . . . . . . . . . 14 |- ( x = ( f " ( 1 ... n ) ) -> ( ( x C_ A -> A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) ) <-> ( ( f " ( 1 ... n ) ) C_ A -> A. k e. ( A \ ( f " ( 1 ... n ) ) ) ( F ` k ) e. ( Z ` { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } ) ) ) )
161	151, 160	spcv 3172	. . . . . . . . . . . . 13 |- ( A. x ( x C_ A -> A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) ) -> ( ( f " ( 1 ... n ) ) C_ A -> A. k e. ( A \ ( f " ( 1 ... n ) ) ) ( F ` k ) e. ( Z ` { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } ) ) )
162	143, 148, 161	sylc 62	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> A. k e. ( A \ ( f " ( 1 ... n ) ) ) ( F ` k ) e. ( Z ` { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } ) )
163		fveq2 5878	. . . . . . . . . . . . . 14 |- ( k = ( f ` ( n + 1 ) ) -> ( F ` k ) = ( F ` ( f ` ( n + 1 ) ) ) )
164	163	eleq1d 2491	. . . . . . . . . . . . 13 |- ( k = ( f ` ( n + 1 ) ) -> ( ( F ` k ) e. ( Z ` { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } ) <-> ( F ` ( f ` ( n + 1 ) ) ) e. ( Z ` { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } ) ) )
165	164	rspcv 3178	. . . . . . . . . . . 12 |- ( ( f ` ( n + 1 ) ) e. ( A \ ( f " ( 1 ... n ) ) ) -> ( A. k e. ( A \ ( f " ( 1 ... n ) ) ) ( F ` k ) e. ( Z ` { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } ) -> ( F ` ( f ` ( n + 1 ) ) ) e. ( Z ` { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } ) ) )
166	137, 162, 165	sylc 62	. . . . . . . . . . 11 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( F ` ( f ` ( n + 1 ) ) ) e. ( Z ` { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } ) )
167	126, 166	eqeltrd 2510	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( ( F o. f ) ` ( n + 1 ) ) e. ( Z ` { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } ) )
168		gsumzadd.z	. . . . . . . . . . . . 13 |- Z = (Cntz ` G )
169	151	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( f " ( 1 ... n ) ) e. _V )
170	15	ad2antrr 730	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> H : A --> B )
171	170, 148	fssresd 5764	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( H |` ( f " ( 1 ... n ) ) ) : ( f " ( 1 ... n ) ) --> B )
172		gsumzaddlem.2	. . . . . . . . . . . . . . 15 |- ( ph -> ran H C_ ( Z ` ran H ) )
173	172	ad2antrr 730	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ran H C_ ( Z ` ran H ) )
174		resss 5144	. . . . . . . . . . . . . . 15 |- ( H |` ( f " ( 1 ... n ) ) ) C_ H
175		rnss 5079	. . . . . . . . . . . . . . 15 |- ( ( H |` ( f " ( 1 ... n ) ) ) C_ H -> ran ( H |` ( f " ( 1 ... n ) ) ) C_ ran H )
176	174, 175	ax-mp 5	. . . . . . . . . . . . . 14 |- ran ( H |` ( f " ( 1 ... n ) ) ) C_ ran H
177	168	cntzidss 16979	. . . . . . . . . . . . . 14 |- ( ( ran H C_ ( Z ` ran H ) /\ ran ( H |` ( f " ( 1 ... n ) ) ) C_ ran H ) -> ran ( H |` ( f " ( 1 ... n ) ) ) C_ ( Z ` ran ( H |` ( f " ( 1 ... n ) ) ) ) )
178	173, 176, 177	sylancl 666	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ran ( H |` ( f " ( 1 ... n ) ) ) C_ ( Z ` ran ( H |` ( f " ( 1 ... n ) ) ) ) )
179	105, 53	syl6eleqr 2521	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> n e. NN )
180		f1ores 5842	. . . . . . . . . . . . . . 15 |- ( ( f : ( 1 ... ( # ` W ) ) -1-1-> A /\ ( 1 ... n ) C_ ( 1 ... ( # ` W ) ) ) -> ( f |` ( 1 ... n ) ) : ( 1 ... n ) -1-1-onto-> ( f " ( 1 ... n ) ) )
181	132, 109, 180	syl2anc 665	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( f |` ( 1 ... n ) ) : ( 1 ... n ) -1-1-onto-> ( f " ( 1 ... n ) ) )
182		f1of1 5827	. . . . . . . . . . . . . 14 |- ( ( f |` ( 1 ... n ) ) : ( 1 ... n ) -1-1-onto-> ( f " ( 1 ... n ) ) -> ( f |` ( 1 ... n ) ) : ( 1 ... n ) -1-1-> ( f " ( 1 ... n ) ) )
183	181, 182	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( f |` ( 1 ... n ) ) : ( 1 ... n ) -1-1-> ( f " ( 1 ... n ) ) )
184		suppssdm 6935	. . . . . . . . . . . . . . 15 |- ( ( H |` ( f " ( 1 ... n ) ) ) supp .0. ) C_ dom ( H |` ( f " ( 1 ... n ) ) )
185		dmres 5141	. . . . . . . . . . . . . . . 16 |- dom ( H |` ( f " ( 1 ... n ) ) ) = ( ( f " ( 1 ... n ) ) i^i dom H )
186	185	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> dom ( H |` ( f " ( 1 ... n ) ) ) = ( ( f " ( 1 ... n ) ) i^i dom H ) )
187	184, 186	syl5sseq 3512	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( ( H |` ( f " ( 1 ... n ) ) ) supp .0. ) C_ ( ( f " ( 1 ... n ) ) i^i dom H ) )
188		inss1 3682	. . . . . . . . . . . . . . 15 |- ( ( f " ( 1 ... n ) ) i^i dom H ) C_ ( f " ( 1 ... n ) )
189		df-ima 4863	. . . . . . . . . . . . . . . 16 |- ( f " ( 1 ... n ) ) = ran ( f |` ( 1 ... n ) )
190	189	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( f " ( 1 ... n ) ) = ran ( f |` ( 1 ... n ) ) )
191	188, 190	syl5sseq 3512	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( ( f " ( 1 ... n ) ) i^i dom H ) C_ ran ( f |` ( 1 ... n ) ) )
192	187, 191	sstrd 3474	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( ( H |` ( f " ( 1 ... n ) ) ) supp .0. ) C_ ran ( f |` ( 1 ... n ) ) )
193		eqid 2422	. . . . . . . . . . . . 13 |- ( ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) supp .0. ) = ( ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) supp .0. )
194	2, 3, 6, 168, 103, 169, 171, 178, 179, 183, 192, 193	gsumval3 17529	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) = ( seq 1 ( .+ , ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) ) ` n ) )
195	189	eqimss2i 3519	. . . . . . . . . . . . . . . . . 18 |- ran ( f |` ( 1 ... n ) ) C_ ( f " ( 1 ... n ) )
196		cores 5354	. . . . . . . . . . . . . . . . . 18 |- ( ran ( f |` ( 1 ... n ) ) C_ ( f " ( 1 ... n ) ) -> ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) = ( H o. ( f |` ( 1 ... n ) ) ) )
197	195, 196	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) = ( H o. ( f |` ( 1 ... n ) ) )
198		resco 5355	. . . . . . . . . . . . . . . . 17 |- ( ( H o. f ) |` ( 1 ... n ) ) = ( H o. ( f |` ( 1 ... n ) ) )
199	197, 198	eqtr4i 2454	. . . . . . . . . . . . . . . 16 |- ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) = ( ( H o. f ) |` ( 1 ... n ) )
200	199	fveq1i 5879	. . . . . . . . . . . . . . 15 |- ( ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) ` k ) = ( ( ( H o. f ) |` ( 1 ... n ) ) ` k )
201		fvres 5892	. . . . . . . . . . . . . . 15 |- ( k e. ( 1 ... n ) -> ( ( ( H o. f ) |` ( 1 ... n ) ) ` k ) = ( ( H o. f ) ` k ) )
202	200, 201	syl5eq 2475	. . . . . . . . . . . . . 14 |- ( k e. ( 1 ... n ) -> ( ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) ` k ) = ( ( H o. f ) ` k ) )
203	202	adantl 467	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) /\ k e. ( 1 ... n ) ) -> ( ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) ` k ) = ( ( H o. f ) ` k ) )
204	105, 203	seqfveq 12237	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( seq 1 ( .+ , ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) ) ` n ) = ( seq 1 ( .+ , ( H o. f ) ) ` n ) )
205	194, 204	eqtr2d 2464	. . . . . . . . . . 11 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( seq 1 ( .+ , ( H o. f ) ) ` n ) = ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) )
206		fvex 5888	. . . . . . . . . . . 12 |- ( seq 1 ( .+ , ( H o. f ) ) ` n ) e. _V
207	206	elsnc 4020	. . . . . . . . . . 11 |- ( ( seq 1 ( .+ , ( H o. f ) ) ` n ) e. { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } <-> ( seq 1 ( .+ , ( H o. f ) ) ` n ) = ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) )
208	205, 207	sylibr 215	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( seq 1 ( .+ , ( H o. f ) ) ` n ) e. { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } )
209	6, 168	cntzi 16971	. . . . . . . . . 10 |- ( ( ( ( F o. f ) ` ( n + 1 ) ) e. ( Z ` { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } ) /\ ( seq 1 ( .+ , ( H o. f ) ) ` n ) e. { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } ) -> ( ( ( F o. f ) ` ( n + 1 ) ) .+ ( seq 1 ( .+ , ( H o. f ) ) ` n ) ) = ( ( seq 1 ( .+ , ( H o. f ) ) ` n ) .+ ( ( F o. f ) ` ( n + 1 ) ) ) )
210	167, 208, 209	syl2anc 665	. . . . . . . . 9 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( ( ( F o. f ) ` ( n + 1 ) ) .+ ( seq 1 ( .+ , ( H o. f ) ) ` n ) ) = ( ( seq 1 ( .+ , ( H o. f ) ) ` n ) .+ ( ( F o. f ) ` ( n + 1 ) ) ) )
211	210	eqcomd 2430	. . . . . . . 8 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( ( seq 1 ( .+ , ( H o. f ) ) ` n ) .+ ( ( F o. f ) ` ( n + 1 ) ) ) = ( ( ( F o. f ) ` ( n + 1 ) ) .+ ( seq 1 ( .+ , ( H o. f ) ) ` n ) ) )
212	2, 6, 103, 116, 119, 122, 124, 211	mnd4g 16541	. . . . . . 7 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( ( ( seq 1 ( .+ , ( F o. f ) ) ` n ) .+ ( seq 1 ( .+ , ( H o. f ) ) ` n ) ) .+ ( ( ( F o. f ) ` ( n + 1 ) ) .+ ( ( H o. f ) ` ( n + 1 ) ) ) ) = ( ( ( seq 1 ( .+ , ( F o. f ) ) ` n ) .+ ( ( F o. f ) ` ( n + 1 ) ) ) .+ ( ( seq 1 ( .+ , ( H o. f ) ) ` n ) .+ ( ( H o. f ) ` ( n + 1 ) ) ) ) )
213	51, 51, 54, 78, 82, 102, 212	seqcaopr3 12248	. . . . . 6 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( seq 1 ( .+ , ( ( F oF .+ H ) o. f ) ) ` ( # ` W ) ) = ( ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) .+ ( seq 1 ( .+ , ( H o. f ) ) ` ( # ` W ) ) ) )
214	50, 55, 79, 87, 87, 90	off 6557	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F oF .+ H ) : A --> B )
215		gsumzaddlem.3	. . . . . . . 8 |- ( ph -> ran ( F oF .+ H ) C_ ( Z ` ran ( F oF .+ H ) ) )
216	215	adantr 466	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ran ( F oF .+ H ) C_ ( Z ` ran ( F oF .+ H ) ) )
217	47, 114	sylan 473	. . . . . . . . 9 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ ( k e. B /\ x e. B ) ) -> ( k .+ x ) e. B )
218	217, 55, 79, 87, 87, 90	off 6557	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F oF .+ H ) : A --> B )
219		eldifi 3587	. . . . . . . . . 10 |- ( x e. ( A \ ran f ) -> x e. A )
220		eqidd 2423	. . . . . . . . . . 11 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
221		eqidd 2423	. . . . . . . . . . 11 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. A ) -> ( H ` x ) = ( H ` x ) )
222	84, 86, 87, 87, 90, 220, 221	ofval 6551	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. A ) -> ( ( F oF .+ H ) ` x ) = ( ( F ` x ) .+ ( H ` x ) ) )
223	219, 222	sylan2 476	. . . . . . . . 9 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( ( F oF .+ H ) ` x ) = ( ( F ` x ) .+ ( H ` x ) ) )
224	18	adantr 466	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F supp .0. ) C_ ( ( F u. H ) supp .0. ) )
225		f1ofo 5835	. . . . . . . . . . . . . . . 16 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> f : ( 1 ... ( # ` W ) ) -onto-> W )
226		forn 5810	. . . . . . . . . . . . . . . 16 |- ( f : ( 1 ... ( # ` W ) ) -onto-> W -> ran f = W )
227	225, 226	syl 17	. . . . . . . . . . . . . . 15 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ran f = W )
228	227, 19	syl6eq 2479	. . . . . . . . . . . . . 14 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ran f = ( ( F u. H ) supp .0. ) )
229	228	sseq2d 3492	. . . . . . . . . . . . 13 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ( ( F supp .0. ) C_ ran f <-> ( F supp .0. ) C_ ( ( F u. H ) supp .0. ) ) )
230	229	ad2antll 733	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( ( F supp .0. ) C_ ran f <-> ( F supp .0. ) C_ ( ( F u. H ) supp .0. ) ) )
231	224, 230	mpbird 235	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F supp .0. ) C_ ran f )
232	13	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> .0. e. _V )
233	55, 231, 87, 232	suppssr 6954	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( F ` x ) = .0. )
234	29	adantr 466	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H supp .0. ) C_ ( ( H u. F ) supp .0. ) )
235	234, 31	syl6sseqr 3511	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H supp .0. ) C_ ( ( F u. H ) supp .0. ) )
236	228	sseq2d 3492	. . . . . . . . . . . . 13 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ( ( H supp .0. ) C_ ran f <-> ( H supp .0. ) C_ ( ( F u. H ) supp .0. ) ) )
237	236	ad2antll 733	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( ( H supp .0. ) C_ ran f <-> ( H supp .0. ) C_ ( ( F u. H ) supp .0. ) ) )
238	235, 237	mpbird 235	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H supp .0. ) C_ ran f )
239	79, 238, 87, 232	suppssr 6954	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( H ` x ) = .0. )
240	233, 239	oveq12d 6320	. . . . . . . . 9 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( ( F ` x ) .+ ( H ` x ) ) = ( .0. .+ .0. ) )
241	8	ad2antrr 730	. . . . . . . . 9 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( .0. .+ .0. ) = .0. )
242	223, 240, 241	3eqtrd 2467	. . . . . . . 8 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( ( F oF .+ H ) ` x ) = .0. )
243	218, 242	suppss 6953	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( ( F oF .+ H ) supp .0. ) C_ ran f )
244		ovex 6330	. . . . . . . . 9 |- ( F oF .+ H ) e. _V
245	244, 149	coex 6756	. . . . . . . 8 |- ( ( F oF .+ H ) o. f ) e. _V
246		suppimacnv 6933	. . . . . . . . 9 |- ( ( ( ( F oF .+ H ) o. f ) e. _V /\ .0. e. _V ) -> ( ( ( F oF .+ H ) o. f ) supp .0. ) = ( `' ( ( F oF .+ H ) o. f ) " ( _V \ { .0. } ) ) )
247	246	eqcomd 2430	. . . . . . . 8 |- ( ( ( ( F oF .+ H ) o. f ) e. _V /\ .0. e. _V ) -> ( `' ( ( F oF .+ H ) o. f ) " ( _V \ { .0. } ) ) = ( ( ( F oF .+ H ) o. f ) supp .0. ) )
248	245, 13, 247	mp2an 676	. . . . . . 7 |- ( `' ( ( F oF .+ H ) o. f ) " ( _V \ { .0. } ) ) = ( ( ( F oF .+ H ) o. f ) supp .0. )
249	2, 3, 6, 168, 47, 87, 214, 216, 52, 73, 243, 248	gsumval3 17529	. . . . . 6 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( G gsumg ( F oF .+ H ) ) = ( seq 1 ( .+ , ( ( F oF .+ H ) o. f ) ) ` ( # ` W ) ) )
250		gsumzaddlem.1	. . . . . . . . 9 |- ( ph -> ran F C_ ( Z ` ran F ) )
251	250	adantr 466	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ran F C_ ( Z ` ran F ) )
252		eqid 2422	. . . . . . . 8 |- ( ( F o. f ) supp .0. ) = ( ( F o. f ) supp .0. )
253	2, 3, 6, 168, 47, 87, 55, 251, 52, 73, 231, 252	gsumval3 17529	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( G gsumg F ) = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) )
254	172	adantr 466	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ran H C_ ( Z ` ran H ) )
255		eqid 2422	. . . . . . . 8 |- ( ( H o. f ) supp .0. ) = ( ( H o. f ) supp .0. )
256	2, 3, 6, 168, 47, 87, 79, 254, 52, 73, 238, 255	gsumval3 17529	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( G gsumg H ) = ( seq 1 ( .+ , ( H o. f ) ) ` ( # ` W ) ) )
257	253, 256	oveq12d 6320	. . . . . 6 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( ( G gsumg F ) .+ ( G gsumg H ) ) = ( ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) .+ ( seq 1 ( .+ , ( H o. f ) ) ` ( # ` W ) ) ) )
258	213, 249, 257	3eqtr4d 2473	. . . . 5 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )
259	258	expr 618	. . . 4 |- ( ( ph /\ ( # ` W ) e. NN ) -> ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) ) )
260	259	exlimdv 1768	. . 3 |- ( ( ph /\ ( # ` W ) e. NN ) -> ( E. f f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) ) )
261	260	expimpd 606	. 2 |- ( ph -> ( ( ( # ` W ) e. NN /\ E. f f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) ) )
262		gsumzadd.fn	. . . . 5 |- ( ph -> F finSupp .0. )
263		gsumzadd.hn	. . . . 5 |- ( ph -> H finSupp .0. )
264	262, 263	fsuppun 7905	. . . 4 |- ( ph -> ( ( F u. H ) supp .0. ) e. Fin )
265	19, 264	syl5eqel 2514	. . 3 |- ( ph -> W e. Fin )
266		fz1f1o 13764	. . 3 |- ( W e. Fin -> ( W = (/) \/ ( ( # ` W ) e. NN /\ E. f f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) )
267	265, 266	syl 17	. 2 |- ( ph -> ( W = (/) \/ ( ( # ` W ) e. NN /\ E. f f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) )
268	46, 261, 267	mpjaod 382	1 |- ( ph -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   \/ wo 369   /\ wa 370   A.wal 1435   = wceq 1437   E.wex 1659   e. wcel 1868   A.wral 2775   _Vcvv 3081   \ cdif 3433   u. cun 3434   i^i cin 3435   C_ wss 3436   (/)c0 3761   {csn 3996   class class class wbr 4420   |-> cmpt 4479   `'ccnv 4849   dom cdm 4850   ran crn 4851   |` cres 4852   "cima 4853   o. ccom 4854   Fn wfn 5593   -->wf 5594   -1-1->wf1 5595   -onto->wfo 5596   -1-1-onto->wf1o 5597   ` cfv 5598  (class class class)co 6302   oFcof 6540   supp csupp 6922   Fincfn 7574   finSupp cfsupp 7886   1c1 9541   + caddc 9543   NNcn 10610   ZZ>=cuz 11160   ...cfz 11785  ..^cfzo 11916   seqcseq 12213   #chash 12515   Basecbs 15109   +g cplusg 15178   0gc0g 15326   gsum_g cgsu 15327   Mndcmnd 16523  Cntzccntz 16957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594  ax-cnex 9596  ax-resscn 9597  ax-1cn 9598  ax-icn 9599  ax-addcl 9600  ax-addrcl 9601  ax-mulcl 9602  ax-mulrcl 9603  ax-mulcom 9604  ax-addass 9605  ax-mulass 9606  ax-distr 9607  ax-i2m1 9608  ax-1ne0 9609  ax-1rid 9610  ax-rnegex 9611  ax-rrecex 9612  ax-cnre 9613  ax-pre-lttri 9614  ax-pre-lttrn 9615  ax-pre-ltadd 9616  ax-pre-mulgt0 9617

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-int 4253  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4761  df-id 4765  df-po 4771  df-so 4772  df-fr 4809  df-se 4810  df-we 4811  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-pred 5396  df-ord 5442  df-on 5443  df-lim 5444  df-suc 5445  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-isom 5607  df-riota 6264  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-of 6542  df-om 6704  df-1st 6804  df-2nd 6805  df-supp 6923  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-1o 7187  df-oadd 7191  df-er 7368  df-en 7575  df-dom 7576  df-sdom 7577  df-fin 7578  df-fsupp 7887  df-oi 8028  df-card 8375  df-pnf 9678  df-mnf 9679  df-xr 9680  df-ltxr 9681  df-le 9682  df-sub 9863  df-neg 9864  df-nn 10611  df-n0 10871  df-z 10939  df-uz 11161  df-fz 11786  df-fzo 11917  df-seq 12214  df-hash 12516  df-0g 15328  df-gsum 15329  df-mgm 16476  df-sgrp 16515  df-mnd 16525  df-cntz 16959

This theorem is referenced by:  gsumzadd  17543  dprdfadd  17641