Metamath Proof Explorer

Theorem esumss

Description: Change the index set to a subset by adding zeroes. (Contributed by Thierry Arnoux, 19-Jun-2017)

Ref Expression
Hypotheses esumss.p ⊢ Ⅎ 𝑘 𝜑
esumss.a ⊢ Ⅎ 𝑘 𝐴
esumss.b ⊢ Ⅎ 𝑘 𝐵
esumss.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
esumss.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
esumss.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
esumss.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 0 )
Assertion esumss ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐶 = Σ* 𝑘 ∈ 𝐵 𝐶 )

Proof

Step Hyp Ref Expression
1 esumss.p ⊢ Ⅎ 𝑘 𝜑
2 esumss.a ⊢ Ⅎ 𝑘 𝐴
3 esumss.b ⊢ Ⅎ 𝑘 𝐵
4 esumss.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
5 esumss.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
6 esumss.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
7 esumss.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 0 )
8 3 2 resmptf ⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ↾ 𝐴 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) )
9 4 8 syl ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ↾ 𝐴 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) )
10 9 oveq2d ⊢ ( 𝜑 → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ↾ 𝐴 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) )
11 xrge0base ⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
12 xrge00 ⊢ 0 = ( 0g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
13 xrge0cmn ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd
14 13 a1i ⊢ ( 𝜑 → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd )
15 xrge0tps ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopSp
16 15 a1i ⊢ ( 𝜑 → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopSp )
17 nfcv ⊢ Ⅎ 𝑘 ( 0 [,] +∞ )
18 eqid ⊢ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ 𝐵 ↦ 𝐶 )
19 1 3 17 6 18 fmptdF ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ ( 0 [,] +∞ ) )
20 1 3 2 7 5 suppss2f ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) supp 0 ) ⊆ 𝐴 )
21 11 12 14 16 5 19 20 tsmsres ⊢ ( 𝜑 → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ↾ 𝐴 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
22 10 21 eqtr3d ⊢ ( 𝜑 → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
23 22 unieqd ⊢ ( 𝜑 → ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
24 df-esum ⊢ Σ* 𝑘 ∈ 𝐴 𝐶 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) )
25 df-esum ⊢ Σ* 𝑘 ∈ 𝐵 𝐶 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) )
26 23 24 25 3eqtr4g ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐶 = Σ* 𝑘 ∈ 𝐵 𝐶 )