Theorem summolem2a 12464

Description: Lemma for summo 12466. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Mario Carneiro, 20-Apr-2014.)

Hypotheses

Ref	Expression
summo.1	|- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )
summo.2	|- ( ( ph /\ k e. A ) -> B e. CC )
summo.3	|- G = ( n e. NN |-> [_ ( f ` n ) / k ]_ B )
summolem2.4	|- H = ( n e. NN |-> [_ ( K ` n ) / k ]_ B )
summolem2.5	|- ( ph -> N e. NN )
summolem2.6	|- ( ph -> M e. ZZ )
summolem2.7	|- ( ph -> A C_ ( ZZ>= ` M ) )
summolem2.8	|- ( ph -> f : ( 1 ... N ) -1-1-onto-> A )
summolem2.9	|- ( ph -> K Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )

Assertion

Ref	Expression
summolem2a	|- ( ph -> seq M ( + , F ) ~~> ( seq 1 ( + , G ) ` N ) )

Distinct variable groups:   f, k, n, A   f, F, k, n   k, G, n   k, K, n   k, N, n   ph, k, n   B, f, n   k, M, n

Allowed substitution hints:   ph( f)   B( k)   G( f)   H( f, k, n)   K( f)   M( f)   N( f)

Proof of Theorem summolem2a

Dummy variables m x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		summo.1	. . 3 |- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )
2		summo.2	. . 3 |- ( ( ph /\ k e. A ) -> B e. CC )
3		summolem2.7	. . . 4 |- ( ph -> A C_ ( ZZ>= ` M ) )
4		summolem2.9	. . . . . . . 8 |- ( ph -> K Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
5		summolem2.8	. . . . . . . . . . . . 13 |- ( ph -> f : ( 1 ... N ) -1-1-onto-> A )
6		ovex 6065	. . . . . . . . . . . . . 14 |- ( 1 ... N ) e. _V
7	6	f1oen 7087	. . . . . . . . . . . . 13 |- ( f : ( 1 ... N ) -1-1-onto-> A -> ( 1 ... N ) ~~ A )
8	5, 7	syl 16	. . . . . . . . . . . 12 |- ( ph -> ( 1 ... N ) ~~ A )
9		fzfid 11267	. . . . . . . . . . . . 13 |- ( ph -> ( 1 ... N ) e. Fin )
10	8	ensymd 7117	. . . . . . . . . . . . . 14 |- ( ph -> A ~~ ( 1 ... N ) )
11		enfii 7285	. . . . . . . . . . . . . 14 |- ( ( ( 1 ... N ) e. Fin /\ A ~~ ( 1 ... N ) ) -> A e. Fin )
12	9, 10, 11	syl2anc 643	. . . . . . . . . . . . 13 |- ( ph -> A e. Fin )
13		hashen 11586	. . . . . . . . . . . . 13 |- ( ( ( 1 ... N ) e. Fin /\ A e. Fin ) -> ( ( # ` ( 1 ... N ) ) = ( # ` A ) <-> ( 1 ... N ) ~~ A ) )
14	9, 12, 13	syl2anc 643	. . . . . . . . . . . 12 |- ( ph -> ( ( # ` ( 1 ... N ) ) = ( # ` A ) <-> ( 1 ... N ) ~~ A ) )
15	8, 14	mpbird 224	. . . . . . . . . . 11 |- ( ph -> ( # ` ( 1 ... N ) ) = ( # ` A ) )
16		summolem2.5	. . . . . . . . . . . 12 |- ( ph -> N e. NN )
17		nnnn0 10184	. . . . . . . . . . . 12 |- ( N e. NN -> N e. NN0 )
18		hashfz1 11585	. . . . . . . . . . . 12 |- ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
19	16, 17, 18	3syl 19	. . . . . . . . . . 11 |- ( ph -> ( # ` ( 1 ... N ) ) = N )
20	15, 19	eqtr3d 2438	. . . . . . . . . 10 |- ( ph -> ( # ` A ) = N )
21	20	oveq2d 6056	. . . . . . . . 9 |- ( ph -> ( 1 ... ( # ` A ) ) = ( 1 ... N ) )
22		isoeq4 6001	. . . . . . . . 9 |- ( ( 1 ... ( # ` A ) ) = ( 1 ... N ) -> ( K Isom < , < ( ( 1 ... ( # ` A ) ) , A ) <-> K Isom < , < ( ( 1 ... N ) , A ) ) )
23	21, 22	syl 16	. . . . . . . 8 |- ( ph -> ( K Isom < , < ( ( 1 ... ( # ` A ) ) , A ) <-> K Isom < , < ( ( 1 ... N ) , A ) ) )
24	4, 23	mpbid 202	. . . . . . 7 |- ( ph -> K Isom < , < ( ( 1 ... N ) , A ) )
25		isof1o 6004	. . . . . . 7 |- ( K Isom < , < ( ( 1 ... N ) , A ) -> K : ( 1 ... N ) -1-1-onto-> A )
26	24, 25	syl 16	. . . . . 6 |- ( ph -> K : ( 1 ... N ) -1-1-onto-> A )
27		f1of 5633	. . . . . 6 |- ( K : ( 1 ... N ) -1-1-onto-> A -> K : ( 1 ... N ) --> A )
28	26, 27	syl 16	. . . . 5 |- ( ph -> K : ( 1 ... N ) --> A )
29		nnuz 10477	. . . . . . 7 |- NN = ( ZZ>= ` 1 )
30	16, 29	syl6eleq 2494	. . . . . 6 |- ( ph -> N e. ( ZZ>= ` 1 ) )
31		eluzfz2 11021	. . . . . 6 |- ( N e. ( ZZ>= ` 1 ) -> N e. ( 1 ... N ) )
32	30, 31	syl 16	. . . . 5 |- ( ph -> N e. ( 1 ... N ) )
33	28, 32	ffvelrnd 5830	. . . 4 |- ( ph -> ( K ` N ) e. A )
34	3, 33	sseldd 3309	. . 3 |- ( ph -> ( K ` N ) e. ( ZZ>= ` M ) )
35	3	sselda 3308	. . . . . 6 |- ( ( ph /\ n e. A ) -> n e. ( ZZ>= ` M ) )
36		f1ocnvfv2 5974	. . . . . . . . 9 |- ( ( K : ( 1 ... N ) -1-1-onto-> A /\ n e. A ) -> ( K ` ( `' K ` n ) ) = n )
37	26, 36	sylan 458	. . . . . . . 8 |- ( ( ph /\ n e. A ) -> ( K ` ( `' K ` n ) ) = n )
38		f1ocnv 5646	. . . . . . . . . . . 12 |- ( K : ( 1 ... N ) -1-1-onto-> A -> `' K : A -1-1-onto-> ( 1 ... N ) )
39		f1of 5633	. . . . . . . . . . . 12 |- ( `' K : A -1-1-onto-> ( 1 ... N ) -> `' K : A --> ( 1 ... N ) )
40	26, 38, 39	3syl 19	. . . . . . . . . . 11 |- ( ph -> `' K : A --> ( 1 ... N ) )
41	40	ffvelrnda 5829	. . . . . . . . . 10 |- ( ( ph /\ n e. A ) -> ( `' K ` n ) e. ( 1 ... N ) )
42		elfzle2 11017	. . . . . . . . . 10 |- ( ( `' K ` n ) e. ( 1 ... N ) -> ( `' K ` n ) <_ N )
43	41, 42	syl 16	. . . . . . . . 9 |- ( ( ph /\ n e. A ) -> ( `' K ` n ) <_ N )
44	24	adantr 452	. . . . . . . . . 10 |- ( ( ph /\ n e. A ) -> K Isom < , < ( ( 1 ... N ) , A ) )
45		fzssuz 11049	. . . . . . . . . . . . 13 |- ( 1 ... N ) C_ ( ZZ>= ` 1 )
46		uzssz 10461	. . . . . . . . . . . . . 14 |- ( ZZ>= ` 1 ) C_ ZZ
47		zssre 10245	. . . . . . . . . . . . . 14 |- ZZ C_ RR
48	46, 47	sstri 3317	. . . . . . . . . . . . 13 |- ( ZZ>= ` 1 ) C_ RR
49	45, 48	sstri 3317	. . . . . . . . . . . 12 |- ( 1 ... N ) C_ RR
50		ressxr 9085	. . . . . . . . . . . 12 |- RR C_ RR*
51	49, 50	sstri 3317	. . . . . . . . . . 11 |- ( 1 ... N ) C_ RR*
52	51	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ n e. A ) -> ( 1 ... N ) C_ RR* )
53	3	adantr 452	. . . . . . . . . . . 12 |- ( ( ph /\ n e. A ) -> A C_ ( ZZ>= ` M ) )
54		uzssz 10461	. . . . . . . . . . . . 13 |- ( ZZ>= ` M ) C_ ZZ
55	54, 47	sstri 3317	. . . . . . . . . . . 12 |- ( ZZ>= ` M ) C_ RR
56	53, 55	syl6ss 3320	. . . . . . . . . . 11 |- ( ( ph /\ n e. A ) -> A C_ RR )
57	56, 50	syl6ss 3320	. . . . . . . . . 10 |- ( ( ph /\ n e. A ) -> A C_ RR* )
58	32	adantr 452	. . . . . . . . . 10 |- ( ( ph /\ n e. A ) -> N e. ( 1 ... N ) )
59		leisorel 11664	. . . . . . . . . 10 |- ( ( K Isom < , < ( ( 1 ... N ) , A ) /\ ( ( 1 ... N ) C_ RR* /\ A C_ RR* ) /\ ( ( `' K ` n ) e. ( 1 ... N ) /\ N e. ( 1 ... N ) ) ) -> ( ( `' K ` n ) <_ N <-> ( K ` ( `' K ` n ) ) <_ ( K ` N ) ) )
60	44, 52, 57, 41, 58, 59	syl122anc 1193	. . . . . . . . 9 |- ( ( ph /\ n e. A ) -> ( ( `' K ` n ) <_ N <-> ( K ` ( `' K ` n ) ) <_ ( K ` N ) ) )
61	43, 60	mpbid 202	. . . . . . . 8 |- ( ( ph /\ n e. A ) -> ( K ` ( `' K ` n ) ) <_ ( K ` N ) )
62	37, 61	eqbrtrrd 4194	. . . . . . 7 |- ( ( ph /\ n e. A ) -> n <_ ( K ` N ) )
63		eluzelz 10452	. . . . . . . . 9 |- ( n e. ( ZZ>= ` M ) -> n e. ZZ )
64	35, 63	syl 16	. . . . . . . 8 |- ( ( ph /\ n e. A ) -> n e. ZZ )
65		eluzelz 10452	. . . . . . . . . 10 |- ( ( K ` N ) e. ( ZZ>= ` M ) -> ( K ` N ) e. ZZ )
66	34, 65	syl 16	. . . . . . . . 9 |- ( ph -> ( K ` N ) e. ZZ )
67	66	adantr 452	. . . . . . . 8 |- ( ( ph /\ n e. A ) -> ( K ` N ) e. ZZ )
68		eluz 10455	. . . . . . . 8 |- ( ( n e. ZZ /\ ( K ` N ) e. ZZ ) -> ( ( K ` N ) e. ( ZZ>= ` n ) <-> n <_ ( K ` N ) ) )
69	64, 67, 68	syl2anc 643	. . . . . . 7 |- ( ( ph /\ n e. A ) -> ( ( K ` N ) e. ( ZZ>= ` n ) <-> n <_ ( K ` N ) ) )
70	62, 69	mpbird 224	. . . . . 6 |- ( ( ph /\ n e. A ) -> ( K ` N ) e. ( ZZ>= ` n ) )
71		elfzuzb 11009	. . . . . 6 |- ( n e. ( M ... ( K ` N ) ) <-> ( n e. ( ZZ>= ` M ) /\ ( K ` N ) e. ( ZZ>= ` n ) ) )
72	35, 70, 71	sylanbrc 646	. . . . 5 |- ( ( ph /\ n e. A ) -> n e. ( M ... ( K ` N ) ) )
73	72	ex 424	. . . 4 |- ( ph -> ( n e. A -> n e. ( M ... ( K ` N ) ) ) )
74	73	ssrdv 3314	. . 3 |- ( ph -> A C_ ( M ... ( K ` N ) ) )
75	1, 2, 34, 74	fsumcvg 12461	. 2 |- ( ph -> seq M ( + , F ) ~~> ( seq M ( + , F ) ` ( K ` N ) ) )
76		addid2 9205	. . . . 5 |- ( m e. CC -> ( 0 + m ) = m )
77	76	adantl 453	. . . 4 |- ( ( ph /\ m e. CC ) -> ( 0 + m ) = m )
78		addid1 9202	. . . . 5 |- ( m e. CC -> ( m + 0 ) = m )
79	78	adantl 453	. . . 4 |- ( ( ph /\ m e. CC ) -> ( m + 0 ) = m )
80		addcl 9028	. . . . 5 |- ( ( m e. CC /\ x e. CC ) -> ( m + x ) e. CC )
81	80	adantl 453	. . . 4 |- ( ( ph /\ ( m e. CC /\ x e. CC ) ) -> ( m + x ) e. CC )
82		0cn 9040	. . . . 5 |- 0 e. CC
83	82	a1i 11	. . . 4 |- ( ph -> 0 e. CC )
84	32, 21	eleqtrrd 2481	. . . 4 |- ( ph -> N e. ( 1 ... ( # ` A ) ) )
85		iftrue 3705	. . . . . . . . . . 11 |- ( k e. A -> if ( k e. A , B , 0 ) = B )
86	85	adantl 453	. . . . . . . . . 10 |- ( ( ph /\ k e. A ) -> if ( k e. A , B , 0 ) = B )
87	86, 2	eqeltrd 2478	. . . . . . . . 9 |- ( ( ph /\ k e. A ) -> if ( k e. A , B , 0 ) e. CC )
88	87	ex 424	. . . . . . . 8 |- ( ph -> ( k e. A -> if ( k e. A , B , 0 ) e. CC ) )
89		iffalse 3706	. . . . . . . . 9 |- ( -. k e. A -> if ( k e. A , B , 0 ) = 0 )
90	89, 82	syl6eqel 2492	. . . . . . . 8 |- ( -. k e. A -> if ( k e. A , B , 0 ) e. CC )
91	88, 90	pm2.61d1 153	. . . . . . 7 |- ( ph -> if ( k e. A , B , 0 ) e. CC )
92	91	adantr 452	. . . . . 6 |- ( ( ph /\ k e. ZZ ) -> if ( k e. A , B , 0 ) e. CC )
93	92, 1	fmptd 5852	. . . . 5 |- ( ph -> F : ZZ --> CC )
94		elfzelz 11015	. . . . 5 |- ( m e. ( M ... ( K ` ( # ` A ) ) ) -> m e. ZZ )
95		ffvelrn 5827	. . . . 5 |- ( ( F : ZZ --> CC /\ m e. ZZ ) -> ( F ` m ) e. CC )
96	93, 94, 95	syl2an 464	. . . 4 |- ( ( ph /\ m e. ( M ... ( K ` ( # ` A ) ) ) ) -> ( F ` m ) e. CC )
97		fveq2 5687	. . . . . . 7 |- ( k = m -> ( F ` k ) = ( F ` m ) )
98	97	eqeq1d 2412	. . . . . 6 |- ( k = m -> ( ( F ` k ) = 0 <-> ( F ` m ) = 0 ) )
99		eldifi 3429	. . . . . . . . 9 |- ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> k e. ( M ... ( K ` ( # ` A ) ) ) )
100		elfzelz 11015	. . . . . . . . 9 |- ( k e. ( M ... ( K ` ( # ` A ) ) ) -> k e. ZZ )
101	99, 100	syl 16	. . . . . . . 8 |- ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> k e. ZZ )
102		eldifn 3430	. . . . . . . . . 10 |- ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> -. k e. A )
103	102, 89	syl 16	. . . . . . . . 9 |- ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> if ( k e. A , B , 0 ) = 0 )
104	103, 82	syl6eqel 2492	. . . . . . . 8 |- ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> if ( k e. A , B , 0 ) e. CC )
105	1	fvmpt2 5771	. . . . . . . 8 |- ( ( k e. ZZ /\ if ( k e. A , B , 0 ) e. CC ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
106	101, 104, 105	syl2anc 643	. . . . . . 7 |- ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
107	106, 103	eqtrd 2436	. . . . . 6 |- ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> ( F ` k ) = 0 )
108	98, 107	vtoclga 2977	. . . . 5 |- ( m e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> ( F ` m ) = 0 )
109	108	adantl 453	. . . 4 |- ( ( ph /\ m e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) ) -> ( F ` m ) = 0 )
110		isof1o 6004	. . . . . . . 8 |- ( K Isom < , < ( ( 1 ... ( # ` A ) ) , A ) -> K : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
111		f1of 5633	. . . . . . . 8 |- ( K : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> K : ( 1 ... ( # ` A ) ) --> A )
112	4, 110, 111	3syl 19	. . . . . . 7 |- ( ph -> K : ( 1 ... ( # ` A ) ) --> A )
113	112	ffvelrnda 5829	. . . . . 6 |- ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( K ` x ) e. A )
114		iftrue 3705	. . . . . 6 |- ( ( K ` x ) e. A -> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) = [_ ( K ` x ) / k ]_ B )
115	113, 114	syl 16	. . . . 5 |- ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) = [_ ( K ` x ) / k ]_ B )
116	3	adantr 452	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> A C_ ( ZZ>= ` M ) )
117	116, 113	sseldd 3309	. . . . . . 7 |- ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( K ` x ) e. ( ZZ>= ` M ) )
118		eluzelz 10452	. . . . . . 7 |- ( ( K ` x ) e. ( ZZ>= ` M ) -> ( K ` x ) e. ZZ )
119	117, 118	syl 16	. . . . . 6 |- ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( K ` x ) e. ZZ )
120		nfv 1626	. . . . . . . . 9 |- F/ k ph
121		nfv 1626	. . . . . . . . . . 11 |- F/ k ( K ` x ) e. A
122		nfcsb1v 3243	. . . . . . . . . . 11 |- F/_ k [_ ( K ` x ) / k ]_ B
123		nfcv 2540	. . . . . . . . . . 11 |- F/_ k 0
124	121, 122, 123	nfif 3723	. . . . . . . . . 10 |- F/_ k if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 )
125	124	nfel1 2550	. . . . . . . . 9 |- F/ k if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) e. CC
126	120, 125	nfim 1828	. . . . . . . 8 |- F/ k ( ph -> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) e. CC )
127		fvex 5701	. . . . . . . 8 |- ( K ` x ) e. _V
128		eleq1 2464	. . . . . . . . . . 11 |- ( k = ( K ` x ) -> ( k e. A <-> ( K ` x ) e. A ) )
129		csbeq1a 3219	. . . . . . . . . . 11 |- ( k = ( K ` x ) -> B = [_ ( K ` x ) / k ]_ B )
130		eqidd 2405	. . . . . . . . . . 11 |- ( k = ( K ` x ) -> 0 = 0 )
131	128, 129, 130	ifbieq12d 3721	. . . . . . . . . 10 |- ( k = ( K ` x ) -> if ( k e. A , B , 0 ) = if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) )
132	131	eleq1d 2470	. . . . . . . . 9 |- ( k = ( K ` x ) -> ( if ( k e. A , B , 0 ) e. CC <-> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) e. CC ) )
133	132	imbi2d 308	. . . . . . . 8 |- ( k = ( K ` x ) -> ( ( ph -> if ( k e. A , B , 0 ) e. CC ) <-> ( ph -> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) e. CC ) ) )
134	126, 127, 133, 91	vtoclf 2965	. . . . . . 7 |- ( ph -> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) e. CC )
135	134	adantr 452	. . . . . 6 |- ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) e. CC )
136		eleq1 2464	. . . . . . . 8 |- ( n = ( K ` x ) -> ( n e. A <-> ( K ` x ) e. A ) )
137		csbeq1 3214	. . . . . . . 8 |- ( n = ( K ` x ) -> [_ n / k ]_ B = [_ ( K ` x ) / k ]_ B )
138		eqidd 2405	. . . . . . . 8 |- ( n = ( K ` x ) -> 0 = 0 )
139	136, 137, 138	ifbieq12d 3721	. . . . . . 7 |- ( n = ( K ` x ) -> if ( n e. A , [_ n / k ]_ B , 0 ) = if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) )
140		nfcv 2540	. . . . . . . . 9 |- F/_ n if ( k e. A , B , 0 )
141		nfv 1626	. . . . . . . . . 10 |- F/ k n e. A
142		nfcsb1v 3243	. . . . . . . . . 10 |- F/_ k [_ n / k ]_ B
143	141, 142, 123	nfif 3723	. . . . . . . . 9 |- F/_ k if ( n e. A , [_ n / k ]_ B , 0 )
144		eleq1 2464	. . . . . . . . . 10 |- ( k = n -> ( k e. A <-> n e. A ) )
145		csbeq1a 3219	. . . . . . . . . 10 |- ( k = n -> B = [_ n / k ]_ B )
146		eqidd 2405	. . . . . . . . . 10 |- ( k = n -> 0 = 0 )
147	144, 145, 146	ifbieq12d 3721	. . . . . . . . 9 |- ( k = n -> if ( k e. A , B , 0 ) = if ( n e. A , [_ n / k ]_ B , 0 ) )
148	140, 143, 147	cbvmpt 4259	. . . . . . . 8 |- ( k e. ZZ |-> if ( k e. A , B , 0 ) ) = ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) )
149	1, 148	eqtri 2424	. . . . . . 7 |- F = ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) )
150	139, 149	fvmptg 5763	. . . . . 6 |- ( ( ( K ` x ) e. ZZ /\ if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) e. CC ) -> ( F ` ( K ` x ) ) = if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) )
151	119, 135, 150	syl2anc 643	. . . . 5 |- ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( F ` ( K ` x ) ) = if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) )
152		elfznn 11036	. . . . . . 7 |- ( x e. ( 1 ... ( # ` A ) ) -> x e. NN )
153	152	adantl 453	. . . . . 6 |- ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> x e. NN )
154	115, 135	eqeltrrd 2479	. . . . . 6 |- ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> [_ ( K ` x ) / k ]_ B e. CC )
155		fveq2 5687	. . . . . . . 8 |- ( n = x -> ( K ` n ) = ( K ` x ) )
156	155	csbeq1d 3217	. . . . . . 7 |- ( n = x -> [_ ( K ` n ) / k ]_ B = [_ ( K ` x ) / k ]_ B )
157		summolem2.4	. . . . . . 7 |- H = ( n e. NN |-> [_ ( K ` n ) / k ]_ B )
158	156, 157	fvmptg 5763	. . . . . 6 |- ( ( x e. NN /\ [_ ( K ` x ) / k ]_ B e. CC ) -> ( H ` x ) = [_ ( K ` x ) / k ]_ B )
159	153, 154, 158	syl2anc 643	. . . . 5 |- ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( H ` x ) = [_ ( K ` x ) / k ]_ B )
160	115, 151, 159	3eqtr4rd 2447	. . . 4 |- ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( H ` x ) = ( F ` ( K ` x ) ) )
161	77, 79, 81, 83, 4, 84, 3, 96, 109, 160	seqcoll 11667	. . 3 |- ( ph -> ( seq M ( + , F ) ` ( K ` N ) ) = ( seq 1 ( + , H ) ` N ) )
162		summo.3	. . . 4 |- G = ( n e. NN |-> [_ ( f ` n ) / k ]_ B )
163	16, 16	jca 519	. . . 4 |- ( ph -> ( N e. NN /\ N e. NN ) )
164	1, 2, 162, 157, 163, 5, 26	summolem3 12463	. . 3 |- ( ph -> ( seq 1 ( + , G ) ` N ) = ( seq 1 ( + , H ) ` N ) )
165	161, 164	eqtr4d 2439	. 2 |- ( ph -> ( seq M ( + , F ) ` ( K ` N ) ) = ( seq 1 ( + , G ) ` N ) )
166	75, 165	breqtrd 4196	1 |- ( ph -> seq M ( + , F ) ~~> ( seq 1 ( + , G ) ` N ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   /\ wa 359   = wceq 1649   e. wcel 1721   [_csb 3211   \ cdif 3277   C_ wss 3280   ifcif 3699   class class class wbr 4172   e. cmpt 4226   `'ccnv 4836   -->wf 5409   -1-1-onto->wf1o 5412   ` cfv 5413   Isom wiso 5414  (class class class)co 6040   ~~ cen 7065   Fincfn 7068   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947   + caddc 8949   RR*cxr 9075   < clt 9076   <_ cle 9077   NNcn 9956   NN0cn0 10177   ZZcz 10238   ZZ>=cuz 10444   ...cfz 10999   seq cseq 11278   #chash 11573   ~~> cli 12233

This theorem is referenced by:  summolem2  12465  zsum  12467

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-card 7782  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-n0 10178  df-z 10239  df-uz 10445  df-rp 10569  df-fz 11000  df-fzo 11091  df-seq 11279  df-exp 11338  df-hash 11574  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-clim 12237