Metamath Proof Explorer
Description: Equality inference for sum. (Contributed by FL, 10-Dec-2006)
|
|
Ref |
Expression |
|
Hypotheses |
sumeq12i.1 |
⊢ 𝐴 = 𝐵 |
|
|
sumeq12i.2 |
⊢ ( 𝑘 ∈ 𝐴 → 𝐶 = 𝐷 ) |
|
Assertion |
sumeq12i |
⊢ Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝐵 𝐷 |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
sumeq12i.1 |
⊢ 𝐴 = 𝐵 |
2 |
|
sumeq12i.2 |
⊢ ( 𝑘 ∈ 𝐴 → 𝐶 = 𝐷 ) |
3 |
2
|
sumeq2i |
⊢ Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝐴 𝐷 |
4 |
1
|
sumeq1i |
⊢ Σ 𝑘 ∈ 𝐴 𝐷 = Σ 𝑘 ∈ 𝐵 𝐷 |
5 |
3 4
|
eqtri |
⊢ Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝐵 𝐷 |