Theorem sumeq2sdv 15665

Description: Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Proof shortened by Glauco Siliprandi, 5-Apr-2020.) Avoid axioms. (Revised by GG, 14-Aug-2025.)

Hypothesis

Ref	Expression
sumeq2sdv.1	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
sumeq2sdv	⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)

Distinct variable group:   𝜑,𝑘

Allowed substitution hints:   𝐴(𝑘)   𝐵(𝑘)   𝐶(𝑘)

Proof of Theorem sumeq2sdv

Dummy variables 𝑥 𝑚 𝑛 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sumeq2sdv.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 = 𝐶)
2	1	csbeq2dv 3844	. . . . . . . . . 10 ⊢ (𝜑 → ⦋𝑛 / 𝑘⦌𝐵 = ⦋𝑛 / 𝑘⦌𝐶)
3	2	ifeq1d 4486	. . . . . . . . 9 ⊢ (𝜑 → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) = if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))
4	3	mpteq2dv 5179	. . . . . . . 8 ⊢ (𝜑 → (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0)))
5	4	seqeq3d 13971	. . . . . . 7 ⊢ (𝜑 → seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) = seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))))
6	5	breq1d 5095	. . . . . 6 ⊢ (𝜑 → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 ↔ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥))
7	6	anbi2d 631	. . . . 5 ⊢ (𝜑 → ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥)))
8	7	rexbidv 3161	. . . 4 ⊢ (𝜑 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥)))
9	1	csbeq2dv 3844	. . . . . . . . . . 11 ⊢ (𝜑 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑛) / 𝑘⦌𝐶)
10	9	mpteq2dv 5179	. . . . . . . . . 10 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))
11	10	seqeq3d 13971	. . . . . . . . 9 ⊢ (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)) = seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶)))
12	11	fveq1d 6842	. . . . . . . 8 ⊢ (𝜑 → (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))
13	12	eqeq2d 2747	. . . . . . 7 ⊢ (𝜑 → (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) ↔ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))
14	13	anbi2d 631	. . . . . 6 ⊢ (𝜑 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
15	14	exbidv 1923	. . . . 5 ⊢ (𝜑 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
16	15	rexbidv 3161	. . . 4 ⊢ (𝜑 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
17	8, 16	orbi12d 919	. . 3 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))))
18	17	iotabidv 6482	. 2 ⊢ (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))))
19		df-sum 15649	. 2 ⊢ Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
20		df-sum 15649	. 2 ⊢ Σ𝑘 ∈ 𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
21	18, 19, 20	3eqtr4g 2796	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 848   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∃wrex 3061  ⦋csb 3837   ⊆ wss 3889  ifcif 4466   class class class wbr 5085   ↦ cmpt 5166  ℩cio 6452  –1-1-onto→wf1o 6497  ‘cfv 6498  (class class class)co 7367  0cc0 11038  1c1 11039   + caddc 11041  ℕcn 12174  ℤcz 12524  ℤ_≥cuz 12788  ...cfz 13461  seqcseq 13963   ⇝ cli 15446  Σcsu 15648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-xp 5637  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-iota 6454  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-seq 13964  df-sum 15649

This theorem is referenced by:  sumsplit  15730  fsumrlim  15774  hash2iun1dif1  15787  incexclem  15801  bpolylem  16013  bpolyval  16014  efval  16044  rpnnen2lem12  16192  pcfac  16870  ramcl  17000  cshwshashnsame  17074  fsumcn  24837  fsum2cn  24838  lebnumlem3  24930  rrxdsfival  25380  uniioombllem6  25555  itg1climres  25681  itgeq1f  25738  itgeq1fOLD  25739  itgeq1  25740  cbvitgv  25744  itgeq2  25745  dvmptfsum  25942  elplyr  26166  plyeq0lem  26175  plyadd  26182  plymul  26183  coeeu  26190  coelem  26191  coeeq  26192  coeidlem  26202  coeid  26203  coeid2  26204  plyco  26206  plycjlem  26241  aareccl  26292  taylply2  26333  pserdvlem2  26393  pserdv  26394  abelthlem6  26401  abelthlem9  26405  logtayl  26624  leibpi  26906  basellem3  27046  dchrvmasum2if  27460  dchrvmaeq0  27467  rpvmasum2  27475  dchrisum0re  27476  brcgr  28969  axsegcon  28996  dipfval  30773  ipval  30774  fsumiunle  32902  itgeq12dv  34470  eulerpartleme  34507  eulerpartlemr  34518  eulerpartlemn  34525  reprsum  34757  reprsuc  34759  reprpmtf1o  34770  vtsval  34781  iprodgam  35924  fwddifnval  36345  sumeq12sdv  36399  itgeq12sdv  36401  cbvitgdavw  36463  cbvitgdavw2  36479  knoppndvlem6  36777  knoppf  36795  rrnmval  38149  fsumshftd  39398  fsumcnf  45452  mccl  46028  dvnmul  46371  dvmptfprod  46373  dvnprodlem1  46374  dvnprodlem3  46376  dvnprod  46377  stoweidlem17  46445  stoweidlem26  46454  stoweidlem30  46458  stoweidlem32  46460  dirkertrigeq  46529  dirkeritg  46530  fourierdlem83  46617  fourierdlem103  46637  etransclem11  46673  etransclem24  46686  etransclem26  46688  etransclem27  46689  etransclem28  46690  etransclem31  46693  etransclem35  46697  etransclem46  46708  etransclem47  46709  rrndistlt  46718  ioorrnopn  46733  sge0val  46794  hoiqssbllem2  47051  nnsum3primes4  48264  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  nnsum4primesevenALTV  48277  nn0sumshdiglemB  49096  nn0sumshdiglem1  49097  aacllem  50276