Metamath Proof Explorer

Theorem cbvsum

Description: Change bound variable in a sum. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 13-Jun-2019)

Ref Expression
Hypotheses cbvsum.1 ⊢ j = k → B = C
cbvsum.2 ⊢ Ⅎ _ k A
cbvsum.3 ⊢ Ⅎ _ j A
cbvsum.4 ⊢ Ⅎ _ k B
cbvsum.5 ⊢ Ⅎ _ j C
Assertion cbvsum ⊢ ∑ j ∈ A B = ∑ k ∈ A C

Proof

Step Hyp Ref Expression
1 cbvsum.1 ⊢ j = k → B = C
2 cbvsum.2 ⊢ Ⅎ _ k A
3 cbvsum.3 ⊢ Ⅎ _ j A
4 cbvsum.4 ⊢ Ⅎ _ k B
5 cbvsum.5 ⊢ Ⅎ _ j C
6 4 5 1 cbvcsbw ⊢ ⦋ n / j⦌ B = ⦋ n / k⦌ C
7 6 a1i ⊢ ⊤ → ⦋ n / j⦌ B = ⦋ n / k⦌ C
8 7 ifeq1d ⊢ ⊤ → if n ∈ A ⦋ n / j⦌ B 0 = if n ∈ A ⦋ n / k⦌ C 0
9 8 mpteq2dv ⊢ ⊤ → n ∈ ℤ ⟼ if n ∈ A ⦋ n / j⦌ B 0 = n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ C 0
10 9 seqeq3d ⊢ ⊤ → seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / j⦌ B 0 = seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ C 0
11 10 mptru ⊢ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / j⦌ B 0 = seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ C 0
12 11 breq1i ⊢ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / j⦌ B 0 ⇝ x ↔ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ C 0 ⇝ x
13 12 anbi2i ⊢ A ⊆ ℤ ≥ m ∧ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / j⦌ B 0 ⇝ x ↔ A ⊆ ℤ ≥ m ∧ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ C 0 ⇝ x
14 13 rexbii ⊢ ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / j⦌ B 0 ⇝ x ↔ ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ C 0 ⇝ x
15 4 5 1 cbvcsbw ⊢ ⦋ f ⁡ n / j⦌ B = ⦋ f ⁡ n / k⦌ C
16 15 a1i ⊢ ⊤ → ⦋ f ⁡ n / j⦌ B = ⦋ f ⁡ n / k⦌ C
17 16 mpteq2dv ⊢ ⊤ → n ∈ ℕ ⟼ ⦋ f ⁡ n / j⦌ B = n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C
18 17 seqeq3d ⊢ ⊤ → seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / j⦌ B = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C
19 18 mptru ⊢ seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / j⦌ B = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C
20 19 fveq1i ⊢ seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / j⦌ B ⁡ m = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C ⁡ m
21 20 eqeq2i ⊢ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / j⦌ B ⁡ m ↔ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C ⁡ m
22 21 anbi2i ⊢ f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / j⦌ B ⁡ m ↔ f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C ⁡ m
23 22 exbii ⊢ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / j⦌ B ⁡ m ↔ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C ⁡ m
24 23 rexbii ⊢ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / j⦌ B ⁡ m ↔ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C ⁡ m
25 14 24 orbi12i ⊢ ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / j⦌ B 0 ⇝ x ∨ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / j⦌ 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
26 25 iotabii ⊢ ι x | ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / j⦌ B 0 ⇝ x ∨ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / j⦌ 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
27 df-sum ⊢ ∑ j ∈ A B = ι x | ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / j⦌ B 0 ⇝ x ∨ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / j⦌ B ⁡ m
28 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
29 26 27 28 3eqtr4i ⊢ ∑ j ∈ A B = ∑ k ∈ A C