Theorem sumeq1 6982

Description: Equality theorem for a sum.

Assertion

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

Proof of Theorem sumeq1

Step	Hyp	Ref	Expression
1		eqeq1 1484	. . . . . . 7 |- (A = B -> (A = (m...n) <-> B = (m...n)))
2	1	anbi1d 619	. . . . . 6 |- (A = B -> ((A = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = C} |` ZZ))` n)) <-> (B = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = C} |` ZZ))` n))))
3	2	rexbidv 1667	. . . . 5 |- (A = B -> (E.n e. (ZZ>` m)(A = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = C} |` ZZ))` n)) <-> E.n e. (ZZ>` m)(B = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = C} |` ZZ))` n))))
4	3	exbidv 1281	. . . 4 |- (A = B -> (E.mE.n e. (ZZ>` m)(A = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = C} |` ZZ))` n)) <-> E.mE.n e. (ZZ>` m)(B = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = C} |` ZZ))` n))))
5	4	abbidv 1580	. . 3 |- (A = B -> {x | E.mE.n e. (ZZ>` m)(A = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = C} |` ZZ))` n))} = {x | E.mE.n e. (ZZ>` m)(B = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = C} |` ZZ))` n))})
6		eqeq1 1484	. . . . . . 7 |- (A = B -> (A = (ZZ>` m) <-> B = (ZZ>` m)))
7	6	anbi1d 619	. . . . . 6 |- (A = B -> ((A = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = C} |` ZZ)) ~~> x) <-> (B = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = C} |` ZZ)) ~~> x)))
8	7	rexbidv 1667	. . . . 5 |- (A = B -> (E.m e. ZZ (A = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = C} |` ZZ)) ~~> x) <-> E.m e. ZZ (B = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = C} |` ZZ)) ~~> x)))
9	8	abbidv 1580	. . . 4 |- (A = B -> {x | E.m e. ZZ (A = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = C} |` ZZ)) ~~> x)} = {x | E.m e. ZZ (B = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = C} |` ZZ)) ~~> x)})
10	9	unieqd 2516	. . 3 |- (A = B -> U.{x | E.m e. ZZ (A = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = C} |` ZZ)) ~~> x)} = U.{x | E.m e. ZZ (B = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = C} |` ZZ)) ~~> x)})
11	5, 10	uneq12d 2188	. 2 |- (A = B -> ({x | E.mE.n e. (ZZ>` m)(A = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = C} |` ZZ))` n))} u. U.{x | E.m e. ZZ (A = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = C} |` ZZ)) ~~> x)}) = ({x | E.mE.n e. (ZZ>` m)(B = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = C} |` ZZ))` n))} u. U.{x | E.m e. ZZ (B = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = C} |` ZZ)) ~~> x)}))
12		df-sum 6980	. 2 |- sum_k e. A C = ({x | E.mE.n e. (ZZ>` m)(A = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = C} |` ZZ))` n))} u. U.{x | E.m e. ZZ (A = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = C} |` ZZ)) ~~> x)})
13		df-sum 6980	. 2 |- sum_k e. B C = ({x | E.mE.n e. (ZZ>` m)(B = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = C} |` ZZ))` n))} u. U.{x | E.m e. ZZ (B = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = C} |` ZZ)) ~~> x)})
14	11, 12, 13	3eqtr4g 1534	1 |- (A = B -> sum_k e. A C = sum_k e. B C)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 958   e. wcel 960  E.wex 982  {cab 1466  E.wrex 1649   u. cun 2048  <.cop 2415  U.cuni 2507   class class class wbr 2624  {copab 2671   |` cres 3178  ` cfv 3188  (class class class)co 3969   + caddc 5249  ZZcz 5310  ZZ>cuz 6418  ...cfz 6468   seq cseqz 6532   ~~> cli 6974  sum_csu 6979

This theorem is referenced by:  sumeq1i 6987  sumeq1d 6990

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-rex 1653  df-v 1815  df-un 2053  df-uni 2508  df-sum 6980

Copyright terms: Public domain