Theorem gsumzaddlem 18321

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 17308	. . . . . . 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 17311	. . . . . 6 |- ( ( G e. Mnd /\ .0. e. B ) -> ( .0. .+ .0. ) = .0. )
8	1, 5, 7	syl2anc 693	. . . . 5 |- ( ph -> ( .0. .+ .0. ) = .0. )
9	8	adantr 481	. . . 4 |- ( ( ph /\ W = (/) ) -> ( .0. .+ .0. ) = .0. )
10		gsumzaddlem.f	. . . . . . . 8 |- ( ph -> F : A --> B )
11		gsumzadd.a	. . . . . . . 8 |- ( ph -> A e. V )
12		fvex 6201	. . . . . . . . . 10 |- ( 0g ` G ) e. _V
13	3, 12	eqeltri 2697	. . . . . . . . 9 |- .0. e. _V
14	13	a1i 11	. . . . . . . 8 |- ( ph -> .0. e. _V )
15		gsumzaddlem.h	. . . . . . . . . . 11 |- ( ph -> H : A --> B )
16		fex 6490	. . . . . . . . . . 11 |- ( ( H : A --> B /\ A e. V ) -> H e. _V )
17	15, 11, 16	syl2anc 693	. . . . . . . . . 10 |- ( ph -> H e. _V )
18	17	suppun 7315	. . . . . . . . 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 3652	. . . . . . . 8 |- ( ph -> ( F supp .0. ) C_ W )
21	10, 11, 14, 20	gsumcllem 18309	. . . . . . 7 |- ( ( ph /\ W = (/) ) -> F = ( x e. A |-> .0. ) )
22	21	oveq2d 6666	. . . . . 6 |- ( ( ph /\ W = (/) ) -> ( G gsumg F ) = ( G gsumg ( x e. A |-> .0. ) ) )
23	3	gsumz 17374	. . . . . . . 8 |- ( ( G e. Mnd /\ A e. V ) -> ( G gsumg ( x e. A |-> .0. ) ) = .0. )
24	1, 11, 23	syl2anc 693	. . . . . . 7 |- ( ph -> ( G gsumg ( x e. A |-> .0. ) ) = .0. )
25	24	adantr 481	. . . . . 6 |- ( ( ph /\ W = (/) ) -> ( G gsumg ( x e. A |-> .0. ) ) = .0. )
26	22, 25	eqtrd 2656	. . . . 5 |- ( ( ph /\ W = (/) ) -> ( G gsumg F ) = .0. )
27		fex 6490	. . . . . . . . . . . 12 |- ( ( F : A --> B /\ A e. V ) -> F e. _V )
28	10, 11, 27	syl2anc 693	. . . . . . . . . . 11 |- ( ph -> F e. _V )
29	28	suppun 7315	. . . . . . . . . 10 |- ( ph -> ( H supp .0. ) C_ ( ( H u. F ) supp .0. ) )
30		uncom 3757	. . . . . . . . . . 11 |- ( F u. H ) = ( H u. F )
31	30	oveq1i 6660	. . . . . . . . . 10 |- ( ( F u. H ) supp .0. ) = ( ( H u. F ) supp .0. )
32	29, 31	syl6sseqr 3652	. . . . . . . . 9 |- ( ph -> ( H supp .0. ) C_ ( ( F u. H ) supp .0. ) )
33	32, 19	syl6sseqr 3652	. . . . . . . 8 |- ( ph -> ( H supp .0. ) C_ W )
34	15, 11, 14, 33	gsumcllem 18309	. . . . . . 7 |- ( ( ph /\ W = (/) ) -> H = ( x e. A |-> .0. ) )
35	34	oveq2d 6666	. . . . . 6 |- ( ( ph /\ W = (/) ) -> ( G gsumg H ) = ( G gsumg ( x e. A |-> .0. ) ) )
36	35, 25	eqtrd 2656	. . . . 5 |- ( ( ph /\ W = (/) ) -> ( G gsumg H ) = .0. )
37	26, 36	oveq12d 6668	. . . 4 |- ( ( ph /\ W = (/) ) -> ( ( G gsumg F ) .+ ( G gsumg H ) ) = ( .0. .+ .0. ) )
38	11	adantr 481	. . . . . . . 8 |- ( ( ph /\ W = (/) ) -> A e. V )
39	5	ad2antrr 762	. . . . . . . 8 |- ( ( ( ph /\ W = (/) ) /\ x e. A ) -> .0. e. B )
40	38, 39, 39, 21, 34	offval2 6914	. . . . . . 7 |- ( ( ph /\ W = (/) ) -> ( F oF .+ H ) = ( x e. A |-> ( .0. .+ .0. ) ) )
41	9	mpteq2dv 4745	. . . . . . 7 |- ( ( ph /\ W = (/) ) -> ( x e. A |-> ( .0. .+ .0. ) ) = ( x e. A |-> .0. ) )
42	40, 41	eqtrd 2656	. . . . . 6 |- ( ( ph /\ W = (/) ) -> ( F oF .+ H ) = ( x e. A |-> .0. ) )
43	42	oveq2d 6666	. . . . 5 |- ( ( ph /\ W = (/) ) -> ( G gsumg ( F oF .+ H ) ) = ( G gsumg ( x e. A |-> .0. ) ) )
44	43, 25	eqtrd 2656	. . . 4 |- ( ( ph /\ W = (/) ) -> ( G gsumg ( F oF .+ H ) ) = .0. )
45	9, 37, 44	3eqtr4rd 2667	. . 3 |- ( ( ph /\ W = (/) ) -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )
46	45	ex 450	. 2 |- ( ph -> ( W = (/) -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) ) )
47	1	adantr 481	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> G e. Mnd )
48	2, 6	mndcl 17301	. . . . . . . . . 10 |- ( ( G e. Mnd /\ z e. B /\ w e. B ) -> ( z .+ w ) e. B )
49	48	3expb 1266	. . . . . . . . 9 |- ( ( G e. Mnd /\ ( z e. B /\ w e. B ) ) -> ( z .+ w ) e. B )
50	47, 49	sylan 488	. . . . . . . 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 6826	. . . . . . 7 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
52		simprl 794	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( # ` W ) e. NN )
53		nnuz 11723	. . . . . . . 8 |- NN = ( ZZ>= ` 1 )
54	52, 53	syl6eleq 2711	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( # ` W ) e. ( ZZ>= ` 1 ) )
55	10	adantr 481	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> F : A --> B )
56		f1of1 6136	. . . . . . . . . . . 12 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> f : ( 1 ... ( # ` W ) ) -1-1-> W )
57	56	ad2antll 765	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> f : ( 1 ... ( # ` W ) ) -1-1-> W )
58		suppssdm 7308	. . . . . . . . . . . . . 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 5331	. . . . . . . . . . . . . 14 |- dom ( F u. H ) = ( dom F u. dom H )
62		fdm 6051	. . . . . . . . . . . . . . . . 17 |- ( F : A --> B -> dom F = A )
63	10, 62	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> dom F = A )
64		fdm 6051	. . . . . . . . . . . . . . . . 17 |- ( H : A --> B -> dom H = A )
65	15, 64	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> dom H = A )
66	63, 65	uneq12d 3768	. . . . . . . . . . . . . . 15 |- ( ph -> ( dom F u. dom H ) = ( A u. A ) )
67		unidm 3756	. . . . . . . . . . . . . . 15 |- ( A u. A ) = A
68	66, 67	syl6eq 2672	. . . . . . . . . . . . . 14 |- ( ph -> ( dom F u. dom H ) = A )
69	61, 68	syl5req 2669	. . . . . . . . . . . . 13 |- ( ph -> A = dom ( F u. H ) )
70	59, 60, 69	3sstr4d 3648	. . . . . . . . . . . 12 |- ( ph -> W C_ A )
71	70	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> W C_ A )
72		f1ss 6106	. . . . . . . . . . 11 |- ( ( f : ( 1 ... ( # ` W ) ) -1-1-> W /\ W C_ A ) -> f : ( 1 ... ( # ` W ) ) -1-1-> A )
73	57, 71, 72	syl2anc 693	. . . . . . . . . 10 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> f : ( 1 ... ( # ` W ) ) -1-1-> A )
74		f1f 6101	. . . . . . . . . 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 6058	. . . . . . . . 9 |- ( ( F : A --> B /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( F o. f ) : ( 1 ... ( # ` W ) ) --> B )
77	55, 75, 76	syl2anc 693	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F o. f ) : ( 1 ... ( # ` W ) ) --> B )
78	77	ffvelrnda 6359	. . . . . . 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 481	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> H : A --> B )
80		fco 6058	. . . . . . . . 9 |- ( ( H : A --> B /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( H o. f ) : ( 1 ... ( # ` W ) ) --> B )
81	79, 75, 80	syl2anc 693	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H o. f ) : ( 1 ... ( # ` W ) ) --> B )
82	81	ffvelrnda 6359	. . . . . . 7 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( H o. f ) ` k ) e. B )
83	55	ffnd 6046	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> F Fn A )
84	79	ffnd 6046	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> H Fn A )
85	11	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> A e. V )
86		ovexd 6680	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( 1 ... ( # ` W ) ) e. _V )
87		inidm 3822	. . . . . . . . . . 11 |- ( A i^i A ) = A
88	83, 84, 75, 85, 85, 86, 87	ofco 6917	. . . . . . . . . 10 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( ( F oF .+ H ) o. f ) = ( ( F o. f ) oF .+ ( H o. f ) ) )
89	88	fveq1d 6193	. . . . . . . . 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 ) )
90	89	adantr 481	. . . . . . . 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 ) )
91		fnfco 6069	. . . . . . . . . 10 |- ( ( F Fn A /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( F o. f ) Fn ( 1 ... ( # ` W ) ) )
92	83, 75, 91	syl2anc 693	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F o. f ) Fn ( 1 ... ( # ` W ) ) )
93		fnfco 6069	. . . . . . . . . 10 |- ( ( H Fn A /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( H o. f ) Fn ( 1 ... ( # ` W ) ) )
94	84, 75, 93	syl2anc 693	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H o. f ) Fn ( 1 ... ( # ` W ) ) )
95		inidm 3822	. . . . . . . . 9 |- ( ( 1 ... ( # ` W ) ) i^i ( 1 ... ( # ` W ) ) ) = ( 1 ... ( # ` W ) )
96		eqidd 2623	. . . . . . . . 9 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. f ) ` k ) = ( ( F o. f ) ` k ) )
97		eqidd 2623	. . . . . . . . 9 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( H o. f ) ` k ) = ( ( H o. f ) ` k ) )
98	92, 94, 86, 86, 95, 96, 97	ofval 6906	. . . . . . . 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 ) ) )
99	90, 98	eqtrd 2656	. . . . . . 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 ) ) )
100	1	ad2antrr 762	. . . . . . . 8 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> G e. Mnd )
101		elfzouz 12474	. . . . . . . . . 10 |- ( n e. ( 1..^ ( # ` W ) ) -> n e. ( ZZ>= ` 1 ) )
102	101	adantl 482	. . . . . . . . 9 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> n e. ( ZZ>= ` 1 ) )
103		elfzouz2 12484	. . . . . . . . . . . . 13 |- ( n e. ( 1..^ ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` n ) )
104	103	adantl 482	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( # ` W ) e. ( ZZ>= ` n ) )
105		fzss2 12381	. . . . . . . . . . . 12 |- ( ( # ` W ) e. ( ZZ>= ` n ) -> ( 1 ... n ) C_ ( 1 ... ( # ` W ) ) )
106	104, 105	syl 17	. . . . . . . . . . 11 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( 1 ... n ) C_ ( 1 ... ( # ` W ) ) )
107	106	sselda 3603	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) /\ k e. ( 1 ... n ) ) -> k e. ( 1 ... ( # ` W ) ) )
108	78	adantlr 751	. . . . . . . . . 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 )
109	107, 108	syldan 487	. . . . . . . . 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 )
110	2, 6	mndcl 17301	. . . . . . . . . . 11 |- ( ( G e. Mnd /\ k e. B /\ x e. B ) -> ( k .+ x ) e. B )
111	110	3expb 1266	. . . . . . . . . 10 |- ( ( G e. Mnd /\ ( k e. B /\ x e. B ) ) -> ( k .+ x ) e. B )
112	100, 111	sylan 488	. . . . . . . . 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 )
113	102, 109, 112	seqcl 12821	. . . . . . . 8 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( seq 1 ( .+ , ( F o. f ) ) ` n ) e. B )
114	82	adantlr 751	. . . . . . . . . 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 )
115	107, 114	syldan 487	. . . . . . . . 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 )
116	102, 115, 112	seqcl 12821	. . . . . . . 8 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( seq 1 ( .+ , ( H o. f ) ) ` n ) e. B )
117		fzofzp1 12565	. . . . . . . . 9 |- ( n e. ( 1..^ ( # ` W ) ) -> ( n + 1 ) e. ( 1 ... ( # ` W ) ) )
118		ffvelrn 6357	. . . . . . . . 9 |- ( ( ( F o. f ) : ( 1 ... ( # ` W ) ) --> B /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. f ) ` ( n + 1 ) ) e. B )
119	77, 117, 118	syl2an 494	. . . . . . . 8 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( ( F o. f ) ` ( n + 1 ) ) e. B )
120		ffvelrn 6357	. . . . . . . . 9 |- ( ( ( H o. f ) : ( 1 ... ( # ` W ) ) --> B /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( ( H o. f ) ` ( n + 1 ) ) e. B )
121	81, 117, 120	syl2an 494	. . . . . . . 8 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( ( H o. f ) ` ( n + 1 ) ) e. B )
122		fvco3 6275	. . . . . . . . . . . 12 |- ( ( f : ( 1 ... ( # ` W ) ) --> A /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. f ) ` ( n + 1 ) ) = ( F ` ( f ` ( n + 1 ) ) ) )
123	75, 117, 122	syl2an 494	. . . . . . . . . . 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 ) ) ) )
124		fveq2 6191	. . . . . . . . . . . . 13 |- ( k = ( f ` ( n + 1 ) ) -> ( F ` k ) = ( F ` ( f ` ( n + 1 ) ) ) )
125	124	eleq1d 2686	. . . . . . . . . . . 12 |- ( 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 ) ) ) ) } ) ) )
126		gsumzaddlem.4	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) )
127	126	expr 643	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x C_ A ) -> ( k e. ( A \ x ) -> ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) ) )
128	127	ralrimiv 2965	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x C_ A ) -> A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) )
129	128	ex 450	. . . . . . . . . . . . . . 15 |- ( ph -> ( x C_ A -> A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) ) )
130	129	alrimiv 1855	. . . . . . . . . . . . . 14 |- ( ph -> A. x ( x C_ A -> A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) ) )
131	130	ad2antrr 762	. . . . . . . . . . . . 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 ) ) } ) ) )
132		imassrn 5477	. . . . . . . . . . . . . 14 |- ( f " ( 1 ... n ) ) C_ ran f
133	75	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> f : ( 1 ... ( # ` W ) ) --> A )
134		frn 6053	. . . . . . . . . . . . . . 15 |- ( f : ( 1 ... ( # ` W ) ) --> A -> ran f C_ A )
135	133, 134	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ran f C_ A )
136	132, 135	syl5ss 3614	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( f " ( 1 ... n ) ) C_ A )
137		vex 3203	. . . . . . . . . . . . . . 15 |- f e. _V
138	137	imaex 7104	. . . . . . . . . . . . . 14 |- ( f " ( 1 ... n ) ) e. _V
139		sseq1 3626	. . . . . . . . . . . . . . 15 |- ( x = ( f " ( 1 ... n ) ) -> ( x C_ A <-> ( f " ( 1 ... n ) ) C_ A ) )
140		difeq2 3722	. . . . . . . . . . . . . . . 16 |- ( x = ( f " ( 1 ... n ) ) -> ( A \ x ) = ( A \ ( f " ( 1 ... n ) ) ) )
141		reseq2 5391	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( f " ( 1 ... n ) ) -> ( H |` x ) = ( H |` ( f " ( 1 ... n ) ) ) )
142	141	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( f " ( 1 ... n ) ) -> ( G gsumg ( H |` x ) ) = ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) )
143	142	sneqd 4189	. . . . . . . . . . . . . . . . . 18 |- ( x = ( f " ( 1 ... n ) ) -> { ( G gsumg ( H |` x ) ) } = { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } )
144	143	fveq2d 6195	. . . . . . . . . . . . . . . . 17 |- ( x = ( f " ( 1 ... n ) ) -> ( Z ` { ( G gsumg ( H |` x ) ) } ) = ( Z ` { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } ) )
145	144	eleq2d 2687	. . . . . . . . . . . . . . . 16 |- ( x = ( f " ( 1 ... n ) ) -> ( ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) <-> ( F ` k ) e. ( Z ` { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } ) ) )
146	140, 145	raleqbidv 3152	. . . . . . . . . . . . . . 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 ) ) ) ) } ) ) )
147	139, 146	imbi12d 334	. . . . . . . . . . . . . 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 ) ) ) ) } ) ) ) )
148	138, 147	spcv 3299	. . . . . . . . . . . . 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 ) ) ) ) } ) ) )
149	131, 136, 148	sylc 65	. . . . . . . . . . . 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 ) ) ) ) } ) )
150		ffvelrn 6357	. . . . . . . . . . . . . 14 |- ( ( f : ( 1 ... ( # ` W ) ) --> A /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( f ` ( n + 1 ) ) e. A )
151	75, 117, 150	syl2an 494	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( f ` ( n + 1 ) ) e. A )
152		fzp1nel 12424	. . . . . . . . . . . . . 14 |- -. ( n + 1 ) e. ( 1 ... n )
153	73	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> f : ( 1 ... ( # ` W ) ) -1-1-> A )
154	117	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( n + 1 ) e. ( 1 ... ( # ` W ) ) )
155		f1elima 6520	. . . . . . . . . . . . . . 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 ) ) )
156	153, 154, 106, 155	syl3anc 1326	. . . . . . . . . . . . . 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 ) ) )
157	152, 156	mtbiri 317	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> -. ( f ` ( n + 1 ) ) e. ( f " ( 1 ... n ) ) )
158	151, 157	eldifd 3585	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( f ` ( n + 1 ) ) e. ( A \ ( f " ( 1 ... n ) ) ) )
159	125, 149, 158	rspcdva 3316	. . . . . . . . . . 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 ) ) ) ) } ) )
160	123, 159	eqeltrd 2701	. . . . . . . . . 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 ) ) ) ) } ) )
161		gsumzadd.z	. . . . . . . . . . . . 13 |- Z = (Cntz ` G )
162	138	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( f " ( 1 ... n ) ) e. _V )
163	15	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> H : A --> B )
164	163, 136	fssresd 6071	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( H |` ( f " ( 1 ... n ) ) ) : ( f " ( 1 ... n ) ) --> B )
165		gsumzaddlem.2	. . . . . . . . . . . . . . 15 |- ( ph -> ran H C_ ( Z ` ran H ) )
166	165	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ran H C_ ( Z ` ran H ) )
167		resss 5422	. . . . . . . . . . . . . . 15 |- ( H |` ( f " ( 1 ... n ) ) ) C_ H
168		rnss 5354	. . . . . . . . . . . . . . 15 |- ( ( H |` ( f " ( 1 ... n ) ) ) C_ H -> ran ( H |` ( f " ( 1 ... n ) ) ) C_ ran H )
169	167, 168	ax-mp 5	. . . . . . . . . . . . . 14 |- ran ( H |` ( f " ( 1 ... n ) ) ) C_ ran H
170	161	cntzidss 17770	. . . . . . . . . . . . . 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 ) ) ) ) )
171	166, 169, 170	sylancl 694	. . . . . . . . . . . . 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 ) ) ) ) )
172	102, 53	syl6eleqr 2712	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> n e. NN )
173		f1ores 6151	. . . . . . . . . . . . . . 15 |- ( ( f : ( 1 ... ( # ` W ) ) -1-1-> A /\ ( 1 ... n ) C_ ( 1 ... ( # ` W ) ) ) -> ( f |` ( 1 ... n ) ) : ( 1 ... n ) -1-1-onto-> ( f " ( 1 ... n ) ) )
174	153, 106, 173	syl2anc 693	. . . . . . . . . . . . . 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 ) ) )
175		f1of1 6136	. . . . . . . . . . . . . 14 |- ( ( f |` ( 1 ... n ) ) : ( 1 ... n ) -1-1-onto-> ( f " ( 1 ... n ) ) -> ( f |` ( 1 ... n ) ) : ( 1 ... n ) -1-1-> ( f " ( 1 ... n ) ) )
176	174, 175	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 ) ) )
177		suppssdm 7308	. . . . . . . . . . . . . . 15 |- ( ( H |` ( f " ( 1 ... n ) ) ) supp .0. ) C_ dom ( H |` ( f " ( 1 ... n ) ) )
178		dmres 5419	. . . . . . . . . . . . . . . 16 |- dom ( H |` ( f " ( 1 ... n ) ) ) = ( ( f " ( 1 ... n ) ) i^i dom H )
179	178	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 ) )
180	177, 179	syl5sseq 3653	. . . . . . . . . . . . . 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 ) )
181		inss1 3833	. . . . . . . . . . . . . . 15 |- ( ( f " ( 1 ... n ) ) i^i dom H ) C_ ( f " ( 1 ... n ) )
182		df-ima 5127	. . . . . . . . . . . . . . . 16 |- ( f " ( 1 ... n ) ) = ran ( f |` ( 1 ... n ) )
183	182	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 ) ) )
184	181, 183	syl5sseq 3653	. . . . . . . . . . . . . 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 ) ) )
185	180, 184	sstrd 3613	. . . . . . . . . . . . 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 ) ) )
186		eqid 2622	. . . . . . . . . . . . 13 |- ( ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) supp .0. ) = ( ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) supp .0. )
187	2, 3, 6, 161, 100, 162, 164, 171, 172, 176, 185, 186	gsumval3 18308	. . . . . . . . . . . 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 ) )
188	182	eqimss2i 3660	. . . . . . . . . . . . . . . . . 18 |- ran ( f |` ( 1 ... n ) ) C_ ( f " ( 1 ... n ) )
189		cores 5638	. . . . . . . . . . . . . . . . . 18 |- ( ran ( f |` ( 1 ... n ) ) C_ ( f " ( 1 ... n ) ) -> ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) = ( H o. ( f |` ( 1 ... n ) ) ) )
190	188, 189	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) = ( H o. ( f |` ( 1 ... n ) ) )
191		resco 5639	. . . . . . . . . . . . . . . . 17 |- ( ( H o. f ) |` ( 1 ... n ) ) = ( H o. ( f |` ( 1 ... n ) ) )
192	190, 191	eqtr4i 2647	. . . . . . . . . . . . . . . 16 |- ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) = ( ( H o. f ) |` ( 1 ... n ) )
193	192	fveq1i 6192	. . . . . . . . . . . . . . 15 |- ( ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) ` k ) = ( ( ( H o. f ) |` ( 1 ... n ) ) ` k )
194		fvres 6207	. . . . . . . . . . . . . . 15 |- ( k e. ( 1 ... n ) -> ( ( ( H o. f ) |` ( 1 ... n ) ) ` k ) = ( ( H o. f ) ` k ) )
195	193, 194	syl5eq 2668	. . . . . . . . . . . . . 14 |- ( k e. ( 1 ... n ) -> ( ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) ` k ) = ( ( H o. f ) ` k ) )
196	195	adantl 482	. . . . . . . . . . . . 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 ) )
197	102, 196	seqfveq 12825	. . . . . . . . . . . 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 ) )
198	187, 197	eqtr2d 2657	. . . . . . . . . . 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 ) ) ) ) )
199		fvex 6201	. . . . . . . . . . . 12 |- ( seq 1 ( .+ , ( H o. f ) ) ` n ) e. _V
200	199	elsn 4192	. . . . . . . . . . 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 ) ) ) ) )
201	198, 200	sylibr 224	. . . . . . . . . 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 ) ) ) ) } )
202	6, 161	cntzi 17762	. . . . . . . . . 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 ) ) ) )
203	160, 201, 202	syl2anc 693	. . . . . . . . 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 ) ) ) )
204	203	eqcomd 2628	. . . . . . . 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 ) ) )
205	2, 6, 100, 113, 116, 119, 121, 204	mnd4g 17307	. . . . . . 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 ) ) ) ) )
206	51, 51, 54, 78, 82, 99, 205	seqcaopr3 12836	. . . . . 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 ) ) ) )
207	50, 55, 79, 85, 85, 87	off 6912	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F oF .+ H ) : A --> B )
208		gsumzaddlem.3	. . . . . . . 8 |- ( ph -> ran ( F oF .+ H ) C_ ( Z ` ran ( F oF .+ H ) ) )
209	208	adantr 481	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ran ( F oF .+ H ) C_ ( Z ` ran ( F oF .+ H ) ) )
210	47, 111	sylan 488	. . . . . . . . 9 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ ( k e. B /\ x e. B ) ) -> ( k .+ x ) e. B )
211	210, 55, 79, 85, 85, 87	off 6912	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F oF .+ H ) : A --> B )
212		eldifi 3732	. . . . . . . . . 10 |- ( x e. ( A \ ran f ) -> x e. A )
213		eqidd 2623	. . . . . . . . . . 11 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
214		eqidd 2623	. . . . . . . . . . 11 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. A ) -> ( H ` x ) = ( H ` x ) )
215	83, 84, 85, 85, 87, 213, 214	ofval 6906	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. A ) -> ( ( F oF .+ H ) ` x ) = ( ( F ` x ) .+ ( H ` x ) ) )
216	212, 215	sylan2 491	. . . . . . . . 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 ) ) )
217	18	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F supp .0. ) C_ ( ( F u. H ) supp .0. ) )
218		f1ofo 6144	. . . . . . . . . . . . . . . 16 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> f : ( 1 ... ( # ` W ) ) -onto-> W )
219		forn 6118	. . . . . . . . . . . . . . . 16 |- ( f : ( 1 ... ( # ` W ) ) -onto-> W -> ran f = W )
220	218, 219	syl 17	. . . . . . . . . . . . . . 15 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ran f = W )
221	220, 19	syl6eq 2672	. . . . . . . . . . . . . 14 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ran f = ( ( F u. H ) supp .0. ) )
222	221	sseq2d 3633	. . . . . . . . . . . . 13 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ( ( F supp .0. ) C_ ran f <-> ( F supp .0. ) C_ ( ( F u. H ) supp .0. ) ) )
223	222	ad2antll 765	. . . . . . . . . . . 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. ) ) )
224	217, 223	mpbird 247	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F supp .0. ) C_ ran f )
225	13	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> .0. e. _V )
226	55, 224, 85, 225	suppssr 7326	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( F ` x ) = .0. )
227	29	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H supp .0. ) C_ ( ( H u. F ) supp .0. ) )
228	227, 31	syl6sseqr 3652	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H supp .0. ) C_ ( ( F u. H ) supp .0. ) )
229	221	sseq2d 3633	. . . . . . . . . . . . 13 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ( ( H supp .0. ) C_ ran f <-> ( H supp .0. ) C_ ( ( F u. H ) supp .0. ) ) )
230	229	ad2antll 765	. . . . . . . . . . . 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. ) ) )
231	228, 230	mpbird 247	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H supp .0. ) C_ ran f )
232	79, 231, 85, 225	suppssr 7326	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( H ` x ) = .0. )
233	226, 232	oveq12d 6668	. . . . . . . . 9 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( ( F ` x ) .+ ( H ` x ) ) = ( .0. .+ .0. ) )
234	8	ad2antrr 762	. . . . . . . . 9 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( .0. .+ .0. ) = .0. )
235	216, 233, 234	3eqtrd 2660	. . . . . . . 8 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( ( F oF .+ H ) ` x ) = .0. )
236	211, 235	suppss 7325	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( ( F oF .+ H ) supp .0. ) C_ ran f )
237		ovex 6678	. . . . . . . . 9 |- ( F oF .+ H ) e. _V
238	237, 137	coex 7118	. . . . . . . 8 |- ( ( F oF .+ H ) o. f ) e. _V
239		suppimacnv 7306	. . . . . . . . 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. } ) ) )
240	239	eqcomd 2628	. . . . . . . 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. ) )
241	238, 13, 240	mp2an 708	. . . . . . 7 |- ( `' ( ( F oF .+ H ) o. f ) " ( _V \ { .0. } ) ) = ( ( ( F oF .+ H ) o. f ) supp .0. )
242	2, 3, 6, 161, 47, 85, 207, 209, 52, 73, 236, 241	gsumval3 18308	. . . . . 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 ) ) )
243		gsumzaddlem.1	. . . . . . . . 9 |- ( ph -> ran F C_ ( Z ` ran F ) )
244	243	adantr 481	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ran F C_ ( Z ` ran F ) )
245		eqid 2622	. . . . . . . 8 |- ( ( F o. f ) supp .0. ) = ( ( F o. f ) supp .0. )
246	2, 3, 6, 161, 47, 85, 55, 244, 52, 73, 224, 245	gsumval3 18308	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( G gsumg F ) = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) )
247	165	adantr 481	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ran H C_ ( Z ` ran H ) )
248		eqid 2622	. . . . . . . 8 |- ( ( H o. f ) supp .0. ) = ( ( H o. f ) supp .0. )
249	2, 3, 6, 161, 47, 85, 79, 247, 52, 73, 231, 248	gsumval3 18308	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( G gsumg H ) = ( seq 1 ( .+ , ( H o. f ) ) ` ( # ` W ) ) )
250	246, 249	oveq12d 6668	. . . . . 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 ) ) ) )
251	206, 242, 250	3eqtr4d 2666	. . . . 5 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )
252	251	expr 643	. . . 4 |- ( ( ph /\ ( # ` W ) e. NN ) -> ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) ) )
253	252	exlimdv 1861	. . 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 ) ) ) )
254	253	expimpd 629	. 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 ) ) ) )
255		gsumzadd.fn	. . . . 5 |- ( ph -> F finSupp .0. )
256		gsumzadd.hn	. . . . 5 |- ( ph -> H finSupp .0. )
257	255, 256	fsuppun 8294	. . . 4 |- ( ph -> ( ( F u. H ) supp .0. ) e. Fin )
258	19, 257	syl5eqel 2705	. . 3 |- ( ph -> W e. Fin )
259		fz1f1o 14441	. . 3 |- ( W e. Fin -> ( W = (/) \/ ( ( # ` W ) e. NN /\ E. f f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) )
260	258, 259	syl 17	. 2 |- ( ph -> ( W = (/) \/ ( ( # ` W ) e. NN /\ E. f f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) )
261	46, 254, 260	mpjaod 396	1 |- ( ph -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )

Syntax hints:   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   A.wal 1481   = wceq 1483   E.wex 1704   e. wcel 1990   A.wral 2912   _Vcvv 3200   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   {csn 4177   class class class wbr 4653   |-> cmpt 4729   `'ccnv 5113   dom cdm 5114   ran crn 5115   |` cres 5116   "cima 5117   o. ccom 5118   Fn wfn 5883   -->wf 5884   -1-1->wf1 5885   -onto->wfo 5886   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   oFcof 6895   supp csupp 7295   Fincfn 7955   finSupp cfsupp 8275   1c1 9937   + caddc 9939   NNcn 11020   ZZ>=cuz 11687   ...cfz 12326  ..^cfzo 12465   seqcseq 12801   #chash 13117   Basecbs 15857   +g cplusg 15941   0gc0g 16100   gsum_g cgsu 16101   Mndcmnd 17294  Cntzccntz 17748

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-n0 11293  df-z 11378  df-uz 11688  df-fz 12327  df-fzo 12466  df-seq 12802  df-hash 13118  df-0g 16102  df-gsum 16103  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-cntz 17750

This theorem is referenced by:  gsumzadd  18322  dprdfadd  18419