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	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐶 = Σ* 𝑘 ∈ 𝐵 𝐷 )