Theorem gsumval3 18308

Description: Value of the group sum operation over an arbitrary finite set. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 31-May-2019.)

Hypotheses

Ref	Expression
gsumval3.b	|- B = ( Base ` G )
gsumval3.0	|- .0. = ( 0g ` G )
gsumval3.p	|- .+ = ( +g ` G )
gsumval3.z	|- Z = (Cntz ` G )
gsumval3.g	|- ( ph -> G e. Mnd )
gsumval3.a	|- ( ph -> A e. V )
gsumval3.f	|- ( ph -> F : A --> B )
gsumval3.c	|- ( ph -> ran F C_ ( Z ` ran F ) )
gsumval3.m	|- ( ph -> M e. NN )
gsumval3.h	|- ( ph -> H : ( 1 ... M ) -1-1-> A )
gsumval3.n	|- ( ph -> ( F supp .0. ) C_ ran H )
gsumval3.w	|- W = ( ( F o. H ) supp .0. )

Assertion

Ref	Expression
gsumval3	|- ( ph -> ( G gsumg F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) )

Proof of Theorem gsumval3

Dummy variables f k m n x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gsumval3.g	. . . . 5 |- ( ph -> G e. Mnd )
2		gsumval3.a	. . . . 5 |- ( ph -> A e. V )
3		gsumval3.0	. . . . . 6 |- .0. = ( 0g ` G )
4	3	gsumz 17374	. . . . 5 |- ( ( G e. Mnd /\ A e. V ) -> ( G gsumg ( x e. A |-> .0. ) ) = .0. )
5	1, 2, 4	syl2anc 693	. . . 4 |- ( ph -> ( G gsumg ( x e. A |-> .0. ) ) = .0. )
6	5	adantr 481	. . 3 |- ( ( ph /\ W = (/) ) -> ( G gsumg ( x e. A |-> .0. ) ) = .0. )
7		gsumval3.f	. . . . . . 7 |- ( ph -> F : A --> B )
8	7	feqmptd 6249	. . . . . 6 |- ( ph -> F = ( x e. A |-> ( F ` x ) ) )
9	8	adantr 481	. . . . 5 |- ( ( ph /\ W = (/) ) -> F = ( x e. A |-> ( F ` x ) ) )
10		gsumval3.h	. . . . . . . . . . . . . 14 |- ( ph -> H : ( 1 ... M ) -1-1-> A )
11		f1f 6101	. . . . . . . . . . . . . 14 |- ( H : ( 1 ... M ) -1-1-> A -> H : ( 1 ... M ) --> A )
12	10, 11	syl 17	. . . . . . . . . . . . 13 |- ( ph -> H : ( 1 ... M ) --> A )
13	12	ad2antrr 762	. . . . . . . . . . . 12 |- ( ( ( ph /\ W = (/) ) /\ x e. ran H ) -> H : ( 1 ... M ) --> A )
14		f1f1orn 6148	. . . . . . . . . . . . . . . 16 |- ( H : ( 1 ... M ) -1-1-> A -> H : ( 1 ... M ) -1-1-onto-> ran H )
15	10, 14	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> H : ( 1 ... M ) -1-1-onto-> ran H )
16	15	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ W = (/) ) -> H : ( 1 ... M ) -1-1-onto-> ran H )
17		f1ocnv 6149	. . . . . . . . . . . . . 14 |- ( H : ( 1 ... M ) -1-1-onto-> ran H -> `' H : ran H -1-1-onto-> ( 1 ... M ) )
18		f1of 6137	. . . . . . . . . . . . . 14 |- ( `' H : ran H -1-1-onto-> ( 1 ... M ) -> `' H : ran H --> ( 1 ... M ) )
19	16, 17, 18	3syl 18	. . . . . . . . . . . . 13 |- ( ( ph /\ W = (/) ) -> `' H : ran H --> ( 1 ... M ) )
20	19	ffvelrnda 6359	. . . . . . . . . . . 12 |- ( ( ( ph /\ W = (/) ) /\ x e. ran H ) -> ( `' H ` x ) e. ( 1 ... M ) )
21		fvco3 6275	. . . . . . . . . . . 12 |- ( ( H : ( 1 ... M ) --> A /\ ( `' H ` x ) e. ( 1 ... M ) ) -> ( ( F o. H ) ` ( `' H ` x ) ) = ( F ` ( H ` ( `' H ` x ) ) ) )
22	13, 20, 21	syl2anc 693	. . . . . . . . . . 11 |- ( ( ( ph /\ W = (/) ) /\ x e. ran H ) -> ( ( F o. H ) ` ( `' H ` x ) ) = ( F ` ( H ` ( `' H ` x ) ) ) )
23		simpr 477	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ W = (/) ) -> W = (/) )
24	23	difeq2d 3728	. . . . . . . . . . . . . . 15 |- ( ( ph /\ W = (/) ) -> ( ( 1 ... M ) \ W ) = ( ( 1 ... M ) \ (/) ) )
25		dif0 3950	. . . . . . . . . . . . . . 15 |- ( ( 1 ... M ) \ (/) ) = ( 1 ... M )
26	24, 25	syl6eq 2672	. . . . . . . . . . . . . 14 |- ( ( ph /\ W = (/) ) -> ( ( 1 ... M ) \ W ) = ( 1 ... M ) )
27	26	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( ph /\ W = (/) ) /\ x e. ran H ) -> ( ( 1 ... M ) \ W ) = ( 1 ... M ) )
28	20, 27	eleqtrrd 2704	. . . . . . . . . . . 12 |- ( ( ( ph /\ W = (/) ) /\ x e. ran H ) -> ( `' H ` x ) e. ( ( 1 ... M ) \ W ) )
29		fco 6058	. . . . . . . . . . . . . . 15 |- ( ( F : A --> B /\ H : ( 1 ... M ) --> A ) -> ( F o. H ) : ( 1 ... M ) --> B )
30	7, 12, 29	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ph -> ( F o. H ) : ( 1 ... M ) --> B )
31	30	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ W = (/) ) -> ( F o. H ) : ( 1 ... M ) --> B )
32		gsumval3.w	. . . . . . . . . . . . . . 15 |- W = ( ( F o. H ) supp .0. )
33	32	eqimss2i 3660	. . . . . . . . . . . . . 14 |- ( ( F o. H ) supp .0. ) C_ W
34	33	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ W = (/) ) -> ( ( F o. H ) supp .0. ) C_ W )
35		ovexd 6680	. . . . . . . . . . . . 13 |- ( ( ph /\ W = (/) ) -> ( 1 ... M ) e. _V )
36		fvex 6201	. . . . . . . . . . . . . . 15 |- ( 0g ` G ) e. _V
37	3, 36	eqeltri 2697	. . . . . . . . . . . . . 14 |- .0. e. _V
38	37	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ W = (/) ) -> .0. e. _V )
39	31, 34, 35, 38	suppssr 7326	. . . . . . . . . . . 12 |- ( ( ( ph /\ W = (/) ) /\ ( `' H ` x ) e. ( ( 1 ... M ) \ W ) ) -> ( ( F o. H ) ` ( `' H ` x ) ) = .0. )
40	28, 39	syldan 487	. . . . . . . . . . 11 |- ( ( ( ph /\ W = (/) ) /\ x e. ran H ) -> ( ( F o. H ) ` ( `' H ` x ) ) = .0. )
41		f1ocnvfv2 6533	. . . . . . . . . . . . 13 |- ( ( H : ( 1 ... M ) -1-1-onto-> ran H /\ x e. ran H ) -> ( H ` ( `' H ` x ) ) = x )
42	16, 41	sylan 488	. . . . . . . . . . . 12 |- ( ( ( ph /\ W = (/) ) /\ x e. ran H ) -> ( H ` ( `' H ` x ) ) = x )
43	42	fveq2d 6195	. . . . . . . . . . 11 |- ( ( ( ph /\ W = (/) ) /\ x e. ran H ) -> ( F ` ( H ` ( `' H ` x ) ) ) = ( F ` x ) )
44	22, 40, 43	3eqtr3rd 2665	. . . . . . . . . 10 |- ( ( ( ph /\ W = (/) ) /\ x e. ran H ) -> ( F ` x ) = .0. )
45		fvex 6201	. . . . . . . . . . 11 |- ( F ` x ) e. _V
46	45	elsn 4192	. . . . . . . . . 10 |- ( ( F ` x ) e. { .0. } <-> ( F ` x ) = .0. )
47	44, 46	sylibr 224	. . . . . . . . 9 |- ( ( ( ph /\ W = (/) ) /\ x e. ran H ) -> ( F ` x ) e. { .0. } )
48	47	adantlr 751	. . . . . . . 8 |- ( ( ( ( ph /\ W = (/) ) /\ x e. A ) /\ x e. ran H ) -> ( F ` x ) e. { .0. } )
49		eldif 3584	. . . . . . . . . . 11 |- ( x e. ( A \ ran H ) <-> ( x e. A /\ -. x e. ran H ) )
50		gsumval3.n	. . . . . . . . . . . . 13 |- ( ph -> ( F supp .0. ) C_ ran H )
51	37	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> .0. e. _V )
52	7, 50, 2, 51	suppssr 7326	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( A \ ran H ) ) -> ( F ` x ) = .0. )
53	52, 46	sylibr 224	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( A \ ran H ) ) -> ( F ` x ) e. { .0. } )
54	49, 53	sylan2br 493	. . . . . . . . . 10 |- ( ( ph /\ ( x e. A /\ -. x e. ran H ) ) -> ( F ` x ) e. { .0. } )
55	54	adantlr 751	. . . . . . . . 9 |- ( ( ( ph /\ W = (/) ) /\ ( x e. A /\ -. x e. ran H ) ) -> ( F ` x ) e. { .0. } )
56	55	anassrs 680	. . . . . . . 8 |- ( ( ( ( ph /\ W = (/) ) /\ x e. A ) /\ -. x e. ran H ) -> ( F ` x ) e. { .0. } )
57	48, 56	pm2.61dan 832	. . . . . . 7 |- ( ( ( ph /\ W = (/) ) /\ x e. A ) -> ( F ` x ) e. { .0. } )
58	57, 46	sylib 208	. . . . . 6 |- ( ( ( ph /\ W = (/) ) /\ x e. A ) -> ( F ` x ) = .0. )
59	58	mpteq2dva 4744	. . . . 5 |- ( ( ph /\ W = (/) ) -> ( x e. A |-> ( F ` x ) ) = ( x e. A |-> .0. ) )
60	9, 59	eqtrd 2656	. . . 4 |- ( ( ph /\ W = (/) ) -> F = ( x e. A |-> .0. ) )
61	60	oveq2d 6666	. . 3 |- ( ( ph /\ W = (/) ) -> ( G gsumg F ) = ( G gsumg ( x e. A |-> .0. ) ) )
62		gsumval3.b	. . . . . . . 8 |- B = ( Base ` G )
63	62, 3	mndidcl 17308	. . . . . . 7 |- ( G e. Mnd -> .0. e. B )
64	1, 63	syl 17	. . . . . 6 |- ( ph -> .0. e. B )
65		gsumval3.p	. . . . . . 7 |- .+ = ( +g ` G )
66	62, 65, 3	mndlid 17311	. . . . . 6 |- ( ( G e. Mnd /\ .0. e. B ) -> ( .0. .+ .0. ) = .0. )
67	1, 64, 66	syl2anc 693	. . . . 5 |- ( ph -> ( .0. .+ .0. ) = .0. )
68	67	adantr 481	. . . 4 |- ( ( ph /\ W = (/) ) -> ( .0. .+ .0. ) = .0. )
69		gsumval3.m	. . . . . 6 |- ( ph -> M e. NN )
70		nnuz 11723	. . . . . 6 |- NN = ( ZZ>= ` 1 )
71	69, 70	syl6eleq 2711	. . . . 5 |- ( ph -> M e. ( ZZ>= ` 1 ) )
72	71	adantr 481	. . . 4 |- ( ( ph /\ W = (/) ) -> M e. ( ZZ>= ` 1 ) )
73	26	eleq2d 2687	. . . . . 6 |- ( ( ph /\ W = (/) ) -> ( x e. ( ( 1 ... M ) \ W ) <-> x e. ( 1 ... M ) ) )
74	73	biimpar 502	. . . . 5 |- ( ( ( ph /\ W = (/) ) /\ x e. ( 1 ... M ) ) -> x e. ( ( 1 ... M ) \ W ) )
75	31, 34, 35, 38	suppssr 7326	. . . . 5 |- ( ( ( ph /\ W = (/) ) /\ x e. ( ( 1 ... M ) \ W ) ) -> ( ( F o. H ) ` x ) = .0. )
76	74, 75	syldan 487	. . . 4 |- ( ( ( ph /\ W = (/) ) /\ x e. ( 1 ... M ) ) -> ( ( F o. H ) ` x ) = .0. )
77	68, 72, 76	seqid3 12845	. . 3 |- ( ( ph /\ W = (/) ) -> ( seq 1 ( .+ , ( F o. H ) ) ` M ) = .0. )
78	6, 61, 77	3eqtr4d 2666	. 2 |- ( ( ph /\ W = (/) ) -> ( G gsumg F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) )
79		fzf 12330	. . . . 5 |- ... : ( ZZ X. ZZ ) --> ~P ZZ
80		ffn 6045	. . . . 5 |- ( ... : ( ZZ X. ZZ ) --> ~P ZZ -> ... Fn ( ZZ X. ZZ ) )
81		ovelrn 6810	. . . . 5 |- ( ... Fn ( ZZ X. ZZ ) -> ( A e. ran ... <-> E. m e. ZZ E. n e. ZZ A = ( m ... n ) ) )
82	79, 80, 81	mp2b 10	. . . 4 |- ( A e. ran ... <-> E. m e. ZZ E. n e. ZZ A = ( m ... n ) )
83	1	ad2antrr 762	. . . . . . . . 9 |- ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> G e. Mnd )
84		simpr 477	. . . . . . . . . . 11 |- ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> A = ( m ... n ) )
85		frel 6050	. . . . . . . . . . . . . . . . 17 |- ( F : A --> B -> Rel F )
86		reldm0 5343	. . . . . . . . . . . . . . . . 17 |- ( Rel F -> ( F = (/) <-> dom F = (/) ) )
87	7, 85, 86	3syl 18	. . . . . . . . . . . . . . . 16 |- ( ph -> ( F = (/) <-> dom F = (/) ) )
88		fdm 6051	. . . . . . . . . . . . . . . . . 18 |- ( F : A --> B -> dom F = A )
89	7, 88	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ph -> dom F = A )
90	89	eqeq1d 2624	. . . . . . . . . . . . . . . 16 |- ( ph -> ( dom F = (/) <-> A = (/) ) )
91	87, 90	bitrd 268	. . . . . . . . . . . . . . 15 |- ( ph -> ( F = (/) <-> A = (/) ) )
92		coeq1 5279	. . . . . . . . . . . . . . . . . . 19 |- ( F = (/) -> ( F o. H ) = ( (/) o. H ) )
93		co01 5650	. . . . . . . . . . . . . . . . . . 19 |- ( (/) o. H ) = (/)
94	92, 93	syl6eq 2672	. . . . . . . . . . . . . . . . . 18 |- ( F = (/) -> ( F o. H ) = (/) )
95	94	oveq1d 6665	. . . . . . . . . . . . . . . . 17 |- ( F = (/) -> ( ( F o. H ) supp .0. ) = ( (/) supp .0. ) )
96		supp0 7300	. . . . . . . . . . . . . . . . . 18 |- ( .0. e. _V -> ( (/) supp .0. ) = (/) )
97	37, 96	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( (/) supp .0. ) = (/)
98	95, 97	syl6eq 2672	. . . . . . . . . . . . . . . 16 |- ( F = (/) -> ( ( F o. H ) supp .0. ) = (/) )
99	32, 98	syl5eq 2668	. . . . . . . . . . . . . . 15 |- ( F = (/) -> W = (/) )
100	91, 99	syl6bir 244	. . . . . . . . . . . . . 14 |- ( ph -> ( A = (/) -> W = (/) ) )
101	100	necon3d 2815	. . . . . . . . . . . . 13 |- ( ph -> ( W =/= (/) -> A =/= (/) ) )
102	101	imp 445	. . . . . . . . . . . 12 |- ( ( ph /\ W =/= (/) ) -> A =/= (/) )
103	102	adantr 481	. . . . . . . . . . 11 |- ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> A =/= (/) )
104	84, 103	eqnetrrd 2862	. . . . . . . . . 10 |- ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ( m ... n ) =/= (/) )
105		fzn0 12355	. . . . . . . . . 10 |- ( ( m ... n ) =/= (/) <-> n e. ( ZZ>= ` m ) )
106	104, 105	sylib 208	. . . . . . . . 9 |- ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> n e. ( ZZ>= ` m ) )
107	7	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> F : A --> B )
108	84	feq2d 6031	. . . . . . . . . 10 |- ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ( F : A --> B <-> F : ( m ... n ) --> B ) )
109	107, 108	mpbid 222	. . . . . . . . 9 |- ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> F : ( m ... n ) --> B )
110	62, 65, 83, 106, 109	gsumval2 17280	. . . . . . . 8 |- ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ( G gsumg F ) = ( seq m ( .+ , F ) ` n ) )
111		frn 6053	. . . . . . . . . . . . . . 15 |- ( H : ( 1 ... M ) --> A -> ran H C_ A )
112	10, 11, 111	3syl 18	. . . . . . . . . . . . . 14 |- ( ph -> ran H C_ A )
113	112	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ran H C_ A )
114	113, 84	sseqtrd 3641	. . . . . . . . . . . 12 |- ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ran H C_ ( m ... n ) )
115		fzssuz 12382	. . . . . . . . . . . . 13 |- ( m ... n ) C_ ( ZZ>= ` m )
116		uzssz 11707	. . . . . . . . . . . . . 14 |- ( ZZ>= ` m ) C_ ZZ
117		zssre 11384	. . . . . . . . . . . . . 14 |- ZZ C_ RR
118	116, 117	sstri 3612	. . . . . . . . . . . . 13 |- ( ZZ>= ` m ) C_ RR
119	115, 118	sstri 3612	. . . . . . . . . . . 12 |- ( m ... n ) C_ RR
120	114, 119	syl6ss 3615	. . . . . . . . . . 11 |- ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ran H C_ RR )
121		ltso 10118	. . . . . . . . . . 11 |- < Or RR
122		soss 5053	. . . . . . . . . . 11 |- ( ran H C_ RR -> ( < Or RR -> < Or ran H ) )
123	120, 121, 122	mpisyl 21	. . . . . . . . . 10 |- ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> < Or ran H )
124		fzfi 12771	. . . . . . . . . . . 12 |- ( 1 ... M ) e. Fin
125	124	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1 ... M ) e. Fin )
126		fex2 7121	. . . . . . . . . . . . . . 15 |- ( ( H : ( 1 ... M ) --> A /\ ( 1 ... M ) e. Fin /\ A e. V ) -> H e. _V )
127	12, 125, 2, 126	syl3anc 1326	. . . . . . . . . . . . . 14 |- ( ph -> H e. _V )
128		f1oen3g 7971	. . . . . . . . . . . . . 14 |- ( ( H e. _V /\ H : ( 1 ... M ) -1-1-onto-> ran H ) -> ( 1 ... M ) ~~ ran H )
129	127, 15, 128	syl2anc 693	. . . . . . . . . . . . 13 |- ( ph -> ( 1 ... M ) ~~ ran H )
130		enfi 8176	. . . . . . . . . . . . 13 |- ( ( 1 ... M ) ~~ ran H -> ( ( 1 ... M ) e. Fin <-> ran H e. Fin ) )
131	129, 130	syl 17	. . . . . . . . . . . 12 |- ( ph -> ( ( 1 ... M ) e. Fin <-> ran H e. Fin ) )
132	124, 131	mpbii 223	. . . . . . . . . . 11 |- ( ph -> ran H e. Fin )
133	132	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ran H e. Fin )
134		fz1iso 13246	. . . . . . . . . 10 |- ( ( < Or ran H /\ ran H e. Fin ) -> E. f f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) )
135	123, 133, 134	syl2anc 693	. . . . . . . . 9 |- ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> E. f f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) )
136	69	nnnn0d 11351	. . . . . . . . . . . . . . . 16 |- ( ph -> M e. NN0 )
137		hashfz1 13134	. . . . . . . . . . . . . . . 16 |- ( M e. NN0 -> ( # ` ( 1 ... M ) ) = M )
138	136, 137	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> ( # ` ( 1 ... M ) ) = M )
139		hashen 13135	. . . . . . . . . . . . . . . . 17 |- ( ( ( 1 ... M ) e. Fin /\ ran H e. Fin ) -> ( ( # ` ( 1 ... M ) ) = ( # ` ran H ) <-> ( 1 ... M ) ~~ ran H ) )
140	124, 132, 139	sylancr 695	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( # ` ( 1 ... M ) ) = ( # ` ran H ) <-> ( 1 ... M ) ~~ ran H ) )
141	129, 140	mpbird 247	. . . . . . . . . . . . . . 15 |- ( ph -> ( # ` ( 1 ... M ) ) = ( # ` ran H ) )
142	138, 141	eqtr3d 2658	. . . . . . . . . . . . . 14 |- ( ph -> M = ( # ` ran H ) )
143	142	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> M = ( # ` ran H ) )
144	143	fveq2d 6195	. . . . . . . . . . . 12 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( seq 1 ( .+ , ( F o. f ) ) ` M ) = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` ran H ) ) )
145	1	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> G e. Mnd )
146	62, 65	mndcl 17301	. . . . . . . . . . . . . . 15 |- ( ( G e. Mnd /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
147	146	3expb 1266	. . . . . . . . . . . . . 14 |- ( ( G e. Mnd /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
148	145, 147	sylan 488	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
149		gsumval3.c	. . . . . . . . . . . . . . . . 17 |- ( ph -> ran F C_ ( Z ` ran F ) )
150	149	ad2antrr 762	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ran F C_ ( Z ` ran F ) )
151	150	sselda 3603	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ran F ) -> x e. ( Z ` ran F ) )
152		gsumval3.z	. . . . . . . . . . . . . . . 16 |- Z = (Cntz ` G )
153	65, 152	cntzi 17762	. . . . . . . . . . . . . . 15 |- ( ( x e. ( Z ` ran F ) /\ y e. ran F ) -> ( x .+ y ) = ( y .+ x ) )
154	151, 153	sylan 488	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ran F ) /\ y e. ran F ) -> ( x .+ y ) = ( y .+ x ) )
155	154	anasss 679	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ ( x e. ran F /\ y e. ran F ) ) -> ( x .+ y ) = ( y .+ x ) )
156	62, 65	mndass 17302	. . . . . . . . . . . . . 14 |- ( ( G e. Mnd /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
157	145, 156	sylan 488	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
158	71	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> M e. ( ZZ>= ` 1 ) )
159	7	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> F : A --> B )
160		frn 6053	. . . . . . . . . . . . . 14 |- ( F : A --> B -> ran F C_ B )
161	159, 160	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ran F C_ B )
162		simprr 796	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) )
163		isof1o 6573	. . . . . . . . . . . . . . . . 17 |- ( f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) -> f : ( 1 ... ( # ` ran H ) ) -1-1-onto-> ran H )
164	162, 163	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> f : ( 1 ... ( # ` ran H ) ) -1-1-onto-> ran H )
165	143	oveq2d 6666	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( 1 ... M ) = ( 1 ... ( # ` ran H ) ) )
166		f1oeq2 6128	. . . . . . . . . . . . . . . . 17 |- ( ( 1 ... M ) = ( 1 ... ( # ` ran H ) ) -> ( f : ( 1 ... M ) -1-1-onto-> ran H <-> f : ( 1 ... ( # ` ran H ) ) -1-1-onto-> ran H ) )
167	165, 166	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( f : ( 1 ... M ) -1-1-onto-> ran H <-> f : ( 1 ... ( # ` ran H ) ) -1-1-onto-> ran H ) )
168	164, 167	mpbird 247	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> f : ( 1 ... M ) -1-1-onto-> ran H )
169		f1ocnv 6149	. . . . . . . . . . . . . . 15 |- ( f : ( 1 ... M ) -1-1-onto-> ran H -> `' f : ran H -1-1-onto-> ( 1 ... M ) )
170	168, 169	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> `' f : ran H -1-1-onto-> ( 1 ... M ) )
171	15	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> H : ( 1 ... M ) -1-1-onto-> ran H )
172		f1oco 6159	. . . . . . . . . . . . . 14 |- ( ( `' f : ran H -1-1-onto-> ( 1 ... M ) /\ H : ( 1 ... M ) -1-1-onto-> ran H ) -> ( `' f o. H ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
173	170, 171, 172	syl2anc 693	. . . . . . . . . . . . 13 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( `' f o. H ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
174		ffn 6045	. . . . . . . . . . . . . . . . 17 |- ( F : A --> B -> F Fn A )
175		dffn4 6121	. . . . . . . . . . . . . . . . 17 |- ( F Fn A <-> F : A -onto-> ran F )
176	174, 175	sylib 208	. . . . . . . . . . . . . . . 16 |- ( F : A --> B -> F : A -onto-> ran F )
177		fof 6115	. . . . . . . . . . . . . . . 16 |- ( F : A -onto-> ran F -> F : A --> ran F )
178	159, 176, 177	3syl 18	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> F : A --> ran F )
179		f1of 6137	. . . . . . . . . . . . . . . . 17 |- ( f : ( 1 ... M ) -1-1-onto-> ran H -> f : ( 1 ... M ) --> ran H )
180	168, 179	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> f : ( 1 ... M ) --> ran H )
181	112	ad2antrr 762	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ran H C_ A )
182	180, 181	fssd 6057	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> f : ( 1 ... M ) --> A )
183		fco 6058	. . . . . . . . . . . . . . 15 |- ( ( F : A --> ran F /\ f : ( 1 ... M ) --> A ) -> ( F o. f ) : ( 1 ... M ) --> ran F )
184	178, 182, 183	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( F o. f ) : ( 1 ... M ) --> ran F )
185	184	ffvelrnda 6359	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ( 1 ... M ) ) -> ( ( F o. f ) ` x ) e. ran F )
186		f1ococnv2 6163	. . . . . . . . . . . . . . . . . . . . . 22 |- ( f : ( 1 ... M ) -1-1-onto-> ran H -> ( f o. `' f ) = ( _I |` ran H ) )
187	168, 186	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( f o. `' f ) = ( _I |` ran H ) )
188	187	coeq1d 5283	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( ( f o. `' f ) o. H ) = ( ( _I |` ran H ) o. H ) )
189		f1of 6137	. . . . . . . . . . . . . . . . . . . . 21 |- ( H : ( 1 ... M ) -1-1-onto-> ran H -> H : ( 1 ... M ) --> ran H )
190		fcoi2 6079	. . . . . . . . . . . . . . . . . . . . 21 |- ( H : ( 1 ... M ) --> ran H -> ( ( _I |` ran H ) o. H ) = H )
191	171, 189, 190	3syl 18	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( ( _I |` ran H ) o. H ) = H )
192	188, 191	eqtr2d 2657	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> H = ( ( f o. `' f ) o. H ) )
193		coass 5654	. . . . . . . . . . . . . . . . . . 19 |- ( ( f o. `' f ) o. H ) = ( f o. ( `' f o. H ) )
194	192, 193	syl6eq 2672	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> H = ( f o. ( `' f o. H ) ) )
195	194	coeq2d 5284	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( F o. H ) = ( F o. ( f o. ( `' f o. H ) ) ) )
196		coass 5654	. . . . . . . . . . . . . . . . 17 |- ( ( F o. f ) o. ( `' f o. H ) ) = ( F o. ( f o. ( `' f o. H ) ) )
197	195, 196	syl6eqr 2674	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( F o. H ) = ( ( F o. f ) o. ( `' f o. H ) ) )
198	197	fveq1d 6193	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( ( F o. H ) ` k ) = ( ( ( F o. f ) o. ( `' f o. H ) ) ` k ) )
199	198	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ k e. ( 1 ... M ) ) -> ( ( F o. H ) ` k ) = ( ( ( F o. f ) o. ( `' f o. H ) ) ` k ) )
200		f1of 6137	. . . . . . . . . . . . . . . . 17 |- ( `' f : ran H -1-1-onto-> ( 1 ... M ) -> `' f : ran H --> ( 1 ... M ) )
201	168, 169, 200	3syl 18	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> `' f : ran H --> ( 1 ... M ) )
202	171, 189	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> H : ( 1 ... M ) --> ran H )
203		fco 6058	. . . . . . . . . . . . . . . 16 |- ( ( `' f : ran H --> ( 1 ... M ) /\ H : ( 1 ... M ) --> ran H ) -> ( `' f o. H ) : ( 1 ... M ) --> ( 1 ... M ) )
204	201, 202, 203	syl2anc 693	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( `' f o. H ) : ( 1 ... M ) --> ( 1 ... M ) )
205		fvco3 6275	. . . . . . . . . . . . . . 15 |- ( ( ( `' f o. H ) : ( 1 ... M ) --> ( 1 ... M ) /\ k e. ( 1 ... M ) ) -> ( ( ( F o. f ) o. ( `' f o. H ) ) ` k ) = ( ( F o. f ) ` ( ( `' f o. H ) ` k ) ) )
206	204, 205	sylan 488	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ k e. ( 1 ... M ) ) -> ( ( ( F o. f ) o. ( `' f o. H ) ) ` k ) = ( ( F o. f ) ` ( ( `' f o. H ) ` k ) ) )
207	199, 206	eqtrd 2656	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ k e. ( 1 ... M ) ) -> ( ( F o. H ) ` k ) = ( ( F o. f ) ` ( ( `' f o. H ) ` k ) ) )
208	148, 155, 157, 158, 161, 173, 185, 207	seqf1o 12842	. . . . . . . . . . . 12 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( seq 1 ( .+ , ( F o. H ) ) ` M ) = ( seq 1 ( .+ , ( F o. f ) ) ` M ) )
209	62, 65, 3	mndlid 17311	. . . . . . . . . . . . . 14 |- ( ( G e. Mnd /\ x e. B ) -> ( .0. .+ x ) = x )
210	145, 209	sylan 488	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. B ) -> ( .0. .+ x ) = x )
211	62, 65, 3	mndrid 17312	. . . . . . . . . . . . . 14 |- ( ( G e. Mnd /\ x e. B ) -> ( x .+ .0. ) = x )
212	145, 211	sylan 488	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. B ) -> ( x .+ .0. ) = x )
213	145, 63	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> .0. e. B )
214		fdm 6051	. . . . . . . . . . . . . . . . 17 |- ( H : ( 1 ... M ) --> A -> dom H = ( 1 ... M ) )
215	10, 11, 214	3syl 18	. . . . . . . . . . . . . . . 16 |- ( ph -> dom H = ( 1 ... M ) )
216		eluzfz1 12348	. . . . . . . . . . . . . . . . 17 |- ( M e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... M ) )
217		ne0i 3921	. . . . . . . . . . . . . . . . 17 |- ( 1 e. ( 1 ... M ) -> ( 1 ... M ) =/= (/) )
218	71, 216, 217	3syl 18	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 1 ... M ) =/= (/) )
219	215, 218	eqnetrd 2861	. . . . . . . . . . . . . . 15 |- ( ph -> dom H =/= (/) )
220		dm0rn0 5342	. . . . . . . . . . . . . . . 16 |- ( dom H = (/) <-> ran H = (/) )
221	220	necon3bii 2846	. . . . . . . . . . . . . . 15 |- ( dom H =/= (/) <-> ran H =/= (/) )
222	219, 221	sylib 208	. . . . . . . . . . . . . 14 |- ( ph -> ran H =/= (/) )
223	222	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ran H =/= (/) )
224	114	adantrr 753	. . . . . . . . . . . . 13 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ran H C_ ( m ... n ) )
225		simprl 794	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> A = ( m ... n ) )
226	225	eleq2d 2687	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( x e. A <-> x e. ( m ... n ) ) )
227	226	biimpar 502	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ( m ... n ) ) -> x e. A )
228	159	ffvelrnda 6359	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. A ) -> ( F ` x ) e. B )
229	227, 228	syldan 487	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ( m ... n ) ) -> ( F ` x ) e. B )
230	225	difeq1d 3727	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( A \ ran H ) = ( ( m ... n ) \ ran H ) )
231	230	eleq2d 2687	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( x e. ( A \ ran H ) <-> x e. ( ( m ... n ) \ ran H ) ) )
232	231	biimpar 502	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ( ( m ... n ) \ ran H ) ) -> x e. ( A \ ran H ) )
233		simpll 790	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ph )
234	233, 52	sylan 488	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ( A \ ran H ) ) -> ( F ` x ) = .0. )
235	232, 234	syldan 487	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ x e. ( ( m ... n ) \ ran H ) ) -> ( F ` x ) = .0. )
236		f1of 6137	. . . . . . . . . . . . . . 15 |- ( f : ( 1 ... ( # ` ran H ) ) -1-1-onto-> ran H -> f : ( 1 ... ( # ` ran H ) ) --> ran H )
237	162, 163, 236	3syl 18	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> f : ( 1 ... ( # ` ran H ) ) --> ran H )
238		fvco3 6275	. . . . . . . . . . . . . 14 |- ( ( f : ( 1 ... ( # ` ran H ) ) --> ran H /\ y e. ( 1 ... ( # ` ran H ) ) ) -> ( ( F o. f ) ` y ) = ( F ` ( f ` y ) ) )
239	237, 238	sylan 488	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) /\ y e. ( 1 ... ( # ` ran H ) ) ) -> ( ( F o. f ) ` y ) = ( F ` ( f ` y ) ) )
240	210, 212, 148, 213, 162, 223, 224, 229, 235, 239	seqcoll2 13249	. . . . . . . . . . . 12 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( seq m ( .+ , F ) ` n ) = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` ran H ) ) )
241	144, 208, 240	3eqtr4d 2666	. . . . . . . . . . 11 |- ( ( ( ph /\ W =/= (/) ) /\ ( A = ( m ... n ) /\ f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) ) ) -> ( seq 1 ( .+ , ( F o. H ) ) ` M ) = ( seq m ( .+ , F ) ` n ) )
242	241	expr 643	. . . . . . . . . 10 |- ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ( f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) -> ( seq 1 ( .+ , ( F o. H ) ) ` M ) = ( seq m ( .+ , F ) ` n ) ) )
243	242	exlimdv 1861	. . . . . . . . 9 |- ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ( E. f f Isom < , < ( ( 1 ... ( # ` ran H ) ) , ran H ) -> ( seq 1 ( .+ , ( F o. H ) ) ` M ) = ( seq m ( .+ , F ) ` n ) ) )
244	135, 243	mpd 15	. . . . . . . 8 |- ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ( seq 1 ( .+ , ( F o. H ) ) ` M ) = ( seq m ( .+ , F ) ` n ) )
245	110, 244	eqtr4d 2659	. . . . . . 7 |- ( ( ( ph /\ W =/= (/) ) /\ A = ( m ... n ) ) -> ( G gsumg F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) )
246	245	ex 450	. . . . . 6 |- ( ( ph /\ W =/= (/) ) -> ( A = ( m ... n ) -> ( G gsumg F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) ) )
247	246	rexlimdvw 3034	. . . . 5 |- ( ( ph /\ W =/= (/) ) -> ( E. n e. ZZ A = ( m ... n ) -> ( G gsumg F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) ) )
248	247	rexlimdvw 3034	. . . 4 |- ( ( ph /\ W =/= (/) ) -> ( E. m e. ZZ E. n e. ZZ A = ( m ... n ) -> ( G gsumg F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) ) )
249	82, 248	syl5bi 232	. . 3 |- ( ( ph /\ W =/= (/) ) -> ( A e. ran ... -> ( G gsumg F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) ) )
250		suppssdm 7308	. . . . . . . . . . 11 |- ( ( F o. H ) supp .0. ) C_ dom ( F o. H )
251	32, 250	eqsstri 3635	. . . . . . . . . 10 |- W C_ dom ( F o. H )
252		fdm 6051	. . . . . . . . . . 11 |- ( ( F o. H ) : ( 1 ... M ) --> B -> dom ( F o. H ) = ( 1 ... M ) )
253	30, 252	syl 17	. . . . . . . . . 10 |- ( ph -> dom ( F o. H ) = ( 1 ... M ) )
254	251, 253	syl5sseq 3653	. . . . . . . . 9 |- ( ph -> W C_ ( 1 ... M ) )
255		fzssuz 12382	. . . . . . . . . . 11 |- ( 1 ... M ) C_ ( ZZ>= ` 1 )
256	255, 70	sseqtr4i 3638	. . . . . . . . . 10 |- ( 1 ... M ) C_ NN
257		nnssre 11024	. . . . . . . . . 10 |- NN C_ RR
258	256, 257	sstri 3612	. . . . . . . . 9 |- ( 1 ... M ) C_ RR
259	254, 258	syl6ss 3615	. . . . . . . 8 |- ( ph -> W C_ RR )
260		soss 5053	. . . . . . . 8 |- ( W C_ RR -> ( < Or RR -> < Or W ) )
261	259, 121, 260	mpisyl 21	. . . . . . 7 |- ( ph -> < Or W )
262		ssfi 8180	. . . . . . . 8 |- ( ( ( 1 ... M ) e. Fin /\ W C_ ( 1 ... M ) ) -> W e. Fin )
263	124, 254, 262	sylancr 695	. . . . . . 7 |- ( ph -> W e. Fin )
264		fz1iso 13246	. . . . . . 7 |- ( ( < Or W /\ W e. Fin ) -> E. f f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) )
265	261, 263, 264	syl2anc 693	. . . . . 6 |- ( ph -> E. f f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) )
266	265	ad2antrr 762	. . . . 5 |- ( ( ( ph /\ W =/= (/) ) /\ -. A e. ran ... ) -> E. f f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) )
267	62, 3, 65, 152, 1, 2, 7, 149, 69, 10, 50, 32	gsumval3lem2 18307	. . . . . . . 8 |- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( G gsumg F ) = ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) )
268	1	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> G e. Mnd )
269	268, 209	sylan 488	. . . . . . . . 9 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) /\ x e. B ) -> ( .0. .+ x ) = x )
270	268, 211	sylan 488	. . . . . . . . 9 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) /\ x e. B ) -> ( x .+ .0. ) = x )
271	268, 147	sylan 488	. . . . . . . . 9 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
272	268, 63	syl 17	. . . . . . . . 9 |- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> .0. e. B )
273		simprr 796	. . . . . . . . 9 |- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) )
274		simplr 792	. . . . . . . . 9 |- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> W =/= (/) )
275	254	ad2antrr 762	. . . . . . . . 9 |- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> W C_ ( 1 ... M ) )
276	30	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( F o. H ) : ( 1 ... M ) --> B )
277	276	ffvelrnda 6359	. . . . . . . . 9 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) /\ x e. ( 1 ... M ) ) -> ( ( F o. H ) ` x ) e. B )
278	33	a1i 11	. . . . . . . . . 10 |- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( ( F o. H ) supp .0. ) C_ W )
279		ovexd 6680	. . . . . . . . . 10 |- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( 1 ... M ) e. _V )
280	37	a1i 11	. . . . . . . . . 10 |- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> .0. e. _V )
281	276, 278, 279, 280	suppssr 7326	. . . . . . . . 9 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) /\ x e. ( ( 1 ... M ) \ W ) ) -> ( ( F o. H ) ` x ) = .0. )
282		coass 5654	. . . . . . . . . . 11 |- ( ( F o. H ) o. f ) = ( F o. ( H o. f ) )
283	282	fveq1i 6192	. . . . . . . . . 10 |- ( ( ( F o. H ) o. f ) ` y ) = ( ( F o. ( H o. f ) ) ` y )
284		isof1o 6573	. . . . . . . . . . . 12 |- ( f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) -> f : ( 1 ... ( # ` W ) ) -1-1-onto-> W )
285		f1of 6137	. . . . . . . . . . . 12 |- ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> f : ( 1 ... ( # ` W ) ) --> W )
286	273, 284, 285	3syl 18	. . . . . . . . . . 11 |- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> f : ( 1 ... ( # ` W ) ) --> W )
287		fvco3 6275	. . . . . . . . . . 11 |- ( ( f : ( 1 ... ( # ` W ) ) --> W /\ y e. ( 1 ... ( # ` W ) ) ) -> ( ( ( F o. H ) o. f ) ` y ) = ( ( F o. H ) ` ( f ` y ) ) )
288	286, 287	sylan 488	. . . . . . . . . 10 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) /\ y e. ( 1 ... ( # ` W ) ) ) -> ( ( ( F o. H ) o. f ) ` y ) = ( ( F o. H ) ` ( f ` y ) ) )
289	283, 288	syl5eqr 2670	. . . . . . . . 9 |- ( ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) /\ y e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. ( H o. f ) ) ` y ) = ( ( F o. H ) ` ( f ` y ) ) )
290	269, 270, 271, 272, 273, 274, 275, 277, 281, 289	seqcoll2 13249	. . . . . . . 8 |- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( seq 1 ( .+ , ( F o. H ) ) ` M ) = ( seq 1 ( .+ , ( F o. ( H o. f ) ) ) ` ( # ` W ) ) )
291	267, 290	eqtr4d 2659	. . . . . . 7 |- ( ( ( ph /\ W =/= (/) ) /\ ( -. A e. ran ... /\ f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) ) ) -> ( G gsumg F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) )
292	291	expr 643	. . . . . 6 |- ( ( ( ph /\ W =/= (/) ) /\ -. A e. ran ... ) -> ( f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) -> ( G gsumg F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) ) )
293	292	exlimdv 1861	. . . . 5 |- ( ( ( ph /\ W =/= (/) ) /\ -. A e. ran ... ) -> ( E. f f Isom < , < ( ( 1 ... ( # ` W ) ) , W ) -> ( G gsumg F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) ) )
294	266, 293	mpd 15	. . . 4 |- ( ( ( ph /\ W =/= (/) ) /\ -. A e. ran ... ) -> ( G gsumg F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) )
295	294	ex 450	. . 3 |- ( ( ph /\ W =/= (/) ) -> ( -. A e. ran ... -> ( G gsumg F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) ) )
296	249, 295	pm2.61d 170	. 2 |- ( ( ph /\ W =/= (/) ) -> ( G gsumg F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) )
297	78, 296	pm2.61dane 2881	1 |- ( ph -> ( G gsumg F ) = ( seq 1 ( .+ , ( F o. H ) ) ` M ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   E.wrex 2913   _Vcvv 3200   \ cdif 3571   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   {csn 4177   class class class wbr 4653   |-> cmpt 4729   _I cid 5023   Or wor 5034   X. cxp 5112   `'ccnv 5113   dom cdm 5114   ran crn 5115   |` cres 5116   o. ccom 5118   Rel wrel 5119   Fn wfn 5883   -->wf 5884   -1-1->wf1 5885   -onto->wfo 5886   -1-1-onto->wf1o 5887   ` cfv 5888   Isom wiso 5889  (class class class)co 6650   supp csupp 7295   ~~ cen 7952   Fincfn 7955   RRcr 9935   1c1 9937   < clt 10074   NNcn 11020   NN0cn0 11292   ZZcz 11377   ZZ>=cuz 11687   ...cfz 12326   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-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-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:  gsumzres  18310  gsumzcl2  18311  gsumzf1o  18313  gsumzaddlem  18321  gsumconst  18334  gsumzmhm  18337  gsumzoppg  18344  gsumfsum  19813  wilthlem3  24796