Step |
Hyp |
Ref |
Expression |
1 |
|
cbvesum.1 |
⊢ ( 𝑗 = 𝑘 → 𝐵 = 𝐶 ) |
2 |
|
cbvesum.2 |
⊢ Ⅎ 𝑘 𝐴 |
3 |
|
cbvesum.3 |
⊢ Ⅎ 𝑗 𝐴 |
4 |
|
cbvesum.4 |
⊢ Ⅎ 𝑘 𝐵 |
5 |
|
cbvesum.5 |
⊢ Ⅎ 𝑗 𝐶 |
6 |
3 2 4 5 1
|
cbvmptf |
⊢ ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) |
7 |
6
|
oveq2i |
⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) |
8 |
7
|
unieqi |
⊢ ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) |
9 |
|
df-esum |
⊢ Σ* 𝑗 ∈ 𝐴 𝐵 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) |
10 |
|
df-esum |
⊢ Σ* 𝑘 ∈ 𝐴 𝐶 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) |
11 |
8 9 10
|
3eqtr4i |
⊢ Σ* 𝑗 ∈ 𝐴 𝐵 = Σ* 𝑘 ∈ 𝐴 𝐶 |