Description: Equality deduction for sum. (Contributed by NM, 1-Dec-2005)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sumeq12rdv.1 | ⊢ ( 𝜑 → 𝐴 = 𝐵 ) | |
sumeq12rdv.2 | ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 = 𝐷 ) | ||
Assertion | sumeq12rdv | ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝐵 𝐷 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sumeq12rdv.1 | ⊢ ( 𝜑 → 𝐴 = 𝐵 ) | |
2 | sumeq12rdv.2 | ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 = 𝐷 ) | |
3 | 1 | sumeq1d | ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝐵 𝐶 ) |
4 | 2 | sumeq2dv | ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑘 ∈ 𝐵 𝐷 ) |
5 | 3 4 | eqtrd | ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝐵 𝐷 ) |