Step |
Hyp |
Ref |
Expression |
1 |
|
esumcl.1 |
⊢ Ⅎ 𝑘 𝐴 |
2 |
|
xrge0base |
⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) |
3 |
|
xrge0cmn |
⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd |
4 |
3
|
a1i |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd ) |
5 |
|
xrge0tps |
⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopSp |
6 |
5
|
a1i |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopSp ) |
7 |
|
simpl |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → 𝐴 ∈ 𝑉 ) |
8 |
1
|
nfel1 |
⊢ Ⅎ 𝑘 𝐴 ∈ 𝑉 |
9 |
|
nfra1 |
⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) |
10 |
8 9
|
nfan |
⊢ Ⅎ 𝑘 ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) |
11 |
|
nfcv |
⊢ Ⅎ 𝑘 ( 0 [,] +∞ ) |
12 |
|
simpr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) |
13 |
12
|
r19.21bi |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) ) |
14 |
|
eqid |
⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) |
15 |
10 1 11 13 14
|
fmptdF |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) ) |
16 |
2 4 6 7 15
|
tsmscl |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ⊆ ( 0 [,] +∞ ) ) |
17 |
|
df-esum |
⊢ Σ* 𝑘 ∈ 𝐴 𝐵 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) |
18 |
|
eqid |
⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) |
19 |
18 7 15
|
xrge0tsmsbi |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → ( Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ↔ Σ* 𝑘 ∈ 𝐴 𝐵 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ) ) |
20 |
17 19
|
mpbiri |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ) |
21 |
16 20
|
sseldd |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) |