Metamath Proof Explorer

Theorem sumeq2w

Description: Equality theorem for sum, when the class expressions B and C are equal everywhere. Proved using only Extensionality. (Contributed by Mario Carneiro, 24-Jun-2014) (Revised by Mario Carneiro, 13-Jun-2019)

Ref Expression
Assertion sumeq2w ( ∀ 𝑘 𝐵 = 𝐶 → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 csbeq2 ⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ⦋ 𝑛 / 𝑘 ⦌ 𝐵 = ⦋ 𝑛 / 𝑘 ⦌ 𝐶 )
2 1 ifeq1d ⊢ ( ∀ 𝑘 𝐵 = 𝐶 → if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) = if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) )
3 2 mpteq2dv ⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) = ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) )
4 3 seqeq3d ⊢ ( ∀ 𝑘 𝐵 = 𝐶 → seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) = seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) ) )
5 4 breq1d ⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ↔ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) ) ⇝ 𝑥 ) )
6 5 anbi2d ⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ↔ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ) )
7 6 rexbidv ⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ↔ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ) )
8 csbeq2 ⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 )
9 8 mpteq2dv ⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) = ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) )
10 9 seqeq3d ⊢ ( ∀ 𝑘 𝐵 = 𝐶 → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) )
11 10 fveq1d ⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) )
12 11 eqeq2d ⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ↔ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) )
13 12 anbi2d ⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) )
14 13 exbidv ⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) )
15 14 rexbidv ⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) )
16 7 15 orbi12d ⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ↔ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) ) )
17 16 iotabidv ⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ) = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) ) )
18 df-sum ⊢ Σ 𝑘 ∈ 𝐴 𝐵 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) )
19 df-sum ⊢ Σ 𝑘 ∈ 𝐴 𝐶 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) )
20 17 18 19 3eqtr4g ⊢ ( ∀ 𝑘 𝐵 = 𝐶 → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 𝐶 )