Metamath Proof Explorer

Theorem sumeq2si

Description: Equality inference for sum. (Contributed by GG, 1-Sep-2025)

Ref Expression
Hypothesis sumeq2si.1 ⊢ B = C
Assertion sumeq2si ⊢ ∑ k ∈ A B = ∑ k ∈ A C

Proof

Step Hyp Ref Expression
1 sumeq2si.1 ⊢ B = C
2 1 csbeq2i ⊢ ⦋ n / k⦌ B = ⦋ n / k⦌ C
3 ifeq1 ⊢ ⦋ n / k⦌ B = ⦋ n / k⦌ C → if n ∈ A ⦋ n / k⦌ B 0 = if n ∈ A ⦋ n / k⦌ C 0
4 2 3 ax-mp ⊢ if n ∈ A ⦋ n / k⦌ B 0 = if n ∈ A ⦋ n / k⦌ C 0
5 4 mpteq2i ⊢ n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ B 0 = n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ C 0
6 seqeq3 ⊢ n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ B 0 = n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ C 0 → seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ B 0 = seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ C 0
7 5 6 ax-mp ⊢ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ B 0 = seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ C 0
8 7 breq1i ⊢ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ B 0 ⇝ x ↔ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ C 0 ⇝ x
9 8 anbi2i ⊢ 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
10 9 rexbii ⊢ ∃ 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
11 1 csbeq2i ⊢ ⦋ f ⁡ n / k⦌ B = ⦋ f ⁡ n / k⦌ C
12 11 mpteq2i ⊢ n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B = n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C
13 seqeq3 ⊢ n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B = n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C → seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C
14 12 13 ax-mp ⊢ seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C
15 14 fveq1i ⊢ seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C ⁡ m
16 15 eqeq2i ⊢ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m ↔ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C ⁡ m
17 16 anbi2i ⊢ 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
18 17 exbii ⊢ ∃ 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
19 18 rexbii ⊢ ∃ 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
20 10 19 orbi12i ⊢ ∃ 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
21 20 iotabii ⊢ ι 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
22 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
23 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
24 21 22 23 3eqtr4i ⊢ ∑ k ∈ A B = ∑ k ∈ A C