# 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 ( 𝑗 = 𝑘𝐵 = 𝐶 )
cbvsum.2 𝑘 𝐴
cbvsum.3 𝑗 𝐴
cbvsum.4 𝑘 𝐵
cbvsum.5 𝑗 𝐶
Assertion cbvsum Σ 𝑗𝐴 𝐵 = Σ 𝑘𝐴 𝐶

### Proof

Step Hyp Ref Expression
1 cbvsum.1 ( 𝑗 = 𝑘𝐵 = 𝐶 )
2 cbvsum.2 𝑘 𝐴
3 cbvsum.3 𝑗 𝐴
4 cbvsum.4 𝑘 𝐵
5 cbvsum.5 𝑗 𝐶
6 4 5 1 cbvcsbw 𝑛 / 𝑗 𝐵 = 𝑛 / 𝑘 𝐶
7 6 a1i ( ⊤ → 𝑛 / 𝑗 𝐵 = 𝑛 / 𝑘 𝐶 )
8 7 ifeq1d ( ⊤ → if ( 𝑛𝐴 , 𝑛 / 𝑗 𝐵 , 0 ) = if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) )
9 8 mpteq2dv ( ⊤ → ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑗 𝐵 , 0 ) ) = ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) )
10 9 seqeq3d ( ⊤ → seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑗 𝐵 , 0 ) ) ) = seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) )
11 10 mptru seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑗 𝐵 , 0 ) ) ) = seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) )
12 11 breq1i ( seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑗 𝐵 , 0 ) ) ) ⇝ 𝑥 ↔ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 )
13 12 anbi2i ( ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑗 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ↔ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ) )
14 13 rexbii ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑗 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ↔ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ) )
15 4 5 1 cbvcsbw ( 𝑓𝑛 ) / 𝑗 𝐵 = ( 𝑓𝑛 ) / 𝑘 𝐶
16 15 a1i ( ⊤ → ( 𝑓𝑛 ) / 𝑗 𝐵 = ( 𝑓𝑛 ) / 𝑘 𝐶 )
17 16 mpteq2dv ( ⊤ → ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) = ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) )
18 17 seqeq3d ( ⊤ → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) )
19 18 mptru seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) )
20 19 fveq1i ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) ) ‘ 𝑚 ) = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 )
21 20 eqeq2i ( 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) ) ‘ 𝑚 ) ↔ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) )
22 21 anbi2i ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) )
23 22 exbii ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) )
24 23 rexbii ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) )
25 14 24 orbi12i ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑗 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) ) ‘ 𝑚 ) ) ) ↔ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) )
26 25 iotabii ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑗 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) ) ‘ 𝑚 ) ) ) ) = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) )
27 df-sum Σ 𝑗𝐴 𝐵 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑗 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) ) ‘ 𝑚 ) ) ) )
28 df-sum Σ 𝑘𝐴 𝐶 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) )
29 26 27 28 3eqtr4i Σ 𝑗𝐴 𝐵 = Σ 𝑘𝐴 𝐶