Metamath Proof Explorer


Theorem esumeq12dvaf

Description: Equality deduction for extended sum. (Contributed by Thierry Arnoux, 26-Mar-2017)

Ref Expression
Hypotheses esumeq12dvaf.1 𝑘 𝜑
esumeq12dvaf.2 ( 𝜑𝐴 = 𝐵 )
esumeq12dvaf.3 ( ( 𝜑𝑘𝐴 ) → 𝐶 = 𝐷 )
Assertion esumeq12dvaf ( 𝜑 → Σ* 𝑘𝐴 𝐶 = Σ* 𝑘𝐵 𝐷 )

Proof

Step Hyp Ref Expression
1 esumeq12dvaf.1 𝑘 𝜑
2 esumeq12dvaf.2 ( 𝜑𝐴 = 𝐵 )
3 esumeq12dvaf.3 ( ( 𝜑𝑘𝐴 ) → 𝐶 = 𝐷 )
4 1 2 alrimi ( 𝜑 → ∀ 𝑘 𝐴 = 𝐵 )
5 3 ex ( 𝜑 → ( 𝑘𝐴𝐶 = 𝐷 ) )
6 1 5 ralrimi ( 𝜑 → ∀ 𝑘𝐴 𝐶 = 𝐷 )
7 mpteq12f ( ( ∀ 𝑘 𝐴 = 𝐵 ∧ ∀ 𝑘𝐴 𝐶 = 𝐷 ) → ( 𝑘𝐴𝐶 ) = ( 𝑘𝐵𝐷 ) )
8 4 6 7 syl2anc ( 𝜑 → ( 𝑘𝐴𝐶 ) = ( 𝑘𝐵𝐷 ) )
9 8 oveq2d ( 𝜑 → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐴𝐶 ) ) = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐵𝐷 ) ) )
10 9 unieqd ( 𝜑 ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐴𝐶 ) ) = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐵𝐷 ) ) )
11 df-esum Σ* 𝑘𝐴 𝐶 = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐴𝐶 ) )
12 df-esum Σ* 𝑘𝐵 𝐷 = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐵𝐷 ) )
13 10 11 12 3eqtr4g ( 𝜑 → Σ* 𝑘𝐴 𝐶 = Σ* 𝑘𝐵 𝐷 )