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 B
cbvsum.3 ⊢ Ⅎ _ 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 B
3 cbvsum.3 ⊢ Ⅎ _ j C
4 2 3 1 cbvcsbw ⊢ ⦋ n / j⦌ B = ⦋ n / k⦌ C
5 4 a1i ⊢ ⊤ → ⦋ n / j⦌ B = ⦋ n / k⦌ C
6 5 ifeq1d ⊢ ⊤ → if n ∈ A ⦋ n / j⦌ B 0 = if n ∈ A ⦋ n / k⦌ C 0
7 6 mpteq2dv ⊢ ⊤ → n ∈ ℤ ⟼ if n ∈ A ⦋ n / j⦌ B 0 = n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ C 0
8 7 seqeq3d ⊢ ⊤ → seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / j⦌ B 0 = seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ C 0
9 8 mptru ⊢ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / j⦌ B 0 = seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ C 0
10 9 breq1i ⊢ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / j⦌ B 0 ⇝ x ↔ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ C 0 ⇝ x
11 10 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
12 11 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
13 2 3 1 cbvcsbw ⊢ ⦋ f ⁡ n / j⦌ B = ⦋ f ⁡ n / k⦌ C
14 13 a1i ⊢ ⊤ → ⦋ f ⁡ n / j⦌ B = ⦋ f ⁡ n / k⦌ C
15 14 mpteq2dv ⊢ ⊤ → n ∈ ℕ ⟼ ⦋ f ⁡ n / j⦌ B = n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C
16 15 seqeq3d ⊢ ⊤ → seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / j⦌ B = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C
17 16 mptru ⊢ seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / j⦌ B = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C
18 17 fveq1i ⊢ seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / j⦌ B ⁡ m = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C ⁡ m
19 18 eqeq2i ⊢ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / j⦌ B ⁡ m ↔ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ C ⁡ m
20 19 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
21 20 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
22 21 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
23 12 22 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
24 23 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
25 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
26 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
27 24 25 26 3eqtr4i ⊢ ∑ j ∈ A B = ∑ k ∈ A C