Theorem gsumzaddlem 16722

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 15749	. . . . . . 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 15751	. . . . . 6 |- ( ( G e. Mnd /\ .0. e. B ) -> ( .0. .+ .0. ) = .0. )
8	1, 5, 7	syl2anc 661	. . . . 5 |- ( ph -> ( .0. .+ .0. ) = .0. )
9	8	adantr 465	. . . 4 |- ( ( ph /\ W = (/) ) -> ( .0. .+ .0. ) = .0. )
10		gsumzaddlem.f	. . . . . . . 8 |- ( ph -> F : A --> B )
11		gsumzadd.a	. . . . . . . 8 |- ( ph -> A e. V )
12		fvex 5874	. . . . . . . . . 10 |- ( 0g ` G ) e. _V
13	3, 12	eqeltri 2551	. . . . . . . . 9 |- .0. e. _V
14	13	a1i 11	. . . . . . . 8 |- ( ph -> .0. e. _V )
15		gsumzaddlem.h	. . . . . . . . . . 11 |- ( ph -> H : A --> B )
16		fex 6131	. . . . . . . . . . 11 |- ( ( H : A --> B /\ A e. V ) -> H e. _V )
17	15, 11, 16	syl2anc 661	. . . . . . . . . 10 |- ( ph -> H e. _V )
18	17	suppun 6917	. . . . . . . . 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 3551	. . . . . . . 8 |- ( ph -> ( F supp .0. ) C_ W )
21	10, 11, 14, 20	gsumcllem 16700	. . . . . . 7 |- ( ( ph /\ W = (/) ) -> F = ( x e. A |-> .0. ) )
22	21	oveq2d 6298	. . . . . 6 |- ( ( ph /\ W = (/) ) -> ( G gsumg F ) = ( G gsumg ( x e. A |-> .0. ) ) )
23	3	gsumz 15821	. . . . . . . 8 |- ( ( G e. Mnd /\ A e. V ) -> ( G gsumg ( x e. A |-> .0. ) ) = .0. )
24	1, 11, 23	syl2anc 661	. . . . . . 7 |- ( ph -> ( G gsumg ( x e. A |-> .0. ) ) = .0. )
25	24	adantr 465	. . . . . 6 |- ( ( ph /\ W = (/) ) -> ( G gsumg ( x e. A |-> .0. ) ) = .0. )
26	22, 25	eqtrd 2508	. . . . 5 |- ( ( ph /\ W = (/) ) -> ( G gsumg F ) = .0. )
27		fex 6131	. . . . . . . . . . . 12 |- ( ( F : A --> B /\ A e. V ) -> F e. _V )
28	10, 11, 27	syl2anc 661	. . . . . . . . . . 11 |- ( ph -> F e. _V )
29	28	suppun 6917	. . . . . . . . . 10 |- ( ph -> ( H supp .0. ) C_ ( ( H u. F ) supp .0. ) )
30		uncom 3648	. . . . . . . . . . 11 |- ( F u. H ) = ( H u. F )
31	30	oveq1i 6292	. . . . . . . . . 10 |- ( ( F u. H ) supp .0. ) = ( ( H u. F ) supp .0. )
32	29, 31	syl6sseqr 3551	. . . . . . . . 9 |- ( ph -> ( H supp .0. ) C_ ( ( F u. H ) supp .0. ) )
33	32, 19	syl6sseqr 3551	. . . . . . . 8 |- ( ph -> ( H supp .0. ) C_ W )
34	15, 11, 14, 33	gsumcllem 16700	. . . . . . 7 |- ( ( ph /\ W = (/) ) -> H = ( x e. A |-> .0. ) )
35	34	oveq2d 6298	. . . . . 6 |- ( ( ph /\ W = (/) ) -> ( G gsumg H ) = ( G gsumg ( x e. A |-> .0. ) ) )
36	35, 25	eqtrd 2508	. . . . 5 |- ( ( ph /\ W = (/) ) -> ( G gsumg H ) = .0. )
37	26, 36	oveq12d 6300	. . . 4 |- ( ( ph /\ W = (/) ) -> ( ( G gsumg F ) .+ ( G gsumg H ) ) = ( .0. .+ .0. ) )
38	11	adantr 465	. . . . . . . 8 |- ( ( ph /\ W = (/) ) -> A e. V )
39	5	ad2antrr 725	. . . . . . . 8 |- ( ( ( ph /\ W = (/) ) /\ x e. A ) -> .0. e. B )
40	38, 39, 39, 21, 34	offval2 6538	. . . . . . 7 |- ( ( ph /\ W = (/) ) -> ( F oF .+ H ) = ( x e. A |-> ( .0. .+ .0. ) ) )
41	9	mpteq2dv 4534	. . . . . . 7 |- ( ( ph /\ W = (/) ) -> ( x e. A |-> ( .0. .+ .0. ) ) = ( x e. A |-> .0. ) )
42	40, 41	eqtrd 2508	. . . . . 6 |- ( ( ph /\ W = (/) ) -> ( F oF .+ H ) = ( x e. A |-> .0. ) )
43	42	oveq2d 6298	. . . . 5 |- ( ( ph /\ W = (/) ) -> ( G gsumg ( F oF .+ H ) ) = ( G gsumg ( x e. A |-> .0. ) ) )
44	43, 25	eqtrd 2508	. . . 4 |- ( ( ph /\ W = (/) ) -> ( G gsumg ( F oF .+ H ) ) = .0. )
45	9, 37, 44	3eqtr4rd 2519	. . 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 465	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> G e. Mnd )
48	2, 6	mndcl 15730	. . . . . . . . . 10 |- ( ( G e. Mnd /\ z e. B /\ w e. B ) -> ( z .+ w ) e. B )
49	48	3expb 1197	. . . . . . . . 9 |- ( ( G e. Mnd /\ ( z e. B /\ w e. B ) ) -> ( z .+ w ) e. B )
50	47, 49	sylan 471	. . . . . . . 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 6449	. . . . . . 7 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
52		simprl 755	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( # ` W ) e. NN )
53		nnuz 11113	. . . . . . . 8 |- NN = ( ZZ>= ` 1 )
54	52, 53	syl6eleq 2565	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( # ` W ) e. ( ZZ>= ` 1 ) )
55	10	adantr 465	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> F : A --> B )
56		f1of1 5813	. . . . . . . . . . . 12 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> f : ( 1 ... ( # ` W ) ) -1-1-> W )
57	56	ad2antll 728	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> f : ( 1 ... ( # ` W ) ) -1-1-> W )
58		suppssdm 6911	. . . . . . . . . . . . . 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 5207	. . . . . . . . . . . . . 14 |- dom ( F u. H ) = ( dom F u. dom H )
62		fdm 5733	. . . . . . . . . . . . . . . . 17 |- ( F : A --> B -> dom F = A )
63	10, 62	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> dom F = A )
64		fdm 5733	. . . . . . . . . . . . . . . . 17 |- ( H : A --> B -> dom H = A )
65	15, 64	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> dom H = A )
66	63, 65	uneq12d 3659	. . . . . . . . . . . . . . 15 |- ( ph -> ( dom F u. dom H ) = ( A u. A ) )
67		unidm 3647	. . . . . . . . . . . . . . 15 |- ( A u. A ) = A
68	66, 67	syl6eq 2524	. . . . . . . . . . . . . 14 |- ( ph -> ( dom F u. dom H ) = A )
69	61, 68	syl5req 2521	. . . . . . . . . . . . 13 |- ( ph -> A = dom ( F u. H ) )
70	59, 60, 69	3sstr4d 3547	. . . . . . . . . . . 12 |- ( ph -> W C_ A )
71	70	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> W C_ A )
72		f1ss 5784	. . . . . . . . . . 11 |- ( ( f : ( 1 ... ( # ` W ) ) -1-1-> W /\ W C_ A ) -> f : ( 1 ... ( # ` W ) ) -1-1-> A )
73	57, 71, 72	syl2anc 661	. . . . . . . . . 10 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> f : ( 1 ... ( # ` W ) ) -1-1-> A )
74		f1f 5779	. . . . . . . . . 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 5739	. . . . . . . . 9 |- ( ( F : A --> B /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( F o. f ) : ( 1 ... ( # ` W ) ) --> B )
77	55, 75, 76	syl2anc 661	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F o. f ) : ( 1 ... ( # ` W ) ) --> B )
78	77	ffvelrnda 6019	. . . . . . 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 465	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> H : A --> B )
80		fco 5739	. . . . . . . . 9 |- ( ( H : A --> B /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( H o. f ) : ( 1 ... ( # ` W ) ) --> B )
81	79, 75, 80	syl2anc 661	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H o. f ) : ( 1 ... ( # ` W ) ) --> B )
82	81	ffvelrnda 6019	. . . . . . 7 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( H o. f ) ` k ) e. B )
83		ffn 5729	. . . . . . . . . . . 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 5729	. . . . . . . . . . . 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 465	. . . . . . . . . . 11 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> A e. V )
88		ovex 6307	. . . . . . . . . . . 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 3707	. . . . . . . . . . 11 |- ( A i^i A ) = A
91	84, 86, 75, 87, 87, 89, 90	ofco 6542	. . . . . . . . . 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 5866	. . . . . . . . 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 465	. . . . . . . 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 5748	. . . . . . . . . 10 |- ( ( F Fn A /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( F o. f ) Fn ( 1 ... ( # ` W ) ) )
95	84, 75, 94	syl2anc 661	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F o. f ) Fn ( 1 ... ( # ` W ) ) )
96		fnfco 5748	. . . . . . . . . 10 |- ( ( H Fn A /\ f : ( 1 ... ( # ` W ) ) --> A ) -> ( H o. f ) Fn ( 1 ... ( # ` W ) ) )
97	86, 75, 96	syl2anc 661	. . . . . . . . 9 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H o. f ) Fn ( 1 ... ( # ` W ) ) )
98		inidm 3707	. . . . . . . . 9 |- ( ( 1 ... ( # ` W ) ) i^i ( 1 ... ( # ` W ) ) ) = ( 1 ... ( # ` W ) )
99		eqidd 2468	. . . . . . . . 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 2468	. . . . . . . . 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 6531	. . . . . . . 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 2508	. . . . . . 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 725	. . . . . . . 8 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> G e. Mnd )
104		elfzouz 11797	. . . . . . . . . 10 |- ( n e. ( 1..^ ( # ` W ) ) -> n e. ( ZZ>= ` 1 ) )
105	104	adantl 466	. . . . . . . . 9 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> n e. ( ZZ>= ` 1 ) )
106		elfzouz2 11806	. . . . . . . . . . . . 13 |- ( n e. ( 1..^ ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` n ) )
107	106	adantl 466	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( # ` W ) e. ( ZZ>= ` n ) )
108		fzss2 11719	. . . . . . . . . . . 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 3504	. . . . . . . . . 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 714	. . . . . . . . . 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 470	. . . . . . . . 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 15730	. . . . . . . . . . 11 |- ( ( G e. Mnd /\ k e. B /\ x e. B ) -> ( k .+ x ) e. B )
114	113	3expb 1197	. . . . . . . . . 10 |- ( ( G e. Mnd /\ ( k e. B /\ x e. B ) ) -> ( k .+ x ) e. B )
115	103, 114	sylan 471	. . . . . . . . 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 12090	. . . . . . . 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 714	. . . . . . . . . 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 470	. . . . . . . . 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 12090	. . . . . . . 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 11873	. . . . . . . . 9 |- ( n e. ( 1..^ ( # ` W ) ) -> ( n + 1 ) e. ( 1 ... ( # ` W ) ) )
121		ffvelrn 6017	. . . . . . . . 9 |- ( ( ( F o. f ) : ( 1 ... ( # ` W ) ) --> B /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. f ) ` ( n + 1 ) ) e. B )
122	77, 120, 121	syl2an 477	. . . . . . . 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 6017	. . . . . . . . 9 |- ( ( ( H o. f ) : ( 1 ... ( # ` W ) ) --> B /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( ( H o. f ) ` ( n + 1 ) ) e. B )
124	81, 120, 123	syl2an 477	. . . . . . . 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 5942	. . . . . . . . . . . 12 |- ( ( f : ( 1 ... ( # ` W ) ) --> A /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. f ) ` ( n + 1 ) ) = ( F ` ( f ` ( n + 1 ) ) ) )
126	75, 120, 125	syl2an 477	. . . . . . . . . . 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 6017	. . . . . . . . . . . . . 14 |- ( ( f : ( 1 ... ( # ` W ) ) --> A /\ ( n + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( f ` ( n + 1 ) ) e. A )
128	75, 120, 127	syl2an 477	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( f ` ( n + 1 ) ) e. A )
129		fzp1disj 11734	. . . . . . . . . . . . . . 15 |- ( ( 1 ... n ) i^i { ( n + 1 ) } ) = (/)
130		disjsn 4088	. . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( n + 1 ) e. ( 1 ... ( # ` W ) ) )
134		f1elima 6157	. . . . . . . . . . . . . . 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 1228	. . . . . . . . . . . . . 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 3487	. . . . . . . . . . . 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 615	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x C_ A ) -> ( k e. ( A \ x ) -> ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) ) )
140	139	ralrimiv 2876	. . . . . . . . . . . . . . . 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 1695	. . . . . . . . . . . . . 14 |- ( ph -> A. x ( x C_ A -> A. k e. ( A \ x ) ( F ` k ) e. ( Z ` { ( G gsumg ( H |` x ) ) } ) ) )
143	142	ad2antrr 725	. . . . . . . . . . . . 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 5346	. . . . . . . . . . . . . 14 |- ( f " ( 1 ... n ) ) C_ ran f
145	75	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> f : ( 1 ... ( # ` W ) ) --> A )
146		frn 5735	. . . . . . . . . . . . . . 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 3515	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ( f " ( 1 ... n ) ) C_ A )
149		vex 3116	. . . . . . . . . . . . . . 15 |- f e. _V
150		imaexg 6718	. . . . . . . . . . . . . . 15 |- ( f e. _V -> ( f " ( 1 ... n ) ) e. _V )
151	149, 150	ax-mp 5	. . . . . . . . . . . . . 14 |- ( f " ( 1 ... n ) ) e. _V
152		sseq1 3525	. . . . . . . . . . . . . . 15 |- ( x = ( f " ( 1 ... n ) ) -> ( x C_ A <-> ( f " ( 1 ... n ) ) C_ A ) )
153		difeq2 3616	. . . . . . . . . . . . . . . 16 |- ( x = ( f " ( 1 ... n ) ) -> ( A \ x ) = ( A \ ( f " ( 1 ... n ) ) ) )
154		reseq2 5266	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( f " ( 1 ... n ) ) -> ( H |` x ) = ( H |` ( f " ( 1 ... n ) ) ) )
155	154	oveq2d 6298	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( f " ( 1 ... n ) ) -> ( G gsumg ( H |` x ) ) = ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) )
156	155	sneqd 4039	. . . . . . . . . . . . . . . . . 18 |- ( x = ( f " ( 1 ... n ) ) -> { ( G gsumg ( H |` x ) ) } = { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } )
157	156	fveq2d 5868	. . . . . . . . . . . . . . . . 17 |- ( x = ( f " ( 1 ... n ) ) -> ( Z ` { ( G gsumg ( H |` x ) ) } ) = ( Z ` { ( G gsumg ( H |` ( f " ( 1 ... n ) ) ) ) } ) )
158	157	eleq2d 2537	. . . . . . . . . . . . . . . 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 3072	. . . . . . . . . . . . . . 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 3204	. . . . . . . . . . . . 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 5864	. . . . . . . . . . . . . 14 |- ( k = ( f ` ( n + 1 ) ) -> ( F ` k ) = ( F ` ( f ` ( n + 1 ) ) ) )
164	163	eleq1d 2536	. . . . . . . . . . . . 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 3210	. . . . . . . . . . . 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 2555	. . . . . . . . . 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 725	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> H : A --> B )
171		fssres 5749	. . . . . . . . . . . . . 14 |- ( ( H : A --> B /\ ( f " ( 1 ... n ) ) C_ A ) -> ( H |` ( f " ( 1 ... n ) ) ) : ( f " ( 1 ... n ) ) --> B )
172	170, 148, 171	syl2anc 661	. . . . . . . . . . . . 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 725	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> ran H C_ ( Z ` ran H ) )
175		resss 5295	. . . . . . . . . . . . . . 15 |- ( H |` ( f " ( 1 ... n ) ) ) C_ H
176		rnss 5229	. . . . . . . . . . . . . . 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 16167	. . . . . . . . . . . . . 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 662	. . . . . . . . . . . . 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 2566	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ n e. ( 1..^ ( # ` W ) ) ) -> n e. NN )
181		f1ores 5828	. . . . . . . . . . . . . . 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 661	. . . . . . . . . . . . . 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 5813	. . . . . . . . . . . . . 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 6911	. . . . . . . . . . . . . . 15 |- ( ( H |` ( f " ( 1 ... n ) ) ) supp .0. ) C_ dom ( H |` ( f " ( 1 ... n ) ) )
186		dmres 5292	. . . . . . . . . . . . . . . 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 3552	. . . . . . . . . . . . . 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 3718	. . . . . . . . . . . . . . 15 |- ( ( f " ( 1 ... n ) ) i^i dom H ) C_ ( f " ( 1 ... n ) )
190		df-ima 5012	. . . . . . . . . . . . . . . 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 3552	. . . . . . . . . . . . . 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 3514	. . . . . . . . . . . . 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 2467	. . . . . . . . . . . . 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 16699	. . . . . . . . . . . 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 3559	. . . . . . . . . . . . . . . . . 18 |- ran ( f |` ( 1 ... n ) ) C_ ( f " ( 1 ... n ) )
197		cores 5508	. . . . . . . . . . . . . . . . . 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 5509	. . . . . . . . . . . . . . . . 17 |- ( ( H o. f ) |` ( 1 ... n ) ) = ( H o. ( f |` ( 1 ... n ) ) )
200	198, 199	eqtr4i 2499	. . . . . . . . . . . . . . . 16 |- ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) = ( ( H o. f ) |` ( 1 ... n ) )
201	200	fveq1i 5865	. . . . . . . . . . . . . . 15 |- ( ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) ` k ) = ( ( ( H o. f ) |` ( 1 ... n ) ) ` k )
202		fvres 5878	. . . . . . . . . . . . . . 15 |- ( k e. ( 1 ... n ) -> ( ( ( H o. f ) |` ( 1 ... n ) ) ` k ) = ( ( H o. f ) ` k ) )
203	201, 202	syl5eq 2520	. . . . . . . . . . . . . 14 |- ( k e. ( 1 ... n ) -> ( ( ( H |` ( f " ( 1 ... n ) ) ) o. ( f |` ( 1 ... n ) ) ) ` k ) = ( ( H o. f ) ` k ) )
204	203	adantl 466	. . . . . . . . . . . . 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 12094	. . . . . . . . . . . 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 2509	. . . . . . . . . . 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 5874	. . . . . . . . . . . 12 |- ( seq 1 ( .+ , ( H o. f ) ) ` n ) e. _V
208	207	elsnc 4051	. . . . . . . . . . 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 16159	. . . . . . . . . 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 661	. . . . . . . . 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 2475	. . . . . . . 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 15736	. . . . . . 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 12105	. . . . . 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 6536	. . . . . . 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 465	. . . . . . 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 471	. . . . . . . . 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 6536	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F oF .+ H ) : A --> B )
220		eldifi 3626	. . . . . . . . . 10 |- ( x e. ( A \ ran f ) -> x e. A )
221		eqidd 2468	. . . . . . . . . . 11 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
222		eqidd 2468	. . . . . . . . . . 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 6531	. . . . . . . . . 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 474	. . . . . . . . 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 465	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( F supp .0. ) C_ ( ( F u. H ) supp .0. ) )
226		f1ofo 5821	. . . . . . . . . . . . . . . 16 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> f : ( 1 ... ( # ` W ) ) -onto-> W )
227		forn 5796	. . . . . . . . . . . . . . . 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 2524	. . . . . . . . . . . . . 14 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> ran f = ( ( F u. H ) supp .0. ) )
230	229	sseq2d 3532	. . . . . . . . . . . . 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 728	. . . . . . . . . . . 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 6928	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( F ` x ) = .0. )
235	29	adantr 465	. . . . . . . . . . . . 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 3551	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( H supp .0. ) C_ ( ( F u. H ) supp .0. ) )
237	229	sseq2d 3532	. . . . . . . . . . . . 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 728	. . . . . . . . . . . 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 6928	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( A \ ran f ) ) -> ( H ` x ) = .0. )
241	234, 240	oveq12d 6300	. . . . . . . . 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 725	. . . . . . . . 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 2512	. . . . . . . 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 6927	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( ( F oF .+ H ) supp .0. ) C_ ran f )
245		ovex 6307	. . . . . . . . 9 |- ( F oF .+ H ) e. _V
246	245, 149	coex 6733	. . . . . . . 8 |- ( ( F oF .+ H ) o. f ) e. _V
247		suppimacnv 6909	. . . . . . . . 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 2475	. . . . . . . 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 672	. . . . . . 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 16699	. . . . . 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 465	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ran F C_ ( Z ` ran F ) )
253		eqid 2467	. . . . . . . 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 16699	. . . . . . 7 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( G gsumg F ) = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) )
255	173	adantr 465	. . . . . . . 8 |- ( ( ph /\ ( ( # ` W ) e. NN /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ran H C_ ( Z ` ran H ) )
256		eqid 2467	. . . . . . . 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 16699	. . . . . . 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 6300	. . . . . 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 2518	. . . . 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 615	. . . 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 1700	. . 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 603	. 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 7844	. . . 4 |- ( ph -> ( ( F u. H ) supp .0. ) e. Fin )
266	19, 265	syl5eqel 2559	. . 3 |- ( ph -> W e. Fin )
267		fz1f1o 13488	. . 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 1377   = wceq 1379   E.wex 1596   e. wcel 1767   A.wral 2814   _Vcvv 3113   \ cdif 3473   u. cun 3474   i^i cin 3475   C_ wss 3476   (/)c0 3785   {csn 4027   class class class wbr 4447   |-> cmpt 4505   `'ccnv 4998   dom cdm 4999   ran crn 5000   |` cres 5001   "cima 5002   o. ccom 5003   Fn wfn 5581   -->wf 5582   -1-1->wf1 5583   -onto->wfo 5584   -1-1-onto->wf1o 5585   ` cfv 5586  (class class class)co 6282   oFcof 6520   supp csupp 6898   Fincfn 7513   finSupp cfsupp 7825   1c1 9489   + caddc 9491   NNcn 10532   ZZ>=cuz 11078   ...cfz 11668  ..^cfzo 11788   seqcseq 12070   #chash 12367   Basecbs 14483   +g cplusg 14548   0gc0g 14688   gsum_g cgsu 14689   Mndcmnd 15719  Cntzccntz 16145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-cnex 9544  ax-resscn 9545  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-addrcl 9549  ax-mulcl 9550  ax-mulrcl 9551  ax-mulcom 9552  ax-addass 9553  ax-mulass 9554  ax-distr 9555  ax-i2m1 9556  ax-1ne0 9557  ax-1rid 9558  ax-rnegex 9559  ax-rrecex 9560  ax-cnre 9561  ax-pre-lttri 9562  ax-pre-lttrn 9563  ax-pre-ltadd 9564  ax-pre-mulgt0 9565

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-isom 5595  df-riota 6243  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-of 6522  df-om 6679  df-1st 6781  df-2nd 6782  df-supp 6899  df-recs 7039  df-rdg 7073  df-1o 7127  df-oadd 7131  df-er 7308  df-en 7514  df-dom 7515  df-sdom 7516  df-fin 7517  df-fsupp 7826  df-oi 7931  df-card 8316  df-pnf 9626  df-mnf 9627  df-xr 9628  df-ltxr 9629  df-le 9630  df-sub 9803  df-neg 9804  df-nn 10533  df-n0 10792  df-z 10861  df-uz 11079  df-fz 11669  df-fzo 11789  df-seq 12071  df-hash 12368  df-0g 14690  df-gsum 14691  df-mnd 15725  df-cntz 16147

This theorem is referenced by:  gsumzadd  16723  dprdfadd  16847