Theorem cbvsum 15648

Description: Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)

Hypotheses

Ref	Expression
cbvsum.1	⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)
cbvsum.2	⊢ Ⅎ𝑘𝐵
cbvsum.3	⊢ Ⅎ𝑗𝐶

Assertion

Ref	Expression
cbvsum	⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶

Distinct variable group:   𝑗,𝑘

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

Proof of Theorem cbvsum

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

Step	Hyp	Ref	Expression
1		cbvsum.2	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘𝐵
2		cbvsum.3	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗𝐶
3		cbvsum.1	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)
4	1, 2, 3	cbvcsbw 3848	. . . . . . . . . . . 12 ⊢ ⦋𝑛 / 𝑗⦌𝐵 = ⦋𝑛 / 𝑘⦌𝐶
5	4	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → ⦋𝑛 / 𝑗⦌𝐵 = ⦋𝑛 / 𝑘⦌𝐶)
6	5	ifeq1d 4487	. . . . . . . . . 10 ⊢ (⊤ → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑗⦌𝐵, 0) = if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))
7	6	mpteq2dv 5180	. . . . . . . . 9 ⊢ (⊤ → (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑗⦌𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0)))
8	7	seqeq3d 13962	. . . . . . . 8 ⊢ (⊤ → seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑗⦌𝐵, 0))) = seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))))
9	8	mptru 1549	. . . . . . 7 ⊢ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑗⦌𝐵, 0))) = seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0)))
10	9	breq1i 5093	. . . . . 6 ⊢ (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑗⦌𝐵, 0))) ⇝ 𝑥 ↔ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥)
11	10	anbi2i 624	. . . . 5 ⊢ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑗⦌𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥))
12	11	rexbii 3085	. . . 4 ⊢ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑗⦌𝐵, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥))
13	1, 2, 3	cbvcsbw 3848	. . . . . . . . . . . . 13 ⊢ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵 = ⦋(𝑓‘𝑛) / 𝑘⦌𝐶
14	13	a1i 11	. . . . . . . . . . . 12 ⊢ (⊤ → ⦋(𝑓‘𝑛) / 𝑗⦌𝐵 = ⦋(𝑓‘𝑛) / 𝑘⦌𝐶)
15	14	mpteq2dv 5180	. . . . . . . . . . 11 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵) = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))
16	15	seqeq3d 13962	. . . . . . . . . 10 ⊢ (⊤ → seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵)) = seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶)))
17	16	mptru 1549	. . . . . . . . 9 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵)) = seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))
18	17	fveq1i 6835	. . . . . . . 8 ⊢ (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)
19	18	eqeq2i 2750	. . . . . . 7 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵))‘𝑚) ↔ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))
20	19	anbi2i 624	. . . . . 6 ⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))
21	20	exbii 1850	. . . . 5 ⊢ (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))
22	21	rexbii 3085	. . . 4 ⊢ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))
23	12, 22	orbi12i 915	. . 3 ⊢ ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑗⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵))‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
24	23	iotabii 6477	. 2 ⊢ (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑗⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵))‘𝑚)))) = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
25		df-sum 15640	. 2 ⊢ Σ𝑗 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑗⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵))‘𝑚))))
26		df-sum 15640	. 2 ⊢ Σ𝑘 ∈ 𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
27	24, 25, 26	3eqtr4i 2770	1 ⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 848   = wceq 1542  ⊤wtru 1543  ∃wex 1781   ∈ wcel 2114  Ⅎwnfc 2884  ∃wrex 3062  ⦋csb 3838   ⊆ wss 3890  ifcif 4467   class class class wbr 5086   ↦ cmpt 5167  ℩cio 6446  –1-1-onto→wf1o 6491  ‘cfv 6492  (class class class)co 7360  0cc0 11029  1c1 11030   + caddc 11032  ℕcn 12165  ℤcz 12515  ℤ_≥cuz 12779  ...cfz 13452  seqcseq 13954   ⇝ cli 15437  Σcsu 15639

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-11 2163  ax-12 2185  ax-ext 2709

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-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-xp 5630  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-iota 6448  df-fv 6500  df-ov 7363  df-oprab 7364  df-mpo 7365  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-seq 13955  df-sum 15640

This theorem is referenced by:  sumfc  15662  sumss2  15679  fsumclf  15691  fsumzcl2  15692  fsumsplitf  15695  sumsnf  15696  sumsns  15703  fsummsnunz  15707  fsumsplitsnun  15708  fsum2dlem  15723  fsumcom2  15727  fsumshftm  15734  fsumrlim  15765  fsumo1  15766  o1fsum  15767  fsumiun  15775  ovolfiniun  25478  ovoliun2  25483  volfiniun  25524  itgfsum  25804  elplyd  26177  coeeq2  26217  fsumdvdscom  27162  fsumdvdsmul  27172  fsumvma  27190  fsumiunle  32917  esumpfinvalf  34236  fsumshftd  39412  sticksstones8  42606  sticksstones10  42608  sticksstones12a  42610  sticksstones12  42611  aks6d1c7lem3  42635  binomcxplemdvsum  44800  sumsnd  45475  fsummulc1f  46019  fsumf1of  46022  fsumiunss  46023  fsumreclf  46024  fsumlessf  46025  fsumsermpt  46027  dvnmul  46389  fourierdlem115  46667  sge0revalmpt  46824  sge0fsummpt  46836  sge0iunmptlemfi  46859  sge0iunmptlemre  46861  sge0ltfirpmpt2  46872  sge0isummpt2  46878  sge0xaddlem2  46880  sge0fsummptf  46882  fsummsndifre  47840  fsumsplitsndif  47841  fsummmodsndifre  47842  fsummmodsnunz  47843