Metamath Proof Explorer

Theorem sumeq1

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

Ref Expression
Assertion sumeq1 ⊢ A = B → ∑ k ∈ A C = ∑ k ∈ B C

Proof

Step Hyp Ref Expression
1 sseq1 ⊢ A = B → A ⊆ ℤ ≥ m ↔ B ⊆ ℤ ≥ m
2 simpl ⊢ A = B ∧ n ∈ ℤ → A = B
3 2 eleq2d ⊢ A = B ∧ n ∈ ℤ → n ∈ A ↔ n ∈ B
4 3 ifbid ⊢ A = B ∧ n ∈ ℤ → if n ∈ A ⦋ n / k⦌ C 0 = if n ∈ B ⦋ n / k⦌ C 0
5 4 mpteq2dva ⊢ A = B → n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ C 0 = n ∈ ℤ ⟼ if n ∈ B ⦋ n / k⦌ C 0
6 5 seqeq3d ⊢ A = B → seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ C 0 = seq m + n ∈ ℤ ⟼ if n ∈ B ⦋ n / k⦌ C 0
7 6 breq1d ⊢ A = B → seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ C 0 ⇝ x ↔ seq m + n ∈ ℤ ⟼ if n ∈ B ⦋ n / k⦌ C 0 ⇝ x
8 1 7 anbi12d ⊢ A = B → A ⊆ ℤ ≥ m ∧ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ C 0 ⇝ x ↔ B ⊆ ℤ ≥ m ∧ seq m + n ∈ ℤ ⟼ if n ∈ B ⦋ n / k⦌ C 0 ⇝ x
9 8 rexbidv ⊢ A = B → ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ C 0 ⇝ x ↔ ∃ m ∈ ℤ B ⊆ ℤ ≥ m ∧ seq m + n ∈ ℤ ⟼ if n ∈ B ⦋ n / k⦌ C 0 ⇝ x
10 f1oeq3 ⊢ A = B → f : 1 … m ⟶ 1-1 onto A ↔ f : 1 … m ⟶ 1-1 onto B
11 10 anbi1d ⊢ A = B → f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C ⁡ m ↔ f : 1 … m ⟶ 1-1 onto B ∧ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C ⁡ m
12 11 exbidv ⊢ A = B → ∃ f f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C ⁡ m ↔ ∃ f f : 1 … m ⟶ 1-1 onto B ∧ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C ⁡ m
13 12 rexbidv ⊢ A = B → ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C ⁡ m ↔ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto B ∧ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C ⁡ m
14 9 13 orbi12d ⊢ A = B → ∃ 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 ↔ ∃ m ∈ ℤ B ⊆ ℤ ≥ m ∧ seq m + n ∈ ℤ ⟼ if n ∈ B ⦋ n / k⦌ C 0 ⇝ x ∨ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto B ∧ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C ⁡ m
15 14 iotabidv ⊢ A = B → ι 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 = ι x | ∃ m ∈ ℤ B ⊆ ℤ ≥ m ∧ seq m + n ∈ ℤ ⟼ if n ∈ B ⦋ n / k⦌ C 0 ⇝ x ∨ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto B ∧ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C ⁡ m
16 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
17 df-sum ⊢ ∑ k ∈ B C = ι x | ∃ m ∈ ℤ B ⊆ ℤ ≥ m ∧ seq m + n ∈ ℤ ⟼ if n ∈ B ⦋ n / k⦌ C 0 ⇝ x ∨ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto B ∧ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C ⁡ m
18 15 16 17 3eqtr4g ⊢ A = B → ∑ k ∈ A C = ∑ k ∈ B C