Metamath Proof Explorer

Theorem sge0tsms

Description: sum^ applied to a nonnegative function (its meaningful domain) is the same as the infinite group sum (that's always convergent, in this case). (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0tsms.g ⊢ 𝐺 = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
sge0tsms.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
sge0tsms.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
Assertion sge0tsms ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ( 𝐺 tsums 𝐹 ) )

Proof

Step Hyp Ref Expression
1 sge0tsms.g ⊢ 𝐺 = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
2 sge0tsms.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
3 sge0tsms.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
4 eqid ⊢ sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < )
5 4 a1i ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) )
6 xrltso ⊢ < Or ℝ*
7 6 supex ⊢ sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) ∈ V
8 7 a1i ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) ∈ V )
9 elsng ⊢ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) ∈ V → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) ∈ { sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) } ↔ sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) ) )
10 8 9 syl ⊢ ( 𝜑 → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) ∈ { sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) } ↔ sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) ) )
11 5 10 mpbird ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) ∈ { sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) } )
12 2 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → 𝑋 ∈ 𝑉 )
13 3 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
14 simpr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → +∞ ∈ ran 𝐹 )
15 12 13 14 sge0pnfval ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐹 ) = +∞ )
16 3 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
17 16 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → 𝐹 Fn 𝑋 )
18 fvelrnb ⊢ ( 𝐹 Fn 𝑋 → ( +∞ ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) = +∞ ) )
19 17 18 syl ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ( +∞ ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) = +∞ ) )
20 14 19 mpbid ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ∃ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) = +∞ )
21 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
22 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) )
23 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
24 elinel1 ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑥 ∈ 𝒫 𝑋 )
25 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋 )
26 24 25 syl ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑥 ⊆ 𝑋 )
27 26 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑥 ⊆ 𝑋 )
28 fssres ⊢ ( ( 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝐹 ↾ 𝑥 ) : 𝑥 ⟶ ( 0 [,] +∞ ) )
29 23 27 28 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( 𝐹 ↾ 𝑥 ) : 𝑥 ⟶ ( 0 [,] +∞ ) )
30 elinel2 ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑥 ∈ Fin )
31 30 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑥 ∈ Fin )
32 0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 0 ∈ ℝ )
33 29 31 32 fdmfifsupp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( 𝐹 ↾ 𝑥 ) finSupp 0 )
34 1 22 29 33 gsumge0cl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ∈ ( 0 [,] +∞ ) )
35 21 34 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ∈ ℝ* )
36 35 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ∈ ℝ* )
37 36 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ∈ ℝ* )
38 eqid ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) )
39 38 rnmptss ⊢ ( ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ∈ ℝ* → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) ⊆ ℝ* )
40 37 39 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) ⊆ ℝ* )
41 snelpwi ⊢ ( 𝑦 ∈ 𝑋 → { 𝑦 } ∈ 𝒫 𝑋 )
42 snfi ⊢ { 𝑦 } ∈ Fin
43 42 a1i ⊢ ( 𝑦 ∈ 𝑋 → { 𝑦 } ∈ Fin )
44 41 43 elind ⊢ ( 𝑦 ∈ 𝑋 → { 𝑦 } ∈ ( 𝒫 𝑋 ∩ Fin ) )
45 44 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → { 𝑦 } ∈ ( 𝒫 𝑋 ∩ Fin ) )
46 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
47 snssi ⊢ ( 𝑦 ∈ 𝑋 → { 𝑦 } ⊆ 𝑋 )
48 47 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → { 𝑦 } ⊆ 𝑋 )
49 46 48 fssresd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ↾ { 𝑦 } ) : { 𝑦 } ⟶ ( 0 [,] +∞ ) )
50 49 feqmptd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ↾ { 𝑦 } ) = ( 𝑥 ∈ { 𝑦 } ↦ ( ( 𝐹 ↾ { 𝑦 } ) ‘ 𝑥 ) ) )
51 fvres ⊢ ( 𝑥 ∈ { 𝑦 } → ( ( 𝐹 ↾ { 𝑦 } ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
52 51 mpteq2ia ⊢ ( 𝑥 ∈ { 𝑦 } ↦ ( ( 𝐹 ↾ { 𝑦 } ) ‘ 𝑥 ) ) = ( 𝑥 ∈ { 𝑦 } ↦ ( 𝐹 ‘ 𝑥 ) )
53 52 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ∈ { 𝑦 } ↦ ( ( 𝐹 ↾ { 𝑦 } ) ‘ 𝑥 ) ) = ( 𝑥 ∈ { 𝑦 } ↦ ( 𝐹 ‘ 𝑥 ) ) )
54 50 53 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ↾ { 𝑦 } ) = ( 𝑥 ∈ { 𝑦 } ↦ ( 𝐹 ‘ 𝑥 ) ) )
55 54 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐺 Σg ( 𝐹 ↾ { 𝑦 } ) ) = ( 𝐺 Σg ( 𝑥 ∈ { 𝑦 } ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
56 55 3adant3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → ( 𝐺 Σg ( 𝐹 ↾ { 𝑦 } ) ) = ( 𝐺 Σg ( 𝑥 ∈ { 𝑦 } ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
57 xrge0cmn ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd
58 1 57 eqeltri ⊢ 𝐺 ∈ CMnd
59 cmnmnd ⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
60 58 59 ax-mp ⊢ 𝐺 ∈ Mnd
61 60 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → 𝐺 ∈ Mnd )
62 simp2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → 𝑦 ∈ 𝑋 )
63 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
64 63 3adant3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
65 dfss2 ⊢ ( ( 0 [,] +∞ ) ⊆ ℝ* ↔ ( ( 0 [,] +∞ ) ∩ ℝ* ) = ( 0 [,] +∞ ) )
66 21 65 mpbi ⊢ ( ( 0 [,] +∞ ) ∩ ℝ* ) = ( 0 [,] +∞ )
67 66 eqcomi ⊢ ( 0 [,] +∞ ) = ( ( 0 [,] +∞ ) ∩ ℝ* )
68 ovex ⊢ ( 0 [,] +∞ ) ∈ V
69 xrsbas ⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
70 1 69 ressbas ⊢ ( ( 0 [,] +∞ ) ∈ V → ( ( 0 [,] +∞ ) ∩ ℝ* ) = ( Base ‘ 𝐺 ) )
71 68 70 ax-mp ⊢ ( ( 0 [,] +∞ ) ∩ ℝ* ) = ( Base ‘ 𝐺 )
72 67 71 eqtri ⊢ ( 0 [,] +∞ ) = ( Base ‘ 𝐺 )
73 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
74 72 73 gsumsn ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) ) → ( 𝐺 Σg ( 𝑥 ∈ { 𝑦 } ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ 𝑦 ) )
75 61 62 64 74 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → ( 𝐺 Σg ( 𝑥 ∈ { 𝑦 } ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ 𝑦 ) )
76 simp3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → ( 𝐹 ‘ 𝑦 ) = +∞ )
77 56 75 76 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → +∞ = ( 𝐺 Σg ( 𝐹 ↾ { 𝑦 } ) ) )
78 reseq2 ⊢ ( 𝑥 = { 𝑦 } → ( 𝐹 ↾ 𝑥 ) = ( 𝐹 ↾ { 𝑦 } ) )
79 78 oveq2d ⊢ ( 𝑥 = { 𝑦 } → ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) = ( 𝐺 Σg ( 𝐹 ↾ { 𝑦 } ) ) )
80 79 rspceeqv ⊢ ( ( { 𝑦 } ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ +∞ = ( 𝐺 Σg ( 𝐹 ↾ { 𝑦 } ) ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) +∞ = ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) )
81 45 77 80 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) +∞ = ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) )
82 pnfxr ⊢ +∞ ∈ ℝ*
83 82 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → +∞ ∈ ℝ* )
84 38 elrnmpt ⊢ ( +∞ ∈ ℝ* → ( +∞ ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) +∞ = ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) )
85 83 84 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → ( +∞ ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) +∞ = ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) )
86 81 85 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → +∞ ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) )
87 supxrpnf ⊢ ( ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) ⊆ ℝ* ∧ +∞ ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) ) → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) = +∞ )
88 40 86 87 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) = +∞ )
89 88 3exp ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑋 → ( ( 𝐹 ‘ 𝑦 ) = +∞ → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) = +∞ ) ) )
90 89 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ( 𝑦 ∈ 𝑋 → ( ( 𝐹 ‘ 𝑦 ) = +∞ → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) = +∞ ) ) )
91 90 rexlimdv ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ( ∃ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) = +∞ → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) = +∞ ) )
92 20 91 mpd ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) = +∞ )
93 15 92 eqtr4d ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) )
94 2 adantr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → 𝑋 ∈ 𝑉 )
95 3 adantr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
96 simpr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → ¬ +∞ ∈ ran 𝐹 )
97 95 96 fge0iccico ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
98 94 97 sge0reval ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) )
99 23 27 feqresmpt ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( 𝐹 ↾ 𝑥 ) = ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) ) )
100 99 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( 𝐹 ↾ 𝑥 ) = ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) ) )
101 100 oveq2d ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) = ( 𝐺 Σg ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) ) ) )
102 1 fveq2i ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
103 eqid ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
104 xrsadd ⊢ +e = ( +g ‘ ℝ*𝑠 )
105 103 104 ressplusg ⊢ ( ( 0 [,] +∞ ) ∈ V → +e = ( +g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) )
106 68 105 ax-mp ⊢ +e = ( +g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
107 106 eqcomi ⊢ ( +g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) = +e
108 102 107 eqtr2i ⊢ +e = ( +g ‘ 𝐺 )
109 1 oveq1i ⊢ ( 𝐺 ↾s ( 0 [,) +∞ ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ↾s ( 0 [,) +∞ ) )
110 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
111 68 110 pm3.2i ⊢ ( ( 0 [,] +∞ ) ∈ V ∧ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) )
112 ressabs ⊢ ( ( ( 0 [,] +∞ ) ∈ V ∧ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ↾s ( 0 [,) +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,) +∞ ) ) )
113 111 112 ax-mp ⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ↾s ( 0 [,) +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,) +∞ ) )
114 109 113 eqtr2i ⊢ ( ℝ*𝑠 ↾s ( 0 [,) +∞ ) ) = ( 𝐺 ↾s ( 0 [,) +∞ ) )
115 58 elexi ⊢ 𝐺 ∈ V
116 115 a1i ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝐺 ∈ V )
117 simpr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) )
118 110 a1i ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) )
119 0xr ⊢ 0 ∈ ℝ*
120 119 a1i ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 0 ∈ ℝ* )
121 82 a1i ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → +∞ ∈ ℝ* )
122 95 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
123 26 sselda ⊢ ( ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑋 )
124 123 adantll ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑋 )
125 122 124 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
126 21 125 sselid ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ* )
127 iccgelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) ) → 0 ≤ ( 𝐹 ‘ 𝑦 ) )
128 120 121 125 127 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 0 ≤ ( 𝐹 ‘ 𝑦 ) )
129 id ⊢ ( ( 𝐹 ‘ 𝑦 ) = +∞ → ( 𝐹 ‘ 𝑦 ) = +∞ )
130 129 eqcomd ⊢ ( ( 𝐹 ‘ 𝑦 ) = +∞ → +∞ = ( 𝐹 ‘ 𝑦 ) )
131 130 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → +∞ = ( 𝐹 ‘ 𝑦 ) )
132 3 ffund ⊢ ( 𝜑 → Fun 𝐹 )
133 132 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → Fun 𝐹 )
134 22 123 sylan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑋 )
135 3 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝑋 )
136 135 eqcomd ⊢ ( 𝜑 → 𝑋 = dom 𝐹 )
137 136 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑋 = dom 𝐹 )
138 134 137 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ dom 𝐹 )
139 fvelrn ⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑦 ) ∈ ran 𝐹 )
140 133 138 139 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ran 𝐹 )
141 140 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → ( 𝐹 ‘ 𝑦 ) ∈ ran 𝐹 )
142 131 141 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → +∞ ∈ ran 𝐹 )
143 142 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → +∞ ∈ ran 𝐹 )
144 96 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → ¬ +∞ ∈ ran 𝐹 )
145 143 144 pm2.65da ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ¬ ( 𝐹 ‘ 𝑦 ) = +∞ )
146 145 neqned ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ≠ +∞ )
147 ge0xrre ⊢ ( ( ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) ∧ ( 𝐹 ‘ 𝑦 ) ≠ +∞ ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
148 125 146 147 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
149 148 ltpnfd ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) < +∞ )
150 120 121 126 128 149 elicod ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,) +∞ ) )
151 eqid ⊢ ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) ) = ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) )
152 150 151 fmptd ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) ) : 𝑥 ⟶ ( 0 [,) +∞ ) )
153 0e0icopnf ⊢ 0 ∈ ( 0 [,) +∞ )
154 153 a1i ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 0 ∈ ( 0 [,) +∞ ) )
155 eliccxr ⊢ ( 𝑦 ∈ ( 0 [,] +∞ ) → 𝑦 ∈ ℝ* )
156 xaddlid ⊢ ( 𝑦 ∈ ℝ* → ( 0 +e 𝑦 ) = 𝑦 )
157 xaddrid ⊢ ( 𝑦 ∈ ℝ* → ( 𝑦 +e 0 ) = 𝑦 )
158 156 157 jca ⊢ ( 𝑦 ∈ ℝ* → ( ( 0 +e 𝑦 ) = 𝑦 ∧ ( 𝑦 +e 0 ) = 𝑦 ) )
159 155 158 syl ⊢ ( 𝑦 ∈ ( 0 [,] +∞ ) → ( ( 0 +e 𝑦 ) = 𝑦 ∧ ( 𝑦 +e 0 ) = 𝑦 ) )
160 159 adantl ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( ( 0 +e 𝑦 ) = 𝑦 ∧ ( 𝑦 +e 0 ) = 𝑦 ) )
161 72 108 114 116 117 118 152 154 160 gsumress ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( 𝐺 Σg ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,) +∞ ) ) Σg ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) ) ) )
162 rege0subm ⊢ ( 0 [,) +∞ ) ∈ ( SubMnd ‘ ℂfld )
163 162 a1i ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( 0 [,) +∞ ) ∈ ( SubMnd ‘ ℂfld ) )
164 eqid ⊢ ( ℂfld ↾s ( 0 [,) +∞ ) ) = ( ℂfld ↾s ( 0 [,) +∞ ) )
165 117 163 152 164 gsumsubm ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( ℂfld Σg ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) ) ) = ( ( ℂfld ↾s ( 0 [,) +∞ ) ) Σg ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) ) ) )
166 eqidd ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( ( ℂfld ↾s ( 0 [,) +∞ ) ) Σg ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) ) ) = ( ( ℂfld ↾s ( 0 [,) +∞ ) ) Σg ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) ) ) )
167 vex ⊢ 𝑥 ∈ V
168 167 mptex ⊢ ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ V
169 168 a1i ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ V )
170 ovexd ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( ℂfld ↾s ( 0 [,) +∞ ) ) ∈ V )
171 ovexd ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( ℝ*𝑠 ↾s ( 0 [,) +∞ ) ) ∈ V )
172 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
173 ax-resscn ⊢ ℝ ⊆ ℂ
174 172 173 sstri ⊢ ( 0 [,) +∞ ) ⊆ ℂ
175 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
176 164 175 ressbas2 ⊢ ( ( 0 [,) +∞ ) ⊆ ℂ → ( 0 [,) +∞ ) = ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
177 174 176 ax-mp ⊢ ( 0 [,) +∞ ) = ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) )
178 177 eqcomi ⊢ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) = ( 0 [,) +∞ )
179 110 21 sstri ⊢ ( 0 [,) +∞ ) ⊆ ℝ*
180 eqid ⊢ ( ℝ*𝑠 ↾s ( 0 [,) +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,) +∞ ) )
181 180 69 ressbas2 ⊢ ( ( 0 [,) +∞ ) ⊆ ℝ* → ( 0 [,) +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,) +∞ ) ) ) )
182 179 181 ax-mp ⊢ ( 0 [,) +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,) +∞ ) ) )
183 178 182 eqtri ⊢ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,) +∞ ) ) )
184 183 a1i ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,) +∞ ) ) ) )
185 rge0srg ⊢ ( ℂfld ↾s ( 0 [,) +∞ ) ) ∈ SRing
186 185 a1i ⊢ ( ( 𝑠 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) ∧ 𝑡 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) ) → ( ℂfld ↾s ( 0 [,) +∞ ) ) ∈ SRing )
187 simpl ⊢ ( ( 𝑠 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) ∧ 𝑡 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) ) → 𝑠 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
188 simpr ⊢ ( ( 𝑠 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) ∧ 𝑡 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) ) → 𝑡 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
189 eqid ⊢ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) = ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) )
190 eqid ⊢ ( +g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) = ( +g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) )
191 189 190 srgacl ⊢ ( ( ( ℂfld ↾s ( 0 [,) +∞ ) ) ∈ SRing ∧ 𝑠 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) ∧ 𝑡 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) ) → ( 𝑠 ( +g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) 𝑡 ) ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
192 186 187 188 191 syl3anc ⊢ ( ( 𝑠 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) ∧ 𝑡 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) ) → ( 𝑠 ( +g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) 𝑡 ) ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
193 192 adantl ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ ( 𝑠 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) ∧ 𝑡 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) ) ) → ( 𝑠 ( +g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) 𝑡 ) ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
194 172 a1i ⊢ ( 𝑠 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) → ( 0 [,) +∞ ) ⊆ ℝ )
195 id ⊢ ( 𝑠 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) → 𝑠 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
196 195 178 eleqtrdi ⊢ ( 𝑠 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) → 𝑠 ∈ ( 0 [,) +∞ ) )
197 194 196 sseldd ⊢ ( 𝑠 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) → 𝑠 ∈ ℝ )
198 197 adantr ⊢ ( ( 𝑠 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) ∧ 𝑡 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) ) → 𝑠 ∈ ℝ )
199 172 a1i ⊢ ( 𝑡 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) → ( 0 [,) +∞ ) ⊆ ℝ )
200 id ⊢ ( 𝑡 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) → 𝑡 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
201 200 178 eleqtrdi ⊢ ( 𝑡 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) → 𝑡 ∈ ( 0 [,) +∞ ) )
202 199 201 sseldd ⊢ ( 𝑡 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) → 𝑡 ∈ ℝ )
203 202 adantl ⊢ ( ( 𝑠 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) ∧ 𝑡 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) ) → 𝑡 ∈ ℝ )
204 rexadd ⊢ ( ( 𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ ) → ( 𝑠 +e 𝑡 ) = ( 𝑠 + 𝑡 ) )
205 204 eqcomd ⊢ ( ( 𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ ) → ( 𝑠 + 𝑡 ) = ( 𝑠 +e 𝑡 ) )
206 162 elexi ⊢ ( 0 [,) +∞ ) ∈ V
207 cnfldadd ⊢ + = ( +g ‘ ℂfld )
208 164 207 ressplusg ⊢ ( ( 0 [,) +∞ ) ∈ V → + = ( +g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
209 206 208 ax-mp ⊢ + = ( +g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) )
210 209 207 eqtr3i ⊢ ( +g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) = ( +g ‘ ℂfld )
211 210 207 eqtr4i ⊢ ( +g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) = +
212 211 oveqi ⊢ ( 𝑠 ( +g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) 𝑡 ) = ( 𝑠 + 𝑡 )
213 212 a1i ⊢ ( ( 𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ ) → ( 𝑠 ( +g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) 𝑡 ) = ( 𝑠 + 𝑡 ) )
214 180 104 ressplusg ⊢ ( ( 0 [,) +∞ ) ∈ V → +e = ( +g ‘ ( ℝ*𝑠 ↾s ( 0 [,) +∞ ) ) ) )
215 206 214 ax-mp ⊢ +e = ( +g ‘ ( ℝ*𝑠 ↾s ( 0 [,) +∞ ) ) )
216 215 eqcomi ⊢ ( +g ‘ ( ℝ*𝑠 ↾s ( 0 [,) +∞ ) ) ) = +e
217 216 oveqi ⊢ ( 𝑠 ( +g ‘ ( ℝ*𝑠 ↾s ( 0 [,) +∞ ) ) ) 𝑡 ) = ( 𝑠 +e 𝑡 )
218 217 a1i ⊢ ( ( 𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ ) → ( 𝑠 ( +g ‘ ( ℝ*𝑠 ↾s ( 0 [,) +∞ ) ) ) 𝑡 ) = ( 𝑠 +e 𝑡 ) )
219 205 213 218 3eqtr4d ⊢ ( ( 𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ ) → ( 𝑠 ( +g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) 𝑡 ) = ( 𝑠 ( +g ‘ ( ℝ*𝑠 ↾s ( 0 [,) +∞ ) ) ) 𝑡 ) )
220 198 203 219 syl2anc ⊢ ( ( 𝑠 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) ∧ 𝑡 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) ) → ( 𝑠 ( +g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) 𝑡 ) = ( 𝑠 ( +g ‘ ( ℝ*𝑠 ↾s ( 0 [,) +∞ ) ) ) 𝑡 ) )
221 220 adantl ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ ( 𝑠 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) ∧ 𝑡 ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) ) ) → ( 𝑠 ( +g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) 𝑡 ) = ( 𝑠 ( +g ‘ ( ℝ*𝑠 ↾s ( 0 [,) +∞ ) ) ) 𝑡 ) )
222 funmpt ⊢ Fun ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) )
223 222 a1i ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → Fun ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) ) )
224 150 177 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
225 224 ralrimiva ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
226 151 rnmptss ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) → ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) ) ⊆ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
227 225 226 syl ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) ) ⊆ ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
228 169 170 171 184 193 221 223 227 gsumpropd2 ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( ( ℂfld ↾s ( 0 [,) +∞ ) ) Σg ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,) +∞ ) ) Σg ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) ) ) )
229 165 166 228 3eqtrd ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( ℂfld Σg ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,) +∞ ) ) Σg ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) ) ) )
230 30 adantl ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑥 ∈ Fin )
231 148 recnd ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
232 230 231 gsumfsum ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( ℂfld Σg ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) ) ) = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
233 229 232 eqtr3d ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,) +∞ ) ) Σg ( 𝑦 ∈ 𝑥 ↦ ( 𝐹 ‘ 𝑦 ) ) ) = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
234 101 161 233 3eqtrrd ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) )
235 234 mpteq2dva ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) )
236 235 rneqd ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) = ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) )
237 236 supeq1d ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) )
238 98 237 eqtrd ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) )
239 93 238 pm2.61dan ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) )
240 1 2 3 4 xrge0tsms ⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = { sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) } )
241 239 240 eleq12d ⊢ ( 𝜑 → ( ( Σ^ ‘ 𝐹 ) ∈ ( 𝐺 tsums 𝐹 ) ↔ sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) ∈ { sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) } ) )
242 11 241 mpbird ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ( 𝐺 tsums 𝐹 ) )