Step |
Hyp |
Ref |
Expression |
1 |
|
esumpfinval.a |
⊢ ( 𝜑 → 𝐴 ∈ Fin ) |
2 |
|
esumpfinval.b |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) ) |
3 |
|
df-esum |
⊢ Σ* 𝑘 ∈ 𝐴 𝐵 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) |
4 |
|
xrge0base |
⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) |
5 |
|
xrge00 |
⊢ 0 = ( 0g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) |
6 |
|
xrge0cmn |
⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd |
7 |
6
|
a1i |
⊢ ( 𝜑 → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd ) |
8 |
|
xrge0tps |
⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopSp |
9 |
8
|
a1i |
⊢ ( 𝜑 → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopSp ) |
10 |
|
icossicc |
⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) |
11 |
10 2
|
sselid |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) ) |
12 |
11
|
fmpttd |
⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) ) |
13 |
|
eqid |
⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) |
14 |
|
c0ex |
⊢ 0 ∈ V |
15 |
14
|
a1i |
⊢ ( 𝜑 → 0 ∈ V ) |
16 |
13 1 2 15
|
fsuppmptdm |
⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) finSupp 0 ) |
17 |
|
xrge0topn |
⊢ ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) |
18 |
17
|
eqcomi |
⊢ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) = ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) |
19 |
|
xrhaus |
⊢ ( ordTop ‘ ≤ ) ∈ Haus |
20 |
|
ovex |
⊢ ( 0 [,] +∞ ) ∈ V |
21 |
|
resthaus |
⊢ ( ( ( ordTop ‘ ≤ ) ∈ Haus ∧ ( 0 [,] +∞ ) ∈ V ) → ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ∈ Haus ) |
22 |
19 20 21
|
mp2an |
⊢ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ∈ Haus |
23 |
22
|
a1i |
⊢ ( 𝜑 → ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ∈ Haus ) |
24 |
4 5 7 9 1 12 16 18 23
|
haustsmsid |
⊢ ( 𝜑 → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = { ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) } ) |
25 |
24
|
unieqd |
⊢ ( 𝜑 → ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ∪ { ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) } ) |
26 |
3 25
|
eqtrid |
⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = ∪ { ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) } ) |
27 |
|
ovex |
⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ V |
28 |
27
|
unisn |
⊢ ∪ { ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) } = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) |
29 |
26 28
|
eqtrdi |
⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ) |
30 |
2
|
fmpttd |
⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,) +∞ ) ) |
31 |
|
esumpfinvallem |
⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,) +∞ ) ) → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ) |
32 |
1 30 31
|
syl2anc |
⊢ ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ) |
33 |
|
rge0ssre |
⊢ ( 0 [,) +∞ ) ⊆ ℝ |
34 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
35 |
33 34
|
sstri |
⊢ ( 0 [,) +∞ ) ⊆ ℂ |
36 |
35 2
|
sselid |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) |
37 |
1 36
|
gsumfsum |
⊢ ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = Σ 𝑘 ∈ 𝐴 𝐵 ) |
38 |
29 32 37
|
3eqtr2d |
⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 𝐵 ) |