Theorem sumeq2sdv 15645

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 3866	. . . . . . . . . 10 ⊢ (𝜑 → ⦋𝑛 / 𝑘⦌𝐵 = ⦋𝑛 / 𝑘⦌𝐶)
3	2	ifeq1d 4504	. . . . . . . . 9 ⊢ (𝜑 → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) = if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))
4	3	mpteq2dv 5196	. . . . . . . 8 ⊢ (𝜑 → (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0)))
5	4	seqeq3d 13950	. . . . . . 7 ⊢ (𝜑 → seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) = seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))))
6	5	breq1d 5112	. . . . . 6 ⊢ (𝜑 → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 ↔ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥))
7	6	anbi2d 630	. . . . 5 ⊢ (𝜑 → ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥)))
8	7	rexbidv 3157	. . . 4 ⊢ (𝜑 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥)))
9	1	csbeq2dv 3866	. . . . . . . . . . 11 ⊢ (𝜑 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑛) / 𝑘⦌𝐶)
10	9	mpteq2dv 5196	. . . . . . . . . 10 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))
11	10	seqeq3d 13950	. . . . . . . . 9 ⊢ (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)) = seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶)))
12	11	fveq1d 6842	. . . . . . . 8 ⊢ (𝜑 → (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))
13	12	eqeq2d 2740	. . . . . . 7 ⊢ (𝜑 → (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) ↔ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))
14	13	anbi2d 630	. . . . . 6 ⊢ (𝜑 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
15	14	exbidv 1921	. . . . 5 ⊢ (𝜑 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
16	15	rexbidv 3157	. . . 4 ⊢ (𝜑 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
17	8, 16	orbi12d 918	. . 3 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))))
18	17	iotabidv 6483	. 2 ⊢ (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))))
19		df-sum 15629	. 2 ⊢ Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
20		df-sum 15629	. 2 ⊢ Σ𝑘 ∈ 𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
21	18, 19, 20	3eqtr4g 2789	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∃wrex 3053  ⦋csb 3859   ⊆ wss 3911  ifcif 4484   class class class wbr 5102   ↦ cmpt 5183  ℩cio 6450  –1-1-onto→wf1o 6498  ‘cfv 6499  (class class class)co 7369  0cc0 11044  1c1 11045   + caddc 11047  ℕcn 12162  ℤcz 12505  ℤ_≥cuz 12769  ...cfz 13444  seqcseq 13942   ⇝ cli 15426  Σcsu 15628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-xp 5637  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-iota 6452  df-fv 6507  df-ov 7372  df-oprab 7373  df-mpo 7374  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-seq 13943  df-sum 15629

This theorem is referenced by:  sumsplit  15710  fsumrlim  15753  hash2iun1dif1  15766  incexclem  15778  bpolylem  15990  bpolyval  15991  efval  16021  rpnnen2lem12  16169  pcfac  16846  ramcl  16976  cshwshashnsame  17050  fsumcn  24794  fsum2cn  24795  lebnumlem3  24895  rrxdsfival  25346  uniioombllem6  25522  itg1climres  25648  itgeq1f  25705  itgeq1fOLD  25706  itgeq1  25707  cbvitgv  25711  itgeq2  25712  dvmptfsum  25912  elplyr  26139  plyeq0lem  26148  plyadd  26155  plymul  26156  coeeu  26163  coelem  26164  coeeq  26165  coeidlem  26175  coeid  26176  coeid2  26177  plyco  26179  plycjlem  26215  aareccl  26267  taylply2  26308  taylply2OLD  26309  pserdvlem2  26371  pserdv  26372  abelthlem6  26379  abelthlem9  26383  logtayl  26602  leibpi  26885  basellem3  27026  dchrvmasum2if  27441  dchrvmaeq0  27448  rpvmasum2  27456  dchrisum0re  27457  brcgr  28880  axsegcon  28907  dipfval  30681  ipval  30682  fsumiunle  32804  itgeq12dv  34310  eulerpartleme  34347  eulerpartlemr  34358  eulerpartlemn  34365  reprsum  34597  reprsuc  34599  reprpmtf1o  34610  vtsval  34621  iprodgam  35722  fwddifnval  36144  sumeq12sdv  36198  itgeq12sdv  36200  cbvitgdavw  36262  cbvitgdavw2  36278  knoppndvlem6  36498  knoppf  36516  rrnmval  37815  fsumshftd  38938  fsumcnf  45008  mccl  45589  dvnmul  45934  dvmptfprod  45936  dvnprodlem1  45937  dvnprodlem3  45939  dvnprod  45940  stoweidlem17  46008  stoweidlem26  46017  stoweidlem30  46021  stoweidlem32  46023  dirkertrigeq  46092  dirkeritg  46093  fourierdlem83  46180  fourierdlem103  46200  etransclem11  46236  etransclem24  46249  etransclem26  46251  etransclem27  46252  etransclem28  46253  etransclem31  46256  etransclem35  46260  etransclem46  46271  etransclem47  46272  rrndistlt  46281  ioorrnopn  46296  sge0val  46357  hoiqssbllem2  46614  nnsum3primes4  47782  nnsum4primesodd  47790  nnsum4primesoddALTV  47791  nnsum4primesevenALTV  47795  nn0sumshdiglemB  48602  nn0sumshdiglem1  48603  aacllem  49783