Theorem sumeq2 6953

Description: Equality theorem for sum.

Assertion

Ref	Expression
sumeq2	|- (A.k e. A B = C -> sum_k e. A B = sum_k e. A C)

Distinct variable group:   A,k

Proof of Theorem sumeq2

Step	Hyp	Ref	Expression
1		hbra1 1686	. . . . . . . . . . . . . . . 16 |- (A.k e. A B = C -> A.kA.k e. A B = C)
2		ax-17 970	. . . . . . . . . . . . . . . 16 |- (A.k e. A B = C -> A.yA.k e. A B = C)
3		ra4 1693	. . . . . . . . . . . . . . . . . . 19 |- (A.k e. A B = C -> (k e. A -> B = C))
4	3	imp 350	. . . . . . . . . . . . . . . . . 18 |- ((A.k e. A B = C /\ k e. A) -> B = C)
5	4	eqeq2d 1485	. . . . . . . . . . . . . . . . 17 |- ((A.k e. A B = C /\ k e. A) -> (y = B <-> y = C))
6	5	pm5.32da 648	. . . . . . . . . . . . . . . 16 |- (A.k e. A B = C -> ((k e. A /\ y = B) <-> (k e. A /\ y = C)))
7	1, 2, 6	opabbid 2666	. . . . . . . . . . . . . . 15 |- (A.k e. A B = C -> {<.k, y>. | (k e. A /\ y = B)} = {<.k, y>. | (k e. A /\ y = C)})
8		resopab 3392	. . . . . . . . . . . . . . 15 |- ({<.k, y>. | y = B} |` A) = {<.k, y>. | (k e. A /\ y = B)}
9		resopab 3392	. . . . . . . . . . . . . . 15 |- ({<.k, y>. | y = C} |` A) = {<.k, y>. | (k e. A /\ y = C)}
10	7, 8, 9	3eqtr4g 1530	. . . . . . . . . . . . . 14 |- (A.k e. A B = C -> ({<.k, y>. | y = B} |` A) = ({<.k, y>. | y = C} |` A))
11	10	adantr 389	. . . . . . . . . . . . 13 |- ((A.k e. A B = C /\ A = (m...n)) -> ({<.k, y>. | y = B} |` A) = ({<.k, y>. | y = C} |` A))
12		reseq2 3366	. . . . . . . . . . . . . 14 |- (A = (m...n) -> ({<.k, y>. | y = B} |` A) = ({<.k, y>. | y = B} |` (m...n)))
13	12	adantl 388	. . . . . . . . . . . . 13 |- ((A.k e. A B = C /\ A = (m...n)) -> ({<.k, y>. | y = B} |` A) = ({<.k, y>. | y = B} |` (m...n)))
14		reseq2 3366	. . . . . . . . . . . . . 14 |- (A = (m...n) -> ({<.k, y>. | y = C} |` A) = ({<.k, y>. | y = C} |` (m...n)))
15	14	adantl 388	. . . . . . . . . . . . 13 |- ((A.k e. A B = C /\ A = (m...n)) -> ({<.k, y>. | y = C} |` A) = ({<.k, y>. | y = C} |` (m...n)))
16	11, 13, 15	3eqtr3d 1514	. . . . . . . . . . . 12 |- ((A.k e. A B = C /\ A = (m...n)) -> ({<.k, y>. | y = B} |` (m...n)) = ({<.k, y>. | y = C} |` (m...n)))
17	16	opreq2d 3973	. . . . . . . . . . 11 |- ((A.k e. A B = C /\ A = (m...n)) -> (<.m, + >. seq ({<.k, y>. | y = B} |` (m...n))) = (<.m, + >. seq ({<.k, y>. | y = C} |` (m...n))))
18	17	fveq1d 3723	. . . . . . . . . 10 |- ((A.k e. A B = C /\ A = (m...n)) -> ((<.m, + >. seq ({<.k, y>. | y = B} |` (m...n)))` n) = ((<.m, + >. seq ({<.k, y>. | y = C} |` (m...n)))` n))
19	18	adantlr 393	. . . . . . . . 9 |- (((A.k e. A B = C /\ n e. (ZZ>` m)) /\ A = (m...n)) -> ((<.m, + >. seq ({<.k, y>. | y = B} |` (m...n)))` n) = ((<.m, + >. seq ({<.k, y>. | y = C} |` (m...n)))` n))
20		elfzelz 6432	. . . . . . . . . . . . . 14 |- (x e. (m...n) -> x e. ZZ)
21		fvres 3731	. . . . . . . . . . . . . 14 |- (x e. ZZ -> (({<.k, y>. | y = B} |` ZZ)` x) = ({<.k, y>. | y = B}` x))
22	20, 21	syl 10	. . . . . . . . . . . . 13 |- (x e. (m...n) -> (({<.k, y>. | y = B} |` ZZ)` x) = ({<.k, y>. | y = B}` x))
23		fvres 3731	. . . . . . . . . . . . 13 |- (x e. (m...n) -> (({<.k, y>. | y = B} |` (m...n))` x) = ({<.k, y>. | y = B}` x))
24	22, 23	eqtr4d 1509	. . . . . . . . . . . 12 |- (x e. (m...n) -> (({<.k, y>. | y = B} |` ZZ)` x) = (({<.k, y>. | y = B} |` (m...n))` x))
25	24	rgen 1697	. . . . . . . . . . 11 |- A.x e. (m...n)(({<.k, y>. | y = B} |` ZZ)` x) = (({<.k, y>. | y = B} |` (m...n))` x)
26		addex 5304	. . . . . . . . . . . 12 |- + e. V
27		funopabeq 3546	. . . . . . . . . . . . 13 |- Fun {<.k, y>. | y = B}
28		zex 6105	. . . . . . . . . . . . 13 |- ZZ e. V
29		resfunexg 3576	. . . . . . . . . . . . 13 |- ((Fun {<.k, y>. | y = B} /\ ZZ e. V) -> ({<.k, y>. | y = B} |` ZZ) e. V)
30	27, 28, 29	mp2an 696	. . . . . . . . . . . 12 |- ({<.k, y>. | y = B} |` ZZ) e. V
31		oprex 3980	. . . . . . . . . . . . 13 |- (m...n) e. V
32		resfunexg 3576	. . . . . . . . . . . . 13 |- ((Fun {<.k, y>. | y = B} /\ (m...n) e. V) -> ({<.k, y>. | y = B} |` (m...n)) e. V)
33	27, 31, 32	mp2an 696	. . . . . . . . . . . 12 |- ({<.k, y>. | y = B} |` (m...n)) e. V
34	26, 30, 33	seqzfveq 6504	. . . . . . . . . . 11 |- ((n e. (ZZ>` m) /\ A.x e. (m...n)(({<.k, y>. | y = B} |` ZZ)` x) = (({<.k, y>. | y = B} |` (m...n))` x)) -> ((<.m, + >. seq ({<.k, y>. | y = B} |` ZZ))` n) = ((<.m, + >. seq ({<.k, y>. | y = B} |` (m...n)))` n))
35	25, 34	mpan2 695	. . . . . . . . . 10 |- (n e. (ZZ>` m) -> ((<.m, + >. seq ({<.k, y>. | y = B} |` ZZ))` n) = ((<.m, + >. seq ({<.k, y>. | y = B} |` (m...n)))` n))
36	35	ad2antlr 405	. . . . . . . . 9 |- (((A.k e. A B = C /\ n e. (ZZ>` m)) /\ A = (m...n)) -> ((<.m, + >. seq ({<.k, y>. | y = B} |` ZZ))` n) = ((<.m, + >. seq ({<.k, y>. | y = B} |` (m...n)))` n))
37		fvres 3731	. . . . . . . . . . . . . 14 |- (x e. ZZ -> (({<.k, y>. | y = C} |` ZZ)` x) = ({<.k, y>. | y = C}` x))
38	20, 37	syl 10	. . . . . . . . . . . . 13 |- (x e. (m...n) -> (({<.k, y>. | y = C} |` ZZ)` x) = ({<.k, y>. | y = C}` x))
39		fvres 3731	. . . . . . . . . . . . 13 |- (x e. (m...n) -> (({<.k, y>. | y = C} |` (m...n))` x) = ({<.k, y>. | y = C}` x))
40	38, 39	eqtr4d 1509	. . . . . . . . . . . 12 |- (x e. (m...n) -> (({<.k, y>. | y = C} |` ZZ)` x) = (({<.k, y>. | y = C} |` (m...n))` x))
41	40	rgen 1697	. . . . . . . . . . 11 |- A.x e. (m...n)(({<.k, y>. | y = C} |` ZZ)` x) = (({<.k, y>. | y = C} |` (m...n))` x)
42		funopabeq 3546	. . . . . . . . . . . . 13 |- Fun {<.k, y>. | y = C}
43		resfunexg 3576	. . . . . . . . . . . . 13 |- ((Fun {<.k, y>. | y = C} /\ ZZ e. V) -> ({<.k, y>. | y = C} |` ZZ) e. V)
44	42, 28, 43	mp2an 696	. . . . . . . . . . . 12 |- ({<.k, y>. | y = C} |` ZZ) e. V
45		resfunexg 3576	. . . . . . . . . . . . 13 |- ((Fun {<.k, y>. | y = C} /\ (m...n) e. V) -> ({<.k, y>. | y = C} |` (m...n)) e. V)
46	42, 31, 45	mp2an 696	. . . . . . . . . . . 12 |- ({<.k, y>. | y = C} |` (m...n)) e. V
47	26, 44, 46	seqzfveq 6504	. . . . . . . . . . 11 |- ((n e. (ZZ>` m) /\ A.x e. (m...n)(({<.k, y>. | y = C} |` ZZ)` x) = (({<.k, y>. | y = C} |` (m...n))` x)) -> ((<.m, + >. seq ({<.