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 ⊢ ∀ k B = C → ∑ k ∈ A B = ∑ k ∈ A C

Proof

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