# 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 ( 𝐴 = 𝐵 → Σ 𝑘𝐴 𝐶 = Σ 𝑘𝐵 𝐶 )

### Proof

Step Hyp Ref Expression
1 sseq1 ( 𝐴 = 𝐵 → ( 𝐴 ⊆ ( ℤ𝑚 ) ↔ 𝐵 ⊆ ( ℤ𝑚 ) ) )
2 simpl ( ( 𝐴 = 𝐵𝑛 ∈ ℤ ) → 𝐴 = 𝐵 )
3 2 eleq2d ( ( 𝐴 = 𝐵𝑛 ∈ ℤ ) → ( 𝑛𝐴𝑛𝐵 ) )
4 3 ifbid ( ( 𝐴 = 𝐵𝑛 ∈ ℤ ) → if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) = if ( 𝑛𝐵 , 𝑛 / 𝑘 𝐶 , 0 ) )
5 4 mpteq2dva ( 𝐴 = 𝐵 → ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) = ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐵 , 𝑛 / 𝑘 𝐶 , 0 ) ) )
6 5 seqeq3d ( 𝐴 = 𝐵 → seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) = seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐵 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) )
7 6 breq1d ( 𝐴 = 𝐵 → ( seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ↔ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐵 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ) )
8 1 7 anbi12d ( 𝐴 = 𝐵 → ( ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ↔ ( 𝐵 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐵 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ) )
9 8 rexbidv ( 𝐴 = 𝐵 → ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ↔ ∃ 𝑚 ∈ ℤ ( 𝐵 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐵 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ) )
10 f1oeq3 ( 𝐴 = 𝐵 → ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐵 ) )
11 10 anbi1d ( 𝐴 = 𝐵 → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐵𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) )
12 11 exbidv ( 𝐴 = 𝐵 → ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐵𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) )
13 12 rexbidv ( 𝐴 = 𝐵 → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐵𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) )
14 9 13 orbi12d ( 𝐴 = 𝐵 → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) ↔ ( ∃ 𝑚 ∈ ℤ ( 𝐵 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐵 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐵𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) ) )
15 14 iotabidv ( 𝐴 = 𝐵 → ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) ) = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐵 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐵 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐵𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) ) )
16 df-sum Σ 𝑘𝐴 𝐶 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) )
17 df-sum Σ 𝑘𝐵 𝐶 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐵 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐵 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐵𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) )
18 15 16 17 3eqtr4g ( 𝐴 = 𝐵 → Σ 𝑘𝐴 𝐶 = Σ 𝑘𝐵 𝐶 )