Theorem gsumzaddlem 16401

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 15435	. . . . . . 7 |- ( G e. Mnd -> .0. e. B )
5	1, 4	syl 16	. . . . . 6 |- ( ph -> .0. e. B )
6		gsumzadd.p	. . . . . . 7 |- .+ = ( +g ` G )
7	2, 6, 3	mndlid 15437	. . . . . 6 |- ( ( G e. Mnd /\ .0. e. B ) -> ( .0. .+ .0. ) = .0. )
8	1, 5, 7	syl2anc 656	. . . . 5 |- ( ph -> ( .0. .+ .0. ) = .0. )
9	8	adantr 462	. . . 4 |- ( ( ph /\ W = (/) ) -> ( .0. .+ .0. ) = .0. )
10		gsumzaddlem.f	. . . . . . . 8 |- ( ph -> F : A --> B )
11		gsumzadd.a	. . . . . . . 8 |- ( ph -> A e. V )
12		fvex 5698	. . . . . . . . . 10 |- ( 0g ` G ) e. _V
13	3, 12	eqeltri 2511	. . . . . . . . 9 |- .0. e. _V
14	13	a1i 11	. . . . . . . 8 |- ( ph -> .0. e. _V )
15		gsumzaddlem.h	. . . . . . . . . . 11 |- ( ph -> H : A --> B )
16		fex 5947	. . . . . . . . . . 11 |- ( ( H : A --> B /\ A e. V ) -> H e. _V )
17	15, 11, 16	syl2anc 656	. . . . . . . . . 10 |- ( ph -> H e. _V )
18	17	suppun 6708	. . . . . . . . 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 3400	. . . . . . . 8 |- ( ph -> ( F supp .0. ) C_ W )
21	10, 11, 14, 20	gsumcllem 16379	. . . . . . 7 |- ( ( ph /\ W = (/) ) -> F = ( x e. A |-> .0. ) )
22	21	oveq2d 6106	. . . . . 6 |- ( ( ph /\ W = (/) ) -> ( G gsumg F ) = ( G gsumg ( x e. A |-> .0. ) ) )
23	3	gsumz 15504	. . . . . . . 8 |- ( ( G e. Mnd /\ A e. V ) -> ( G gsumg ( x e. A |-> .0. ) ) = .0. )
24	1, 11, 23	syl2anc 656	. . . . . . 7 |- ( ph -> ( G gsumg ( x e. A |-> .0. ) ) = .0. )
25	24	adantr 462	. . . . . 6 |- ( ( ph /\ W = (/) ) -> ( G gsumg ( x e. A |-> .0. ) ) = .0. )
26	22, 25	eqtrd 2473	. . . . 5 |- ( ( ph /\ W = (/) ) -> ( G gsumg F ) = .0. )
27		fex 5947	. . . . . . . . . . . 12 |- ( ( F : A --> B /\ A e. V ) -> F e. _V )
28	10, 11, 27	syl2anc 656	. . . . . . . . . . 11 |- ( ph -> F e. _V )
29	28	suppun 6708	. . . . . . . . . 10 |- ( ph -> ( H supp .0. ) C_ ( ( H u. F ) supp .0. ) )
30		uncom 3497	. . . . . . . . . . 11 |- ( F u. H ) = ( H u. F )
31	30	oveq1i 6100	. . . . . . . . . 10 |- ( ( F u. H ) supp .0. ) = ( ( H u. F ) supp .0. )
32	29, 31	syl6sseqr 3400	. . . . . . . . 9 |- ( ph -> ( H supp .0. ) C_ ( ( F u. H ) supp .0. ) )
33	32, 19	syl6sseqr 3400	. . . . . . . 8 |- ( ph -> ( H supp .0. ) C_ W )
34	15, 11, 14, 33	gsumcllem 16379	. . . . . . 7 |- ( ( ph /\ W = (/) ) -> H = ( x e. A |-> .0. ) )
35	34	oveq2d 6106	. . . . . 6 |- ( ( ph /\ W = (/) ) -> ( G gsumg H ) = ( G gsumg ( x e. A |-> .0. ) ) )
36	35, 25	eqtrd 2473	. . . . 5 |- ( ( ph /\ W = (/) ) -> ( G gsumg H ) = .0. )
37	26, 36	oveq12d 6108	. . . 4 |- ( ( ph /\ W = (/) ) -> ( ( G gsumg F ) .+ ( G gsumg H ) ) = ( .0. .+ .0. ) )
38	11	adantr 462	. . . . . . . 8 |- ( ( ph /\ W = (/) ) -> A e. V )
39	5	ad2antrr 720	. . . . . . . 8 |- ( ( ( ph /\ W = (/) ) /\ x e. A ) -> .0. e. B )
40	38, 39, 39, 21, 34	offval2 6335	. . . . . . 7 |- ( ( ph /\ W = (/) ) -> ( F oF .+ H ) = ( x e. A |-> ( .0. .+ .0. ) ) )
41	9	mpteq2dv 4376	. . . . . . 7 |- ( ( ph /\ W = (/) ) -> ( x e. A |-> ( .0. .+ .0. ) ) = ( x e. A |-> .0. ) )
42	40, 41	eqtrd 2473	. . . . . 6 |- ( ( ph /\ W = (/) ) -> ( F oF .+ H ) = ( x e. A |-> .0. ) )
43	42	oveq2d 6106	. . . . 5 |- ( ( ph /\ W = (/) ) -> ( G gsumg ( F oF .+ H ) ) = ( G gsumg ( x e. A |-> .0. ) ) )
44	43, 25	eqtrd 2473	. . . 4 |- ( ( ph /\ W = (/) ) -> ( G gsumg ( F oF .+ H ) ) = .0. )
45	9, 37, 44	3eqtr4rd 2484	. . 3 |- ( ( ph /\ W = (/) ) -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )
46	45	ex 434	. 2 |- ( ph -> ( W = (/) -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) ) )
47	1	adantr 462	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> G e. Mnd )
48	2, 6	mndcl 15416	. . . . . . . . . 10 |- ( ( G e. Mnd /\ z e. B /\ w e. B ) -> ( z .+ w ) e. B )
49	48	3expb 1183	. . . . . . . . 9 |- ( ( G e. Mnd /\ ( z e. B /\ w e. B ) ) -> ( z .+ w ) e. B )
50	47, 49	sylan 468	. . . . . . . 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 6254	. . . . . . 7 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
52		simprl 750	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( # ` W ) e. NN )
53		nnuz 10892	. . . . . . . 8 |- NN = ( ZZ>= ` 1 )
54	52, 53	syl6eleq 2531	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( # ` W ) e. ( ZZ>= ` 1 ) )
55	10	adantr 462	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> F : A --> B )
56		f1of1 5637	. . . . . . . . . . . 12 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> f : ( 1 ... ( # ` W ) ) -1-1-> W )
57	56	ad2antll 723	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> f : ( 1 ... ( # ` W ) ) -1-1-> W )
58		suppssdm 6702	. . . . . . . . . . . . . 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 5042	. . . . . . . . . . . . . 14 |- dom ( F u. H ) = ( dom F u. dom H )
62		fdm 5560	. . . . . . . . . . . . . . . . 17 |- ( F : A --> B -> dom F = A )
63	10, 62	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> dom F = A )
64		fdm 5560	. . . . . . . . . . . . . . . . 17 |- ( H : A --> B -> dom H = A )
65	15, 64	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> dom H = A )
66	63, 65	uneq12d 3508	. . . . . . . . . . . . . . 15 |- ( ph -> ( dom F u. dom H ) = ( A u. A ) )
67		unidm 3496	. . . . . . . . . . . . . . 15 |- ( A u. A ) = A
68	66, 67	syl6eq 2489	. . . . . . . . . . . . . 14 |- ( ph -> ( dom F u. dom H ) = A )
69	61, 68	syl5req 2486	. . . . . . . . . . . . 13 |- ( ph -> A = dom ( F u. H ) )
70	59, 60, 69	3sstr4d 3396	. . . . . . . . . . . 12 |- ( ph -> W C_ A )
71	70	adantr 462	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> W C_ A )
72		f1ss 5608	. . . . . . . . . . 11 |- ( ( f : ( 1 ... ( # ` W ) ) -1-1-> W /\ W C_ A ) -> f : ( 1 ... ( # ` W ) ) -1-1-> A )
73	57, 71, 72	syl2anc 656	. . . . . . . . . 10 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> f : ( 1 ... ( # ` W ) ) -1-1-> A )
74		f1f 5603	. . . . . . . . . 10 |- ( f : ( 1 ... ( # ` W ) ) -1-1-> A -> f : ( 1 ... ( # ` W ) ) --> A )
75	73, 74	syl 16	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> f : ( 1 ... ( # ` W ) ) --> A )
76		fco 5565	. . . . . . . . 9 |- ( ( F : A --> B /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( F o. f ) : ( 1 ... ( # ` W ) ) --> B )
77	55, 75, 76	syl2anc 656	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F o. f ) : ( 1 ... ( # ` W ) ) --> B )
78	77	ffvelrnda 5840	. . . . . . 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 462	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> H : A --> B )
80		fco 5565	. . . . . . . . 9 |- ( ( H : A --> B /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( H o. f ) : ( 1 ... ( # ` W ) ) --> B )
81	79, 75, 80	syl2anc 656	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H o. f ) : ( 1 ... ( # ` W ) ) --> B )
82	81	ffvelrnda 5840	. . . . . . 7 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( H o. f ) ` k ) e. B )
83		ffn 5556	. . . . . . . . . . . 12 |- ( F : A --> B -> F Fn A )
84	55, 83	syl 16	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> F Fn A )
85		ffn 5556	. . . . . . . . . . . 12 |- ( H : A --> B -> H Fn A )
86	79, 85	syl 16	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> H Fn A )
87	11	adantr 462	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> A e. V )
88		ovex 6115	. . . . . . . . . . . 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 3556	. . . . . . . . . . 11 |- ( A i^i A ) = A
91	84, 86, 75, 87, 87, 89, 90	ofco 6339	. . . . . . . . . 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 5690	. . . . . . . . 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 462	. . . . . . . 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 5574	. . . . . . . . . 10 |- ( ( F Fn A /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( F o. f ) Fn ( 1 ... ( # ` W ) ) )
95	84, 75, 94	syl2anc 656	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F o. f ) Fn ( 1 ... ( # ` W ) ) )
96		fnfco 5574	. . . . . . . . . 10 |- ( ( H Fn A /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( H o. f ) Fn ( 1 ... ( # ` W ) ) )
97	86, 75, 96	syl2anc 656	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H o. f ) Fn ( 1 ... ( # ` W ) ) )
98		inidm 3556	. . . . . . . . 9 |- ( ( 1 ... ( # ` W ) ) i^i ( 1 ... ( # ` W ) ) ) = ( 1 ... ( # ` W ) )
99		eqidd 2442	. . . . . . . . 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 2442	. . . . . . . . 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 6328	. . . . . . . 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 2473	. . . . . . 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 720	. . . . . . . 8 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> G e. Mnd )
104		elfzouz 11553	. . . . . . . . . 10 |- ( n e. ( 1..^ ( # ` W ) ) -> n e. ( ZZ>= ` 1 ) )
105	104	adantl 463	. . . . . . . . 9 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> n e. ( ZZ>= ` 1 ) )
106		elfzouz2 11562	. . . . . . . . . . . . 13 |- ( n e. ( 1..^ ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` n ) )
107	106	adantl 463	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( # ` W ) e. ( ZZ>= ` n ) )
108		fzss2 11494	. . . . . . . . . . . 12 |- ( ( # ` W ) e. ( ZZ>= ` n ) -> ( 1 ... n ) C_ ( 1 ... ( # ` W ) ) )
109	107, 108	syl 16	. . . . . . . . . . 11 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( 1 ... n ) C_ ( 1 ... ( # ` W ) ) )
110	109	sselda 3353	. . . . . . . . . 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 709	. . . . . . . . . 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 467	. . . . . . . . 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 15416	. . . . . . . . . . 11 |- ( ( G e. Mnd /\ k e. B /\ x e. B ) -> ( k .+ x ) e. B )
114	113	3expb 1183	. . . . . . . . . 10 |- ( ( G e. Mnd /\ ( k e. B /\ x e. B ) ) -> ( k .+ x ) e. B )
115	103, 114	sylan 468	. . . . . . . . 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 11822	. . . . . . . 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 709	. . . . . . . . . 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 467	. . . . . . . . 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 11822	. . . . . . . 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 11620	. . . . . . . . 9 |- ( n e. ( 1..^ ( # ` W ) ) -> ( n + 1 ) e. ( 1 ... ( # ` W ) ) )
121		ffvelrn 5838	. . . . . . . . 9 |- ( ( ( F o. f ) : ( 1 ... ( # ` W ) ) --> B /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. f ) ` ( n + 1 ) ) e. B )
122	77, 120, 121	syl2an 474	. . . . . . . 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 5838	. . . . . . . . 9 |- ( ( ( H o. f ) : ( 1 ... ( # ` W ) ) --> B /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( ( H o. f ) ` ( n + 1 ) ) e. B )
124	81, 120, 123	syl2an 474	. . . . . . . 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 5765	. . . . . . . . . . . 12 |- ( ( f : ( 1 ... ( # ` W ) ) --> A /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. f ) ` ( n + 1 ) ) = ( F ` ( f ` ( n + 1 ) ) ) )
126	75, 120, 125	syl2an 474	. . . . . . . . . . 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 5838	. . . . . . . . . . . . . 14 |- ( ( f : ( 1 ... ( # ` W ) ) --> A /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( f ` ( n + 1 ) ) e. A )
128	75, 120, 127	syl2an 474	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( f ` ( n + 1 ) ) e. A )
129		fzp1disj 11511	. . . . . . . . . . . . . . 15 |- ( ( 1 ... n ) i^i { ( n + 1 ) } ) = (/)
130		disjsn 3933	. . . . . . . . . . . . . . 15 |- ( ( ( 1 ... n ) i^i { ( n + 1 ) } ) = (/) <-> -. ( n + 1 ) e. ( 1 ... n ) )
131	129, 130	mpbi 208	. . . . . . . . . . . . . 14 |- -. ( n + 1 ) e. ( 1 ... n )
132	73	adantr 462	. . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( n + 1 ) e. ( 1 ... ( # ` W ) ) )
134		f1elima 5973	. . . . . . . . . . . . . . 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 1213	. . . . . . . . . . . . . 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 303	. . . . . . . . . . . . 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 3336	. . . . . . . . . . . 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 612	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x C_ A ) -> ( k e. ( A \ x ) -> ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) ) )
140	139	ralrimiv 2796	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x C_ A ) -> A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) )
141	140	ex 434	. . . . . . . . . . . . . . 15 |- ( ph -> ( x C_ A -> A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) ) )
142	141	alrimiv 1690	. . . . . . . . . . . . . 14 |- ( ph -> A. x ( x C_ A -> A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) ) )
143	142	ad2antrr 720	. . . . . . . . . . . . 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 5177	. . . . . . . . . . . . . 14 |- ( f " ( 1 ... n ) ) C_ ran f
145	75	adantr 462	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> f : ( 1 ... ( # ` W ) ) --> A )
146		frn 5562	. . . . . . . . . . . . . . 15 |- ( f : ( 1 ... ( # ` W ) ) --> A -> ran f C_ A )
147	145, 146	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ran f C_ A )
148	144, 147	syl5ss 3364	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( f " ( 1 ... n ) ) C_ A )
149		vex 2973	. . . . . . . . . . . . . . 15 |- f e. _V
150		imaexg 6514	. . . . . . . . . . . . . . 15 |- ( f e. _V -> ( f " ( 1 ... n ) ) e. _V )
151	149, 150	ax-mp 5	. . . . . . . . . . . . . 14 |- ( f " ( 1 ... n ) ) e. _V
152		sseq1 3374	. . . . . . . . . . . . . . 15 |- ( x = ( f " ( 1 ... n ) ) -> ( x C_ A <-> ( f " ( 1 ... n ) ) C_ A ) )
153		difeq2 3465	. . . . . . . . . . . . . . . 16 |- ( x = ( f " ( 1 ... n ) ) -> ( A \ x ) = ( A \ ( f " ( 1 ... n ) ) ) )
154		reseq2 5101	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( f " ( 1 ... n ) ) -> ( H |` x ) = ( H |` ( f " ( 1 ... n ) ) ) )
155	154	oveq2d 6106	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( f " ( 1 ... n ) ) -> ( G gsumg ( H |` x ) ) = ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) )
156	155	sneqd 3886	. . . . . . . . . . . . . . . . . 18 |- ( x = ( f " ( 1 ... n ) ) -> { ( G gsumg ( H |` x ) ) } = { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } )
157	156	fveq2d 5692	. . . . . . . . . . . . . . . . 17 |- ( x = ( f " ( 1 ... n ) ) -> ( Z ` { ( G gsumg ( H |` x ) ) } ) = ( Z ` { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } ) )
158	157	eleq2d 2508	. . . . . . . . . . . . . . . 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 2929	. . . . . . . . . . . . . . 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 320	. . . . . . . . . . . . . 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 3060	. . . . . . . . . . . . 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 60	. . . . . . . . . . . 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 5688	. . . . . . . . . . . . . 14 |- ( k = ( f ` ( n + 1 ) ) -> ( F ` k ) = ( F ` ( f ` ( n + 1 ) ) ) )
164	163	eleq1d 2507	. . . . . . . . . . . . 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 3066	. . . . . . . . . . . 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 60	. . . . . . . . . . 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 2515	. . . . . . . . . 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 720	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> H : A --> B )
171		fssres 5575	. . . . . . . . . . . . . 14 |- ( ( H : A --> B /\ ( f " ( 1 ... n ) ) C_ A ) -> ( H |` ( f " ( 1 ... n ) ) ) : ( f " ( 1 ... n ) ) --> B )
172	170, 148, 171	syl2anc 656	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( H |` ( f " ( 1 ... n ) ) ) : ( f " ( 1 ... n ) ) --> B )
173		gsumzaddlem.2	. . . . . . . . . . . . . . 15 |- ( ph -> ran H C_ ( Z ` ran H ) )
174	173	ad2antrr 720	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ran H C_ ( Z ` ran H ) )
175		resss 5131	. . . . . . . . . . . . . . 15 |- ( H |` ( f " ( 1 ... n ) ) ) C_ H
176		rnss 5064	. . . . . . . . . . . . . . 15 |- ( ( H |` ( f " ( 1 ... n ) ) ) C_ H -> ran ( H |` ( f " ( 1 ... n ) ) ) C_ ran H )
177	175, 176	ax-mp 5	. . . . . . . . . . . . . 14 |- ran ( H |` ( f " ( 1 ... n ) ) ) C_ ran H
178	168	cntzidss 15848	. . . . . . . . . . . . . 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 ) ) ) ) )
179	174, 177, 178	sylancl 657	. . . . . . . . . . . . 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 ) ) ) ) )
180	105, 53	syl6eleqr 2532	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> n e. NN )
181		f1ores 5652	. . . . . . . . . . . . . . 15 |- ( ( f : ( 1 ... ( # ` W ) ) -1-1-> A /\ ( 1 ... n ) C_ ( 1 ... ( # ` W ) ) ) -> ( f |` ( 1 ... n ) ) : ( 1 ... n ) -1-1-onto-> ( f " ( 1 ... n ) ) )
182	132, 109, 181	syl2anc 656	. . . . . . . . . . . . . 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 ) ) )
183		f1of1 5637	. . . . . . . . . . . . . 14 |- ( ( f |` ( 1 ... n ) ) : ( 1 ... n ) -1-1-onto-> ( f " ( 1 ... n ) ) -> ( f |` ( 1 ... n ) ) : ( 1 ... n ) -1-1-> ( f " ( 1 ... n ) ) )
184	182, 183	syl 16	. . . . . . . . . . . . 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 ) ) )
185		suppssdm 6702	. . . . . . . . . . . . . . 15 |- ( ( H |` ( f " ( 1 ... n ) ) ) supp .0. ) C_ dom ( H |` ( f " ( 1 ... n ) ) )
186		dmres 5128	. . . . . . . . . . . . . . . 16 |- dom ( H |` ( f " ( 1 ... n ) ) ) = ( ( f " ( 1 ... n ) ) i^i dom H )
187	186	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 ) )
188	185, 187	syl5sseq 3401	. . . . . . . . . . . . . 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 ) )
189		inss1 3567	. . . . . . . . . . . . . . 15 |- ( ( f " ( 1 ... n ) ) i^i dom H ) C_ ( f " ( 1 ... n ) )
190		df-ima 4849	. . . . . . . . . . . . . . . 16 |- ( f " ( 1 ... n ) ) = ran ( f |` ( 1 ... n ) )
191	190	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 ) ) )
192	189, 191	syl5sseq 3401	. . . . . . . . . . . . . 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 ) ) )
193	188, 192	sstrd 3363	. . . . . . . . . . . . 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 ) ) )
194		eqid 2441	. . . . . . . . . . . . 13 |- ( ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) supp .0. ) = ( ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) supp .0. )
195	2, 3, 6, 168, 103, 169, 172, 179, 180, 184, 193, 194	gsumval3 16378	. . . . . . . . . . . 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 ) )
196	190	eqimss2i 3408	. . . . . . . . . . . . . . . . . 18 |- ran ( f |` ( 1 ... n ) ) C_ ( f " ( 1 ... n ) )
197		cores 5338	. . . . . . . . . . . . . . . . . 18 |- ( ran ( f |` ( 1 ... n ) ) C_ ( f " ( 1 ... n ) ) -> ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) = ( H o. ( f |` ( 1 ... n ) ) ) )
198	196, 197	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) = ( H o. ( f |` ( 1 ... n ) ) )
199		resco 5339	. . . . . . . . . . . . . . . . 17 |- ( ( H o. f ) |` ( 1 ... n ) ) = ( H o. ( f |` ( 1 ... n ) ) )
200	198, 199	eqtr4i 2464	. . . . . . . . . . . . . . . 16 |- ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) = ( ( H o. f ) |` ( 1 ... n ) )
201	200	fveq1i 5689	. . . . . . . . . . . . . . 15 |- ( ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) ` k ) = ( ( ( H o. f ) |` ( 1 ... n ) ) ` k )
202		fvres 5701	. . . . . . . . . . . . . . 15 |- ( k e. ( 1 ... n ) -> ( ( ( H o. f ) |` ( 1 ... n ) ) ` k ) = ( ( H o. f ) ` k ) )
203	201, 202	syl5eq 2485	. . . . . . . . . . . . . 14 |- ( k e. ( 1 ... n ) -> ( ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) ` k ) = ( ( H o. f ) ` k ) )
204	203	adantl 463	. . . . . . . . . . . . 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 ) )
205	105, 204	seqfveq 11826	. . . . . . . . . . . 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 ) )
206	195, 205	eqtr2d 2474	. . . . . . . . . . 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 ) ) ) ) )
207		fvex 5698	. . . . . . . . . . . 12 |- ( seq 1 ( .+ , ( H o. f ) ) ` n ) e. _V
208	207	elsnc 3898	. . . . . . . . . . 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 ) ) ) ) )
209	206, 208	sylibr 212	. . . . . . . . . 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 ) ) ) ) } )
210	6, 168	cntzi 15840	. . . . . . . . . 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 ) ) ) )
211	167, 209, 210	syl2anc 656	. . . . . . . . 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 ) ) ) )
212	211	eqcomd 2446	. . . . . . . 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 ) ) )
213	2, 6, 103, 116, 119, 122, 124, 212	mnd4g 15422	. . . . . . 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 ) ) ) ) )
214	51, 51, 54, 78, 82, 102, 213	seqcaopr3 11837	. . . . . 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 ) ) ) )
215	50, 55, 79, 87, 87, 90	off 6333	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F oF .+ H ) : A --> B )
216		gsumzaddlem.3	. . . . . . . 8 |- ( ph -> ran ( F oF .+ H ) C_ ( Z ` ran ( F oF .+ H ) ) )
217	216	adantr 462	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ran ( F oF .+ H ) C_ ( Z ` ran ( F oF .+ H ) ) )
218	47, 114	sylan 468	. . . . . . . . 9 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ ( k e. B /\ x e. B ) ) -> ( k .+ x ) e. B )
219	218, 55, 79, 87, 87, 90	off 6333	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F oF .+ H ) : A --> B )
220		eldifi 3475	. . . . . . . . . 10 |- ( x e. ( A \ ran f ) -> x e. A )
221		eqidd 2442	. . . . . . . . . . 11 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
222		eqidd 2442	. . . . . . . . . . 11 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. A ) -> ( H ` x ) = ( H ` x ) )
223	84, 86, 87, 87, 90, 221, 222	ofval 6328	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. A ) -> ( ( F oF .+ H ) ` x ) = ( ( F ` x ) .+ ( H ` x ) ) )
224	220, 223	sylan2 471	. . . . . . . . 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 ) ) )
225	18	adantr 462	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F supp .0. ) C_ ( ( F u. H ) supp .0. ) )
226		f1ofo 5645	. . . . . . . . . . . . . . . 16 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> f : ( 1 ... ( # ` W ) ) -onto-> W )
227		forn 5620	. . . . . . . . . . . . . . . 16 |- ( f : ( 1 ... ( # ` W ) ) -onto-> W -> ran f = W )
228	226, 227	syl 16	. . . . . . . . . . . . . . 15 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ran f = W )
229	228, 19	syl6eq 2489	. . . . . . . . . . . . . 14 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ran f = ( ( F u. H ) supp .0. ) )
230	229	sseq2d 3381	. . . . . . . . . . . . 13 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ( ( F supp .0. ) C_ ran f <-> ( F supp .0. ) C_ ( ( F u. H ) supp .0. ) ) )
231	230	ad2antll 723	. . . . . . . . . . . 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. ) ) )
232	225, 231	mpbird 232	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F supp .0. ) C_ ran f )
233	13	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> .0. e. _V )
234	55, 232, 87, 233	suppssr 6719	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( F ` x ) = .0. )
235	29	adantr 462	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H supp .0. ) C_ ( ( H u. F ) supp .0. ) )
236	235, 31	syl6sseqr 3400	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H supp .0. ) C_ ( ( F u. H ) supp .0. ) )
237	229	sseq2d 3381	. . . . . . . . . . . . 13 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ( ( H supp .0. ) C_ ran f <-> ( H supp .0. ) C_ ( ( F u. H ) supp .0. ) ) )
238	237	ad2antll 723	. . . . . . . . . . . 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. ) ) )
239	236, 238	mpbird 232	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H supp .0. ) C_ ran f )
240	79, 239, 87, 233	suppssr 6719	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( H ` x ) = .0. )
241	234, 240	oveq12d 6108	. . . . . . . . 9 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( ( F ` x ) .+ ( H ` x ) ) = ( .0. .+ .0. ) )
242	8	ad2antrr 720	. . . . . . . . 9 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( .0. .+ .0. ) = .0. )
243	224, 241, 242	3eqtrd 2477	. . . . . . . 8 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( ( F oF .+ H ) ` x ) = .0. )
244	219, 243	suppss 6718	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( ( F oF .+ H ) supp .0. ) C_ ran f )
245		ovex 6115	. . . . . . . . 9 |- ( F oF .+ H ) e. _V
246	245, 149	coex 6528	. . . . . . . 8 |- ( ( F oF .+ H ) o. f ) e. _V
247		suppimacnv 6700	. . . . . . . . 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. } ) ) )
248	247	eqcomd 2446	. . . . . . . 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. ) )
249	246, 13, 248	mp2an 667	. . . . . . 7 |- ( `' ( ( F oF .+ H ) o. f ) " ( _V \ { .0. } ) ) = ( ( ( F oF .+ H ) o. f ) supp .0. )
250	2, 3, 6, 168, 47, 87, 215, 217, 52, 73, 244, 249	gsumval3 16378	. . . . . 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 ) ) )
251		gsumzaddlem.1	. . . . . . . . 9 |- ( ph -> ran F C_ ( Z ` ran F ) )
252	251	adantr 462	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ran F C_ ( Z ` ran F ) )
253		eqid 2441	. . . . . . . 8 |- ( ( F o. f ) supp .0. ) = ( ( F o. f ) supp .0. )
254	2, 3, 6, 168, 47, 87, 55, 252, 52, 73, 232, 253	gsumval3 16378	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( G gsumg F ) = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) )
255	173	adantr 462	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ran H C_ ( Z ` ran H ) )
256		eqid 2441	. . . . . . . 8 |- ( ( H o. f ) supp .0. ) = ( ( H o. f ) supp .0. )
257	2, 3, 6, 168, 47, 87, 79, 255, 52, 73, 239, 256	gsumval3 16378	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( G gsumg H ) = ( seq 1 ( .+ , ( H o. f ) ) ` ( # ` W ) ) )
258	254, 257	oveq12d 6108	. . . . . 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 ) ) ) )
259	214, 250, 258	3eqtr4d 2483	. . . . 5 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )
260	259	expr 612	. . . 4 |- ( ( ph /\ ( # ` W ) e. NN ) -> ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) ) )
261	260	exlimdv 1695	. . 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 ) ) ) )
262	261	expimpd 600	. 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 ) ) ) )
263		gsumzadd.fn	. . . . 5 |- ( ph -> F finSupp .0. )
264		gsumzadd.hn	. . . . 5 |- ( ph -> H finSupp .0. )
265	263, 264	fsuppun 7635	. . . 4 |- ( ph -> ( ( F u. H ) supp .0. ) e. Fin )
266	19, 265	syl5eqel 2525	. . 3 |- ( ph -> W e. Fin )
267		fz1f1o 13183	. . 3 |- ( W e. Fin -> ( W = (/) \/ ( ( # ` W ) e. NN /\ E. f f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) )
268	266, 267	syl 16	. 2 |- ( ph -> ( W = (/) \/ ( ( # ` W ) e. NN /\ E. f f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) )
269	46, 262, 268	mpjaod 381	1 |- ( ph -> ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   A.wal 1362   = wceq 1364   E.wex 1591   e. wcel 1761   A.wral 2713   _Vcvv 2970   \ cdif 3322   u. cun 3323   i^i cin 3324   C_ wss 3325   (/)c0 3634   {csn 3874   class class class wbr 4289   e. cmpt 4347   `'ccnv 4835   dom cdm 4836   ran crn 4837   |` cres 4838   "cima 4839   o. ccom 4840   Fn wfn 5410   -->wf 5411   -1-1->wf1 5412   -onto->wfo 5413   -1-1-onto->wf1o 5414   ` cfv 5415  (class class class)co 6090   oFcof 6317   supp csupp 6689   Fincfn 7306   finSupp cfsupp 7616   1c1 9279   + caddc 9281   NNcn 10318   ZZ>=cuz 10857   ...cfz 11433  ..^cfzo 11544   seqcseq 11802   #chash 12099   Basecbs 14170   +g cplusg 14234   0gc0g 14374   gsum_g cgsu 14375   Mndcmnd 15405  Cntzccntz 15826

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-cnex 9334  ax-resscn 9335  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-addrcl 9339  ax-mulcl 9340  ax-mulrcl 9341  ax-mulcom 9342  ax-addass 9343  ax-mulass 9344  ax-distr 9345  ax-i2m1 9346  ax-1ne0 9347  ax-1rid 9348  ax-rnegex 9349  ax-rrecex 9350  ax-cnre 9351  ax-pre-lttri 9352  ax-pre-lttrn 9353  ax-pre-ltadd 9354  ax-pre-mulgt0 9355

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-reu 2720  df-rmo 2721  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-int 4126  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-se 4676  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-isom 5424  df-riota 6049  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-of 6319  df-om 6476  df-1st 6576  df-2nd 6577  df-supp 6690  df-recs 6828  df-rdg 6862  df-1o 6916  df-oadd 6920  df-er 7097  df-en 7307  df-dom 7308  df-sdom 7309  df-fin 7310  df-fsupp 7617  df-oi 7720  df-card 8105  df-pnf 9416  df-mnf 9417  df-xr 9418  df-ltxr 9419  df-le 9420  df-sub 9593  df-neg 9594  df-nn 10319  df-n0 10576  df-z 10643  df-uz 10858  df-fz 11434  df-fzo 11545  df-seq 11803  df-hash 12100  df-0g 14376  df-gsum 14377  df-mnd 15411  df-cntz 15828

This theorem is referenced by:  gsumzadd  16402  dprdfadd  16500