Metamath Proof Explorer


Theorem sumeq12i

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 Σ 𝑘𝐴 𝐶 = Σ 𝑘𝐵 𝐷