Metamath Proof Explorer

Theorem esumpfinvalf

Description: Same as esumpfinval , minus distinct variable restrictions. (Contributed by Thierry Arnoux, 28-Aug-2017) (Proof shortened by AV, 25-Jul-2019)

Ref Expression
Hypotheses esumpfinvalf.1 ⊢ Ⅎ 𝑘 𝐴
esumpfinvalf.2 ⊢ Ⅎ 𝑘 𝜑
esumpfinvalf.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
esumpfinvalf.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
Assertion esumpfinvalf ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 esumpfinvalf.1 ⊢ Ⅎ 𝑘 𝐴
2 esumpfinvalf.2 ⊢ Ⅎ 𝑘 𝜑
3 esumpfinvalf.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
4 esumpfinvalf.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
5 df-esum ⊢ Σ* 𝑘 ∈ 𝐴 𝐵 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
6 xrge0base ⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
7 xrge00 ⊢ 0 = ( 0g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
8 xrge0cmn ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd
9 8 a1i ⊢ ( 𝜑 → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd )
10 xrge0tps ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopSp
11 10 a1i ⊢ ( 𝜑 → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopSp )
12 nfcv ⊢ Ⅎ 𝑘 ( 0 [,] +∞ )
13 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
14 13 4 sseldi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
15 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
16 2 1 12 14 15 fmptdF ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
17 c0ex ⊢ 0 ∈ V
18 17 a1i ⊢ ( 𝜑 → 0 ∈ V )
19 16 3 18 fdmfifsupp ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) finSupp 0 )
20 xrge0topn ⊢ ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )
21 20 eqcomi ⊢ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) = ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
22 xrhaus ⊢ ( ordTop ‘ ≤ ) ∈ Haus
23 ovex ⊢ ( 0 [,] +∞ ) ∈ V
24 resthaus ⊢ ( ( ( ordTop ‘ ≤ ) ∈ Haus ∧ ( 0 [,] +∞ ) ∈ V ) → ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ∈ Haus )
25 22 23 24 mp2an ⊢ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ∈ Haus
26 25 a1i ⊢ ( 𝜑 → ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ∈ Haus )
27 6 7 9 11 3 16 19 21 26 haustsmsid ⊢ ( 𝜑 → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = { ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) } )
28 27 unieqd ⊢ ( 𝜑 → ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ∪ { ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) } )
29 5 28 syl5eq ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = ∪ { ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) } )
30 ovex ⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ V
31 30 unisn ⊢ ∪ { ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) } = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
32 29 31 eqtrdi ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
33 nfcv ⊢ Ⅎ 𝑘 ( 0 [,) +∞ )
34 2 1 33 4 15 fmptdF ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,) +∞ ) )
35 esumpfinvallem ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,) +∞ ) ) → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
36 3 34 35 syl2anc ⊢ ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
37 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
38 ax-resscn ⊢ ℝ ⊆ ℂ
39 37 38 sstri ⊢ ( 0 [,) +∞ ) ⊆ ℂ
40 39 4 sseldi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
41 40 sbt ⊢ [ 𝑙 / 𝑘 ] ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
42 sbim ⊢ ( [ 𝑙 / 𝑘 ] ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) ↔ ( [ 𝑙 / 𝑘 ] ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → [ 𝑙 / 𝑘 ] 𝐵 ∈ ℂ ) )
43 sban ⊢ ( [ 𝑙 / 𝑘 ] ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ↔ ( [ 𝑙 / 𝑘 ] 𝜑 ∧ [ 𝑙 / 𝑘 ] 𝑘 ∈ 𝐴 ) )
44 2 sbf ⊢ ( [ 𝑙 / 𝑘 ] 𝜑 ↔ 𝜑 )
45 1 clelsb3fw ⊢ ( [ 𝑙 / 𝑘 ] 𝑘 ∈ 𝐴 ↔ 𝑙 ∈ 𝐴 )
46 44 45 anbi12i ⊢ ( ( [ 𝑙 / 𝑘 ] 𝜑 ∧ [ 𝑙 / 𝑘 ] 𝑘 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑙 ∈ 𝐴 ) )
47 43 46 bitri ⊢ ( [ 𝑙 / 𝑘 ] ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑙 ∈ 𝐴 ) )
48 sbsbc ⊢ ( [ 𝑙 / 𝑘 ] 𝐵 ∈ ℂ ↔ [ 𝑙 / 𝑘 ] 𝐵 ∈ ℂ )
49 sbcel1g ⊢ ( 𝑙 ∈ V → ( [ 𝑙 / 𝑘 ] 𝐵 ∈ ℂ ↔ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
50 49 elv ⊢ ( [ 𝑙 / 𝑘 ] 𝐵 ∈ ℂ ↔ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∈ ℂ )
51 48 50 bitri ⊢ ( [ 𝑙 / 𝑘 ] 𝐵 ∈ ℂ ↔ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∈ ℂ )
52 47 51 imbi12i ⊢ ( ( [ 𝑙 / 𝑘 ] ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → [ 𝑙 / 𝑘 ] 𝐵 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑙 ∈ 𝐴 ) → ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
53 42 52 bitri ⊢ ( [ 𝑙 / 𝑘 ] ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑙 ∈ 𝐴 ) → ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
54 41 53 mpbi ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝐴 ) → ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∈ ℂ )
55 3 54 gsumfsum ⊢ ( 𝜑 → ( ℂfld Σg ( 𝑙 ∈ 𝐴 ↦ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) ) = Σ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑘 ⦌ 𝐵 )
56 nfcv ⊢ Ⅎ 𝑙 𝐴
57 nfcv ⊢ Ⅎ 𝑙 𝐵
58 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑙 / 𝑘 ⦌ 𝐵
59 csbeq1a ⊢ ( 𝑘 = 𝑙 → 𝐵 = ⦋ 𝑙 / 𝑘 ⦌ 𝐵 )
60 1 56 57 58 59 cbvmptf ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑙 ∈ 𝐴 ↦ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 )
61 60 oveq2i ⊢ ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( ℂfld Σg ( 𝑙 ∈ 𝐴 ↦ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) )
62 59 56 1 57 58 cbvsum ⊢ Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑘 ⦌ 𝐵
63 55 61 62 3eqtr4g ⊢ ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = Σ 𝑘 ∈ 𝐴 𝐵 )
64 32 36 63 3eqtr2d ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 𝐵 )