Theorem gsumzaddlem 17547

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 16547	. . . . . . 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 16550	. . . . . 6 |- ( ( G e. Mnd /\ .0. e. B ) -> ( .0. .+ .0. ) = .0. )
8	1, 5, 7	syl2anc 666	. . . . 5 |- ( ph -> ( .0. .+ .0. ) = .0. )
9	8	adantr 467	. . . 4 |- ( ( ph /\ W = (/) ) -> ( .0. .+ .0. ) = .0. )
10		gsumzaddlem.f	. . . . . . . 8 |- ( ph -> F : A --> B )
11		gsumzadd.a	. . . . . . . 8 |- ( ph -> A e. V )
12		fvex 5873	. . . . . . . . . 10 |- ( 0g ` G ) e. _V
13	3, 12	eqeltri 2524	. . . . . . . . 9 |- .0. e. _V
14	13	a1i 11	. . . . . . . 8 |- ( ph -> .0. e. _V )
15		gsumzaddlem.h	. . . . . . . . . . 11 |- ( ph -> H : A --> B )
16		fex 6136	. . . . . . . . . . 11 |- ( ( H : A --> B /\ A e. V ) -> H e. _V )
17	15, 11, 16	syl2anc 666	. . . . . . . . . 10 |- ( ph -> H e. _V )
18	17	suppun 6932	. . . . . . . . 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 3478	. . . . . . . 8 |- ( ph -> ( F supp .0. ) C_ W )
21	10, 11, 14, 20	gsumcllem 17535	. . . . . . 7 |- ( ( ph /\ W = (/) ) -> F = ( x e. A |-> .0. ) )
22	21	oveq2d 6304	. . . . . 6 |- ( ( ph /\ W = (/) ) -> ( G gsumg F ) = ( G gsumg ( x e. A |-> .0. ) ) )
23	3	gsumz 16614	. . . . . . . 8 |- ( ( G e. Mnd /\ A e. V ) -> ( G gsumg ( x e. A |-> .0. ) ) = .0. )
24	1, 11, 23	syl2anc 666	. . . . . . 7 |- ( ph -> ( G gsumg ( x e. A |-> .0. ) ) = .0. )
25	24	adantr 467	. . . . . 6 |- ( ( ph /\ W = (/) ) -> ( G gsumg ( x e. A |-> .0. ) ) = .0. )
26	22, 25	eqtrd 2484	. . . . 5 |- ( ( ph /\ W = (/) ) -> ( G gsumg F ) = .0. )
27		fex 6136	. . . . . . . . . . . 12 |- ( ( F : A --> B /\ A e. V ) -> F e. _V )
28	10, 11, 27	syl2anc 666	. . . . . . . . . . 11 |- ( ph -> F e. _V )
29	28	suppun 6932	. . . . . . . . . 10 |- ( ph -> ( H supp .0. ) C_ ( ( H u. F ) supp .0. ) )
30		uncom 3577	. . . . . . . . . . 11 |- ( F u. H ) = ( H u. F )
31	30	oveq1i 6298	. . . . . . . . . 10 |- ( ( F u. H ) supp .0. ) = ( ( H u. F ) supp .0. )
32	29, 31	syl6sseqr 3478	. . . . . . . . 9 |- ( ph -> ( H supp .0. ) C_ ( ( F u. H ) supp .0. ) )
33	32, 19	syl6sseqr 3478	. . . . . . . 8 |- ( ph -> ( H supp .0. ) C_ W )
34	15, 11, 14, 33	gsumcllem 17535	. . . . . . 7 |- ( ( ph /\ W = (/) ) -> H = ( x e. A |-> .0. ) )
35	34	oveq2d 6304	. . . . . 6 |- ( ( ph /\ W = (/) ) -> ( G gsumg H ) = ( G gsumg ( x e. A |-> .0. ) ) )
36	35, 25	eqtrd 2484	. . . . 5 |- ( ( ph /\ W = (/) ) -> ( G gsumg H ) = .0. )
37	26, 36	oveq12d 6306	. . . 4 |- ( ( ph /\ W = (/) ) -> ( ( G gsumg F ) .+ ( G gsumg H ) ) = ( .0. .+ .0. ) )
38	11	adantr 467	. . . . . . . 8 |- ( ( ph /\ W = (/) ) -> A e. V )
39	5	ad2antrr 731	. . . . . . . 8 |- ( ( ( ph /\ W = (/) ) /\ x e. A ) -> .0. e. B )
40	38, 39, 39, 21, 34	offval2 6545	. . . . . . 7 |- ( ( ph /\ W = (/) ) -> ( F oF .+ H ) = ( x e. A |-> ( .0. .+ .0. ) ) )
41	9	mpteq2dv 4489	. . . . . . 7 |- ( ( ph /\ W = (/) ) -> ( x e. A |-> ( .0. .+ .0. ) ) = ( x e. A |-> .0. ) )
42	40, 41	eqtrd 2484	. . . . . 6 |- ( ( ph /\ W = (/) ) -> ( F oF .+ H ) = ( x e. A |-> .0. ) )
43	42	oveq2d 6304	. . . . 5 |- ( ( ph /\ W = (/) ) -> ( G gsumg ( F oF .+ H ) ) = ( G gsumg ( x e. A |-> .0. ) ) )
44	43, 25	eqtrd 2484	. . . 4 |- ( ( ph /\ W = (/) ) -> ( G gsumg ( F oF .+ H ) ) = .0. )
45	9, 37, 44	3eqtr4rd 2495	. . 3 |- ( ( ph /\ W = (/) ) -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )
46	45	ex 436	. 2 |- ( ph -> ( W = (/) -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) ) )
47	1	adantr 467	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> G e. Mnd )
48	2, 6	mndcl 16538	. . . . . . . . . 10 |- ( ( G e. Mnd /\ z e. B /\ w e. B ) -> ( z .+ w ) e. B )
49	48	3expb 1208	. . . . . . . . 9 |- ( ( G e. Mnd /\ ( z e. B /\ w e. B ) ) -> ( z .+ w ) e. B )
50	47, 49	sylan 474	. . . . . . . 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 6458	. . . . . . 7 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
52		simprl 763	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( # ` W ) e. NN )
53		nnuz 11191	. . . . . . . 8 |- NN = ( ZZ>= ` 1 )
54	52, 53	syl6eleq 2538	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( # ` W ) e. ( ZZ>= ` 1 ) )
55	10	adantr 467	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> F : A --> B )
56		f1of1 5811	. . . . . . . . . . . 12 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> f : ( 1 ... ( # ` W ) ) -1-1-> W )
57	56	ad2antll 734	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> f : ( 1 ... ( # ` W ) ) -1-1-> W )
58		suppssdm 6924	. . . . . . . . . . . . . 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 5040	. . . . . . . . . . . . . 14 |- dom ( F u. H ) = ( dom F u. dom H )
62		fdm 5731	. . . . . . . . . . . . . . . . 17 |- ( F : A --> B -> dom F = A )
63	10, 62	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> dom F = A )
64		fdm 5731	. . . . . . . . . . . . . . . . 17 |- ( H : A --> B -> dom H = A )
65	15, 64	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> dom H = A )
66	63, 65	uneq12d 3588	. . . . . . . . . . . . . . 15 |- ( ph -> ( dom F u. dom H ) = ( A u. A ) )
67		unidm 3576	. . . . . . . . . . . . . . 15 |- ( A u. A ) = A
68	66, 67	syl6eq 2500	. . . . . . . . . . . . . 14 |- ( ph -> ( dom F u. dom H ) = A )
69	61, 68	syl5req 2497	. . . . . . . . . . . . 13 |- ( ph -> A = dom ( F u. H ) )
70	59, 60, 69	3sstr4d 3474	. . . . . . . . . . . 12 |- ( ph -> W C_ A )
71	70	adantr 467	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> W C_ A )
72		f1ss 5782	. . . . . . . . . . 11 |- ( ( f : ( 1 ... ( # ` W ) ) -1-1-> W /\ W C_ A ) -> f : ( 1 ... ( # ` W ) ) -1-1-> A )
73	57, 71, 72	syl2anc 666	. . . . . . . . . 10 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> f : ( 1 ... ( # ` W ) ) -1-1-> A )
74		f1f 5777	. . . . . . . . . 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 5737	. . . . . . . . 9 |- ( ( F : A --> B /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( F o. f ) : ( 1 ... ( # ` W ) ) --> B )
77	55, 75, 76	syl2anc 666	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F o. f ) : ( 1 ... ( # ` W ) ) --> B )
78	77	ffvelrnda 6020	. . . . . . 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 467	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> H : A --> B )
80		fco 5737	. . . . . . . . 9 |- ( ( H : A --> B /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( H o. f ) : ( 1 ... ( # ` W ) ) --> B )
81	79, 75, 80	syl2anc 666	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H o. f ) : ( 1 ... ( # ` W ) ) --> B )
82	81	ffvelrnda 6020	. . . . . . 7 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( H o. f ) ` k ) e. B )
83		ffn 5726	. . . . . . . . . . . 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 5726	. . . . . . . . . . . 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 467	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> A e. V )
88		ovex 6316	. . . . . . . . . . . 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 3640	. . . . . . . . . . 11 |- ( A i^i A ) = A
91	84, 86, 75, 87, 87, 89, 90	ofco 6548	. . . . . . . . . 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 5865	. . . . . . . . 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 467	. . . . . . . 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 5746	. . . . . . . . . 10 |- ( ( F Fn A /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( F o. f ) Fn ( 1 ... ( # ` W ) ) )
95	84, 75, 94	syl2anc 666	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F o. f ) Fn ( 1 ... ( # ` W ) ) )
96		fnfco 5746	. . . . . . . . . 10 |- ( ( H Fn A /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( H o. f ) Fn ( 1 ... ( # ` W ) ) )
97	86, 75, 96	syl2anc 666	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H o. f ) Fn ( 1 ... ( # ` W ) ) )
98		inidm 3640	. . . . . . . . 9 |- ( ( 1 ... ( # ` W ) ) i^i ( 1 ... ( # ` W ) ) ) = ( 1 ... ( # ` W ) )
99		eqidd 2451	. . . . . . . . 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 2451	. . . . . . . . 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 6537	. . . . . . . 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 2484	. . . . . . 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 731	. . . . . . . 8 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> G e. Mnd )
104		elfzouz 11921	. . . . . . . . . 10 |- ( n e. ( 1..^ ( # ` W ) ) -> n e. ( ZZ>= ` 1 ) )
105	104	adantl 468	. . . . . . . . 9 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> n e. ( ZZ>= ` 1 ) )
106		elfzouz2 11931	. . . . . . . . . . . . 13 |- ( n e. ( 1..^ ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` n ) )
107	106	adantl 468	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( # ` W ) e. ( ZZ>= ` n ) )
108		fzss2 11835	. . . . . . . . . . . 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 3431	. . . . . . . . . 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 720	. . . . . . . . . 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 473	. . . . . . . . 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 16538	. . . . . . . . . . 11 |- ( ( G e. Mnd /\ k e. B /\ x e. B ) -> ( k .+ x ) e. B )
114	113	3expb 1208	. . . . . . . . . 10 |- ( ( G e. Mnd /\ ( k e. B /\ x e. B ) ) -> ( k .+ x ) e. B )
115	103, 114	sylan 474	. . . . . . . . 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 12230	. . . . . . . 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 720	. . . . . . . . . 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 473	. . . . . . . . 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 12230	. . . . . . . 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 12005	. . . . . . . . 9 |- ( n e. ( 1..^ ( # ` W ) ) -> ( n + 1 ) e. ( 1 ... ( # ` W ) ) )
121		ffvelrn 6018	. . . . . . . . 9 |- ( ( ( F o. f ) : ( 1 ... ( # ` W ) ) --> B /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. f ) ` ( n + 1 ) ) e. B )
122	77, 120, 121	syl2an 480	. . . . . . . 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 6018	. . . . . . . . 9 |- ( ( ( H o. f ) : ( 1 ... ( # ` W ) ) --> B /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( ( H o. f ) ` ( n + 1 ) ) e. B )
124	81, 120, 123	syl2an 480	. . . . . . . 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 5940	. . . . . . . . . . . 12 |- ( ( f : ( 1 ... ( # ` W ) ) --> A /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. f ) ` ( n + 1 ) ) = ( F ` ( f ` ( n + 1 ) ) ) )
126	75, 120, 125	syl2an 480	. . . . . . . . . . 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 6018	. . . . . . . . . . . . . 14 |- ( ( f : ( 1 ... ( # ` W ) ) --> A /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( f ` ( n + 1 ) ) e. A )
128	75, 120, 127	syl2an 480	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( f ` ( n + 1 ) ) e. A )
129		fzp1disj 11851	. . . . . . . . . . . . . . 15 |- ( ( 1 ... n ) i^i { ( n + 1 ) } ) = (/)
130		disjsn 4031	. . . . . . . . . . . . . . 15 |- ( ( ( 1 ... n ) i^i { ( n + 1 ) } ) = (/) <-> -. ( n + 1 ) e. ( 1 ... n ) )
131	129, 130	mpbi 212	. . . . . . . . . . . . . 14 |- -. ( n + 1 ) e. ( 1 ... n )
132	73	adantr 467	. . . . . . . . . . . . . . 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 468	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( n + 1 ) e. ( 1 ... ( # ` W ) ) )
134		f1elima 6162	. . . . . . . . . . . . . . 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 1267	. . . . . . . . . . . . . 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 305	. . . . . . . . . . . . 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 3414	. . . . . . . . . . . 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 619	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x C_ A ) -> ( k e. ( A \ x ) -> ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) ) )
140	139	ralrimiv 2799	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x C_ A ) -> A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) )
141	140	ex 436	. . . . . . . . . . . . . . 15 |- ( ph -> ( x C_ A -> A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) ) )
142	141	alrimiv 1772	. . . . . . . . . . . . . 14 |- ( ph -> A. x ( x C_ A -> A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) ) )
143	142	ad2antrr 731	. . . . . . . . . . . . 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 5178	. . . . . . . . . . . . . 14 |- ( f " ( 1 ... n ) ) C_ ran f
145	75	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> f : ( 1 ... ( # ` W ) ) --> A )
146		frn 5733	. . . . . . . . . . . . . . 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 3442	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( f " ( 1 ... n ) ) C_ A )
149		vex 3047	. . . . . . . . . . . . . . 15 |- f e. _V
150		imaexg 6727	. . . . . . . . . . . . . . 15 |- ( f e. _V -> ( f " ( 1 ... n ) ) e. _V )
151	149, 150	ax-mp 5	. . . . . . . . . . . . . 14 |- ( f " ( 1 ... n ) ) e. _V
152		sseq1 3452	. . . . . . . . . . . . . . 15 |- ( x = ( f " ( 1 ... n ) ) -> ( x C_ A <-> ( f " ( 1 ... n ) ) C_ A ) )
153		difeq2 3544	. . . . . . . . . . . . . . . 16 |- ( x = ( f " ( 1 ... n ) ) -> ( A \ x ) = ( A \ ( f " ( 1 ... n ) ) ) )
154		reseq2 5099	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( f " ( 1 ... n ) ) -> ( H |` x ) = ( H |` ( f " ( 1 ... n ) ) ) )
155	154	oveq2d 6304	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( f " ( 1 ... n ) ) -> ( G gsumg ( H |` x ) ) = ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) )
156	155	sneqd 3979	. . . . . . . . . . . . . . . . . 18 |- ( x = ( f " ( 1 ... n ) ) -> { ( G gsumg ( H |` x ) ) } = { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } )
157	156	fveq2d 5867	. . . . . . . . . . . . . . . . 17 |- ( x = ( f " ( 1 ... n ) ) -> ( Z ` { ( G gsumg ( H |` x ) ) } ) = ( Z ` { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } ) )
158	157	eleq2d 2513	. . . . . . . . . . . . . . . 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 3000	. . . . . . . . . . . . . . 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 322	. . . . . . . . . . . . . 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 3139	. . . . . . . . . . . . 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 5863	. . . . . . . . . . . . . 14 |- ( k = ( f ` ( n + 1 ) ) -> ( F ` k ) = ( F ` ( f ` ( n + 1 ) ) ) )
164	163	eleq1d 2512	. . . . . . . . . . . . 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 3145	. . . . . . . . . . . 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 2528	. . . . . . . . . 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 731	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> H : A --> B )
171	170, 148	fssresd 5748	. . . . . . . . . . . . 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 731	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ran H C_ ( Z ` ran H ) )
174		resss 5127	. . . . . . . . . . . . . . 15 |- ( H |` ( f " ( 1 ... n ) ) ) C_ H
175		rnss 5062	. . . . . . . . . . . . . . 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 16984	. . . . . . . . . . . . . 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 667	. . . . . . . . . . . . 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 2539	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> n e. NN )
180		f1ores 5826	. . . . . . . . . . . . . . 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 666	. . . . . . . . . . . . . 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 5811	. . . . . . . . . . . . . 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 6924	. . . . . . . . . . . . . . 15 |- ( ( H |` ( f " ( 1 ... n ) ) ) supp .0. ) C_ dom ( H |` ( f " ( 1 ... n ) ) )
185		dmres 5124	. . . . . . . . . . . . . . . 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 3479	. . . . . . . . . . . . . 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 3651	. . . . . . . . . . . . . . 15 |- ( ( f " ( 1 ... n ) ) i^i dom H ) C_ ( f " ( 1 ... n ) )
189		df-ima 4846	. . . . . . . . . . . . . . . 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 3479	. . . . . . . . . . . . . 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 3441	. . . . . . . . . . . . 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 2450	. . . . . . . . . . . . 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 17534	. . . . . . . . . . . 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 3486	. . . . . . . . . . . . . . . . . 18 |- ran ( f |` ( 1 ... n ) ) C_ ( f " ( 1 ... n ) )
196		cores 5337	. . . . . . . . . . . . . . . . . 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 5338	. . . . . . . . . . . . . . . . 17 |- ( ( H o. f ) |` ( 1 ... n ) ) = ( H o. ( f |` ( 1 ... n ) ) )
199	197, 198	eqtr4i 2475	. . . . . . . . . . . . . . . 16 |- ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) = ( ( H o. f ) |` ( 1 ... n ) )
200	199	fveq1i 5864	. . . . . . . . . . . . . . 15 |- ( ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) ` k ) = ( ( ( H o. f ) |` ( 1 ... n ) ) ` k )
201		fvres 5877	. . . . . . . . . . . . . . 15 |- ( k e. ( 1 ... n ) -> ( ( ( H o. f ) |` ( 1 ... n ) ) ` k ) = ( ( H o. f ) ` k ) )
202	200, 201	syl5eq 2496	. . . . . . . . . . . . . 14 |- ( k e. ( 1 ... n ) -> ( ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) ` k ) = ( ( H o. f ) ` k ) )
203	202	adantl 468	. . . . . . . . . . . . 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 12234	. . . . . . . . . . . 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 2485	. . . . . . . . . . 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 5873	. . . . . . . . . . . 12 |- ( seq 1 ( .+ , ( H o. f ) ) ` n ) e. _V
207	206	elsnc 3991	. . . . . . . . . . 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 216	. . . . . . . . . 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 16976	. . . . . . . . . 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 666	. . . . . . . . 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 2456	. . . . . . . 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 16546	. . . . . . 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 12245	. . . . . 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 6543	. . . . . . 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 467	. . . . . . 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 474	. . . . . . . . 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 6543	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F oF .+ H ) : A --> B )
219		eldifi 3554	. . . . . . . . . 10 |- ( x e. ( A \ ran f ) -> x e. A )
220		eqidd 2451	. . . . . . . . . . 11 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
221		eqidd 2451	. . . . . . . . . . 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 6537	. . . . . . . . . 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 477	. . . . . . . . 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 467	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F supp .0. ) C_ ( ( F u. H ) supp .0. ) )
225		f1ofo 5819	. . . . . . . . . . . . . . . 16 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> f : ( 1 ... ( # ` W ) ) -onto-> W )
226		forn 5794	. . . . . . . . . . . . . . . 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 2500	. . . . . . . . . . . . . 14 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ran f = ( ( F u. H ) supp .0. ) )
229	228	sseq2d 3459	. . . . . . . . . . . . 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 734	. . . . . . . . . . . 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 236	. . . . . . . . . . 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 6943	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( F ` x ) = .0. )
234	29	adantr 467	. . . . . . . . . . . . 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 3478	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H supp .0. ) C_ ( ( F u. H ) supp .0. ) )
236	228	sseq2d 3459	. . . . . . . . . . . . 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 734	. . . . . . . . . . . 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 236	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H supp .0. ) C_ ran f )
239	79, 238, 87, 232	suppssr 6943	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( H ` x ) = .0. )
240	233, 239	oveq12d 6306	. . . . . . . . 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 731	. . . . . . . . 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 2488	. . . . . . . 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 6942	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( ( F oF .+ H ) supp .0. ) C_ ran f )
244		ovex 6316	. . . . . . . . 9 |- ( F oF .+ H ) e. _V
245	244, 149	coex 6742	. . . . . . . 8 |- ( ( F oF .+ H ) o. f ) e. _V
246		suppimacnv 6922	. . . . . . . . 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 2456	. . . . . . . 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 677	. . . . . . 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 17534	. . . . . 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 467	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ran F C_ ( Z ` ran F ) )
252		eqid 2450	. . . . . . . 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 17534	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( G gsumg F ) = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) )
254	172	adantr 467	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ran H C_ ( Z ` ran H ) )
255		eqid 2450	. . . . . . . 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 17534	. . . . . . 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 6306	. . . . . 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 2494	. . . . 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 619	. . . 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 1778	. . 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 607	. 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 7899	. . . 4 |- ( ph -> ( ( F u. H ) supp .0. ) e. Fin )
265	19, 264	syl5eqel 2532	. . 3 |- ( ph -> W e. Fin )
266		fz1f1o 13769	. . 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 383	1 |- ( ph -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   \/ wo 370   /\ wa 371   A.wal 1441   = wceq 1443   E.wex 1662   e. wcel 1886   A.wral 2736   _Vcvv 3044   \ cdif 3400   u. cun 3401   i^i cin 3402   C_ wss 3403   (/)c0 3730   {csn 3967   class class class wbr 4401   |-> cmpt 4460   `'ccnv 4832   dom cdm 4833   ran crn 4834   |` cres 4835   "cima 4836   o. ccom 4837   Fn wfn 5576   -->wf 5577   -1-1->wf1 5578   -onto->wfo 5579   -1-1-onto->wf1o 5580   ` cfv 5581  (class class class)co 6288   oFcof 6526   supp csupp 6911   Fincfn 7566   finSupp cfsupp 7880   1c1 9537   + caddc 9539   NNcn 10606   ZZ>=cuz 11156   ...cfz 11781  ..^cfzo 11912   seqcseq 12210   #chash 12512   Basecbs 15114   +g cplusg 15183   0gc0g 15331   gsum_g cgsu 15332   Mndcmnd 16528  Cntzccntz 16962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-cnex 9592  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-int 4234  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-se 4793  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-isom 5590  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-of 6528  df-om 6690  df-1st 6790  df-2nd 6791  df-supp 6912  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-1o 7179  df-oadd 7183  df-er 7360  df-en 7567  df-dom 7568  df-sdom 7569  df-fin 7570  df-fsupp 7881  df-oi 8022  df-card 8370  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-sub 9859  df-neg 9860  df-nn 10607  df-n0 10867  df-z 10935  df-uz 11157  df-fz 11782  df-fzo 11913  df-seq 12211  df-hash 12513  df-0g 15333  df-gsum 15334  df-mgm 16481  df-sgrp 16520  df-mnd 16530  df-cntz 16964

This theorem is referenced by:  gsumzadd  17548  dprdfadd  17646