Metamath Proof Explorer

Theorem sumeq2w

Description: Equality theorem for sum, when the class expressions B and C are equal everywhere. Proved using only Extensionality. (Contributed by Mario Carneiro, 24-Jun-2014) (Revised by Mario Carneiro, 13-Jun-2019)

Ref Expression
Assertion sumeq2w ⊢∀kB=C→∑k∈AB=∑k∈AC

Proof

Step Hyp Ref Expression
1 csbeq2 ⊢∀kB=C→⦋n/k⦌B=⦋n/k⦌C
2 1 ifeq1d ⊢∀kB=C→ifn∈A⦋n/k⦌B0=ifn∈A⦋n/k⦌C0
3 2 mpteq2dv ⊢∀kB=C→n∈ℤ⟼ifn∈A⦋n/k⦌B0=n∈ℤ⟼ifn∈A⦋n/k⦌C0
4 3 seqeq3d ⊢∀kB=C→seqm+n∈ℤ⟼ifn∈A⦋n/k⦌B0=seqm+n∈ℤ⟼ifn∈A⦋n/k⦌C0
5 4 breq1d ⊢∀kB=C→seqm+n∈ℤ⟼ifn∈A⦋n/k⦌B0⇝x↔seqm+n∈ℤ⟼ifn∈A⦋n/k⦌C0⇝x
6 5 anbi2d ⊢∀kB=C→A⊆ℤ≥m∧seqm+n∈ℤ⟼ifn∈A⦋n/k⦌B0⇝x↔A⊆ℤ≥m∧seqm+n∈ℤ⟼ifn∈A⦋n/k⦌C0⇝x
7 6 rexbidv ⊢∀kB=C→∃m∈ℤA⊆ℤ≥m∧seqm+n∈ℤ⟼ifn∈A⦋n/k⦌B0⇝x↔∃m∈ℤA⊆ℤ≥m∧seqm+n∈ℤ⟼ifn∈A⦋n/k⦌C0⇝x
8 csbeq2 ⊢∀kB=C→⦋f⁡n/k⦌B=⦋f⁡n/k⦌C
9 8 mpteq2dv ⊢∀kB=C→n∈ℕ⟼⦋f⁡n/k⦌B=n∈ℕ⟼⦋f⁡n/k⦌C
10 9 seqeq3d ⊢∀kB=C→seq1+n∈ℕ⟼⦋f⁡n/k⦌B=seq1+n∈ℕ⟼⦋f⁡n/k⦌C
11 10 fveq1d ⊢∀kB=C→seq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m=seq1+n∈ℕ⟼⦋f⁡n/k⦌C⁡m
12 11 eqeq2d ⊢∀kB=C→x=seq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m↔x=seq1+n∈ℕ⟼⦋f⁡n/k⦌C⁡m
13 12 anbi2d ⊢∀kB=C→f:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m↔f:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌C⁡m
14 13 exbidv ⊢∀kB=C→∃ff:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m↔∃ff:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌C⁡m
15 14 rexbidv ⊢∀kB=C→∃m∈ℕ∃ff:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m↔∃m∈ℕ∃ff:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌C⁡m
16 7 15 orbi12d ⊢∀kB=C→∃m∈ℤA⊆ℤ≥m∧seqm+n∈ℤ⟼ifn∈A⦋n/k⦌B0⇝x∨∃m∈ℕ∃ff:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m↔∃m∈ℤA⊆ℤ≥m∧seqm+n∈ℤ⟼ifn∈A⦋n/k⦌C0⇝x∨∃m∈ℕ∃ff:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌C⁡m
17 16 iotabidv ⊢∀kB=C→ιx|∃m∈ℤA⊆ℤ≥m∧seqm+n∈ℤ⟼ifn∈A⦋n/k⦌B0⇝x∨∃m∈ℕ∃ff:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m=ιx|∃m∈ℤA⊆ℤ≥m∧seqm+n∈ℤ⟼ifn∈A⦋n/k⦌C0⇝x∨∃m∈ℕ∃ff:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌C⁡m
18 df-sum ⊢∑k∈AB=ιx|∃m∈ℤA⊆ℤ≥m∧seqm+n∈ℤ⟼ifn∈A⦋n/k⦌B0⇝x∨∃m∈ℕ∃ff:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m
19 df-sum ⊢∑k∈AC=ιx|∃m∈ℤA⊆ℤ≥m∧seqm+n∈ℤ⟼ifn∈A⦋n/k⦌C0⇝x∨∃m∈ℕ∃ff:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌C⁡m
20 17 18 19 3eqtr4g ⊢∀kB=C→∑k∈AB=∑k∈AC