Theorem sumeq1 15631

Description: Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)

Assertion

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

Proof of Theorem sumeq1

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

Step	Hyp	Ref	Expression
1		sseq1 4006	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ (ℤ≥‘𝑚) ↔ 𝐵 ⊆ (ℤ≥‘𝑚)))
2		simpl 483	. . . . . . . . . . 11 ⊢ ((𝐴 = 𝐵 ∧ 𝑛 ∈ ℤ) → 𝐴 = 𝐵)
3	2	eleq2d 2819	. . . . . . . . . 10 ⊢ ((𝐴 = 𝐵 ∧ 𝑛 ∈ ℤ) → (𝑛 ∈ 𝐴 ↔ 𝑛 ∈ 𝐵))
4	3	ifbid 4550	. . . . . . . . 9 ⊢ ((𝐴 = 𝐵 ∧ 𝑛 ∈ ℤ) → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0) = if(𝑛 ∈ 𝐵, ⦋𝑛 / 𝑘⦌𝐶, 0))
5	4	mpteq2dva 5247	. . . . . . . 8 ⊢ (𝐴 = 𝐵 → (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐵, ⦋𝑛 / 𝑘⦌𝐶, 0)))
6	5	seqeq3d 13970	. . . . . . 7 ⊢ (𝐴 = 𝐵 → seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) = seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐵, ⦋𝑛 / 𝑘⦌𝐶, 0))))
7	6	breq1d 5157	. . . . . 6 ⊢ (𝐴 = 𝐵 → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥 ↔ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐵, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥))
8	1, 7	anbi12d 631	. . . . 5 ⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥) ↔ (𝐵 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐵, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥)))
9	8	rexbidv 3178	. . . 4 ⊢ (𝐴 = 𝐵 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐵, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥)))
10		f1oeq3 6820	. . . . . . 7 ⊢ (𝐴 = 𝐵 → (𝑓:(1...𝑚)–1-1-onto→𝐴 ↔ 𝑓:(1...𝑚)–1-1-onto→𝐵))
11	10	anbi1d 630	. . . . . 6 ⊢ (𝐴 = 𝐵 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐵 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
12	11	exbidv 1924	. . . . 5 ⊢ (𝐴 = 𝐵 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐵 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
13	12	rexbidv 3178	. . . 4 ⊢ (𝐴 = 𝐵 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐵 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
14	9, 13	orbi12d 917	. . 3 ⊢ (𝐴 = 𝐵 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐵, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐵 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))))
15	14	iotabidv 6524	. 2 ⊢ (𝐴 = 𝐵 → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))) = (℩𝑥(∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐵, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐵 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))))
16		df-sum 15629	. 2 ⊢ Σ𝑘 ∈ 𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
17		df-sum 15629	. 2 ⊢ Σ𝑘 ∈ 𝐵 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐵, ⦋𝑛 / 𝑘⦌𝐶, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐵 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
18	15, 16, 17	3eqtr4g 2797	1 ⊢ (𝐴 = 𝐵 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   ∨ wo 845   = wceq 1541  ∃wex 1781   ∈ wcel 2106  ∃wrex 3070  ⦋csb 3892   ⊆ wss 3947  ifcif 4527   class class class wbr 5147   ↦ cmpt 5230  ℩cio 6490  –1-1-onto→wf1o 6539  ‘cfv 6540  (class class class)co 7405  0cc0 11106  1c1 11107   + caddc 11109  ℕcn 12208  ℤcz 12554  ℤ_≥cuz 12818  ...cfz 13480  seqcseq 13962   ⇝ cli 15424  Σcsu 15628

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-xp 5681  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-iota 6492  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-seq 13963  df-sum 15629

This theorem is referenced by:  sumeq1i  15640  sumeq1d  15643  sumz  15664  fsumadd  15682  fsum2d  15713  fsumrev2  15724  fsummulc2  15726  fsumconst  15732  modfsummods  15735  modfsummod  15736  fsumabs  15743  fsumrelem  15749  fsumrlim  15753  fsumo1  15754  fsumiun  15763  sumeven  16326  sumodd  16327  bitsinv2  16380  bitsf1ocnv  16381  bitsinv  16385  prmreclem5  16849  gsumfsum  21004  fsumcn  24377  ovolfiniun  25009  volfiniun  25055  itgfsum  25335  dvmptfsum  25483  pntrsumbnd2  27059  finsumvtxdg2size  28796  esumpcvgval  33064  esumcvg  33072  rrnval  36683  mccl  44300  dvmptfprod  44647  dvnprodlem1  44648  dvnprodlem2  44649  dvnprodlem3  44650  dvnprod  44651  sge0rnn0  45070  sge00  45078  fsumlesge0  45079  sge0sn  45081  sge0cl  45083  sge0f1o  45084  sge0resplit  45108  sge0xaddlem1  45135  sge0xaddlem2  45136  sge0reuz  45149