Theorem cbvsum 15842

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 3857	. . . . . . . . . . . 12 ⊢ ⦋𝑛 / 𝑗⦌𝐵 = ⦋𝑛 / 𝑘⦌𝐶
5	4	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → ⦋𝑛 / 𝑗⦌𝐵 = ⦋𝑛 / 𝑘⦌𝐶)
6	5	ifeq1d 4502	. . . . . . . . . 10 ⊢ (⊤ → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑗⦌𝐵, 0) = if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))
7	6	mpteq2dv 5199	. . . . . . . . 9 ⊢ (⊤ → (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑗⦌𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0)))
8	7	seqeq3d 14132	. . . . . . . 8 ⊢ (⊤ → seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑗⦌𝐵, 0))) = seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))))
9	8	mptru 1577	. . . . . . 7 ⊢ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑗⦌𝐵, 0))) = seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0)))
10	9	breq1i 5110	. . . . . 6 ⊢ (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑗⦌𝐵, 0))) ⇝ 𝑥 ↔ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥)
11	10	anbi2i 635	. . . . 5 ⊢ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑗⦌𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥))
12	11	rexbii 3110	. . . 4 ⊢ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑗⦌𝐵, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥))
13	1, 2, 3	cbvcsbw 3857	. . . . . . . . . . . . 13 ⊢ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵 = ⦋(𝑓‘𝑛) / 𝑘⦌𝐶
14	13	a1i 11	. . . . . . . . . . . 12 ⊢ (⊤ → ⦋(𝑓‘𝑛) / 𝑗⦌𝐵 = ⦋(𝑓‘𝑛) / 𝑘⦌𝐶)
15	14	mpteq2dv 5199	. . . . . . . . . . 11 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵) = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))
16	15	seqeq3d 14132	. . . . . . . . . 10 ⊢ (⊤ → seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵)) = seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶)))
17	16	mptru 1577	. . . . . . . . 9 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵)) = seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))
18	17	fveq1i 6878	. . . . . . . 8 ⊢ (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)
19	18	eqeq2i 2774	. . . . . . 7 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵))‘𝑚) ↔ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))
20	19	anbi2i 635	. . . . . 6 ⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))
21	20	exbii 1881	. . . . 5 ⊢ (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))
22	21	rexbii 3110	. . . 4 ⊢ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))
23	12, 22	orbi12i 928	. . 3 ⊢ ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑗⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵))‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
24	23	iotabii 6516	. 2 ⊢ (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑗⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵))‘𝑚)))) = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
25		df-sum 15834	. 2 ⊢ Σ𝑗 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑗⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵))‘𝑚))))
26		df-sum 15834	. 2 ⊢ Σ𝑘 ∈ 𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
27	24, 25, 26	3eqtr4i 2794	1 ⊢ Σ𝑗 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861   = wceq 1570  ⊤wtru 1571  ∃wex 1812   ∈ wcel 2145  Ⅎwnfc 2908  ∃wrex 3087  ⦋csb 3847   ⊆ wss 3899  ifcif 4482   class class class wbr 5103   ↦ cmpt 5186  ℩cio 6485  –1-1-onto→wf1o 6530  ‘cfv 6531  (class class class)co 7412  0cc0 11181  1c1 11182   + caddc 11184  ℕcn 12316  ℤcz 12674  ℤ_≥cuz 12946  ...cfz 13620  seqcseq 14124   ⇝ cli 15631  Σcsu 15833

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-11 2194  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-xp 5657  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-iota 6487  df-fv 6539  df-ov 7415  df-oprab 7416  df-mpo 7417  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-seq 14125  df-sum 15834

This theorem is used by:  sumfc  15855  sumss2  15872  fsumclf  15884  fsumzcl2  15885  fsumsplitf  15888  sumsnf  15889  sumsns  15896  fsummsnunz  15900  fsumsplitsnun  15901  fsum2dlem  15916  fsumcom2  15920  fsumshftm  15927  fsumrlim  15958  fsumo1  15959  o1fsum  15960  fsumiun  15968  ovolfiniun  25802  ovoliun2  25807  volfiniun  25848  itgfsum  26127  elplyd  26500  coeeq2  26541  fsumdvdscom  27494  fsumdvdsmul  27504  fsumvma  27522  fsumiunle  33402  esumpfinvalf  34690  fsumshftd  39977  sticksstones8  43171  sticksstones10  43173  sticksstones12a  43175  sticksstones12  43176  aks6d1c7lem3  43200  binomcxplemdvsum  45298  sumsnd  45986  fsummulc1f  46527  fsumf1of  46530  fsumiunss  46531  fsumreclf  46532  fsumlessf  46533  fsumsermpt  46535  dvnmul  46897  fourierdlem115  47175  sge0revalmpt  47332  sge0fsummpt  47344  sge0iunmptlemfi  47367  sge0iunmptlemre  47369  sge0ltfirpmpt2  47380  sge0isummpt2  47386  sge0xaddlem2  47388  sge0fsummptf  47390  fsummsndifre  48394  fsumsplitsndif  48395  fsummmodsndifre  48396  fsummmodsnunz  48397