Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sge0tsms Structured version   Visualization version   GIF version

Theorem sge0tsms 44307
Description: Σ^ 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.)
Hypotheses
Ref Expression
sge0tsms.g 𝐺 = (ℝ*𝑠s (0[,]+∞))
sge0tsms.x (𝜑𝑋𝑉)
sge0tsms.f (𝜑𝐹:𝑋⟶(0[,]+∞))
Assertion
Ref Expression
sge0tsms (𝜑 → (Σ^𝐹) ∈ (𝐺 tsums 𝐹))

Proof of Theorem sge0tsms
Dummy variables 𝑠 𝑡 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2737 . . . 4 sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < ) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < )
21a1i 11 . . 3 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < ) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < ))
3 xrltso 12980 . . . . . 6 < Or ℝ*
43supex 9324 . . . . 5 sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < ) ∈ V
54a1i 11 . . . 4 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < ) ∈ V)
6 elsng 4591 . . . 4 (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < ) ∈ V → (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < ) ∈ {sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < )} ↔ sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < ) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < )))
75, 6syl 17 . . 3 (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < ) ∈ {sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < )} ↔ sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < ) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < )))
82, 7mpbird 257 . 2 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < ) ∈ {sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < )})
9 sge0tsms.x . . . . . . 7 (𝜑𝑋𝑉)
109adantr 482 . . . . . 6 ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝑋𝑉)
11 sge0tsms.f . . . . . . 7 (𝜑𝐹:𝑋⟶(0[,]+∞))
1211adantr 482 . . . . . 6 ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝐹:𝑋⟶(0[,]+∞))
13 simpr 486 . . . . . 6 ((𝜑 ∧ +∞ ∈ ran 𝐹) → +∞ ∈ ran 𝐹)
1410, 12, 13sge0pnfval 44300 . . . . 5 ((𝜑 ∧ +∞ ∈ ran 𝐹) → (Σ^𝐹) = +∞)
1511ffnd 6656 . . . . . . . . 9 (𝜑𝐹 Fn 𝑋)
1615adantr 482 . . . . . . . 8 ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝐹 Fn 𝑋)
17 fvelrnb 6890 . . . . . . . 8 (𝐹 Fn 𝑋 → (+∞ ∈ ran 𝐹 ↔ ∃𝑦𝑋 (𝐹𝑦) = +∞))
1816, 17syl 17 . . . . . . 7 ((𝜑 ∧ +∞ ∈ ran 𝐹) → (+∞ ∈ ran 𝐹 ↔ ∃𝑦𝑋 (𝐹𝑦) = +∞))
1913, 18mpbid 231 . . . . . 6 ((𝜑 ∧ +∞ ∈ ran 𝐹) → ∃𝑦𝑋 (𝐹𝑦) = +∞)
20 iccssxr 13267 . . . . . . . . . . . . . 14 (0[,]+∞) ⊆ ℝ*
21 sge0tsms.g . . . . . . . . . . . . . . 15 𝐺 = (ℝ*𝑠s (0[,]+∞))
22 simpr 486 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ (𝒫 𝑋 ∩ Fin))
2311adantr 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝐹:𝑋⟶(0[,]+∞))
24 elinel1 4146 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ 𝒫 𝑋)
25 elpwi 4558 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ 𝒫 𝑋𝑥𝑋)
2624, 25syl 17 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥𝑋)
2726adantl 483 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥𝑋)
28 fssres 6695 . . . . . . . . . . . . . . . 16 ((𝐹:𝑋⟶(0[,]+∞) ∧ 𝑥𝑋) → (𝐹𝑥):𝑥⟶(0[,]+∞))
2923, 27, 28syl2anc 585 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹𝑥):𝑥⟶(0[,]+∞))
30 elinel2 4147 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ Fin)
3130adantl 483 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ Fin)
32 0red 11083 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 0 ∈ ℝ)
3329, 31, 32fdmfifsupp 9240 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹𝑥) finSupp 0)
3421, 22, 29, 33gsumge0cl 44298 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐺 Σg (𝐹𝑥)) ∈ (0[,]+∞))
3520, 34sselid 3933 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐺 Σg (𝐹𝑥)) ∈ ℝ*)
3635ralrimiva 3140 . . . . . . . . . . . 12 (𝜑 → ∀𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐺 Σg (𝐹𝑥)) ∈ ℝ*)
37363ad2ant1 1133 . . . . . . . . . . 11 ((𝜑𝑦𝑋 ∧ (𝐹𝑦) = +∞) → ∀𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐺 Σg (𝐹𝑥)) ∈ ℝ*)
38 eqid 2737 . . . . . . . . . . . 12 (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))) = (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥)))
3938rnmptss 7056 . . . . . . . . . . 11 (∀𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐺 Σg (𝐹𝑥)) ∈ ℝ* → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))) ⊆ ℝ*)
4037, 39syl 17 . . . . . . . . . 10 ((𝜑𝑦𝑋 ∧ (𝐹𝑦) = +∞) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))) ⊆ ℝ*)
41 snelpwi 5392 . . . . . . . . . . . . . 14 (𝑦𝑋 → {𝑦} ∈ 𝒫 𝑋)
42 snfi 8913 . . . . . . . . . . . . . . 15 {𝑦} ∈ Fin
4342a1i 11 . . . . . . . . . . . . . 14 (𝑦𝑋 → {𝑦} ∈ Fin)
4441, 43elind 4145 . . . . . . . . . . . . 13 (𝑦𝑋 → {𝑦} ∈ (𝒫 𝑋 ∩ Fin))
45443ad2ant2 1134 . . . . . . . . . . . 12 ((𝜑𝑦𝑋 ∧ (𝐹𝑦) = +∞) → {𝑦} ∈ (𝒫 𝑋 ∩ Fin))
4611adantr 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑋) → 𝐹:𝑋⟶(0[,]+∞))
47 snssi 4759 . . . . . . . . . . . . . . . . . . 19 (𝑦𝑋 → {𝑦} ⊆ 𝑋)
4847adantl 483 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑋) → {𝑦} ⊆ 𝑋)
4946, 48fssresd 6696 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑋) → (𝐹 ↾ {𝑦}):{𝑦}⟶(0[,]+∞))
5049feqmptd 6897 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑋) → (𝐹 ↾ {𝑦}) = (𝑥 ∈ {𝑦} ↦ ((𝐹 ↾ {𝑦})‘𝑥)))
51 fvres 6848 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ {𝑦} → ((𝐹 ↾ {𝑦})‘𝑥) = (𝐹𝑥))
5251mpteq2ia 5199 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑦} ↦ ((𝐹 ↾ {𝑦})‘𝑥)) = (𝑥 ∈ {𝑦} ↦ (𝐹𝑥))
5352a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑋) → (𝑥 ∈ {𝑦} ↦ ((𝐹 ↾ {𝑦})‘𝑥)) = (𝑥 ∈ {𝑦} ↦ (𝐹𝑥)))
5450, 53eqtrd 2777 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑋) → (𝐹 ↾ {𝑦}) = (𝑥 ∈ {𝑦} ↦ (𝐹𝑥)))
5554oveq2d 7357 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑋) → (𝐺 Σg (𝐹 ↾ {𝑦})) = (𝐺 Σg (𝑥 ∈ {𝑦} ↦ (𝐹𝑥))))
56553adant3 1132 . . . . . . . . . . . . 13 ((𝜑𝑦𝑋 ∧ (𝐹𝑦) = +∞) → (𝐺 Σg (𝐹 ↾ {𝑦})) = (𝐺 Σg (𝑥 ∈ {𝑦} ↦ (𝐹𝑥))))
57 xrge0cmn 20745 . . . . . . . . . . . . . . . . 17 (ℝ*𝑠s (0[,]+∞)) ∈ CMnd
5821, 57eqeltri 2834 . . . . . . . . . . . . . . . 16 𝐺 ∈ CMnd
59 cmnmnd 19497 . . . . . . . . . . . . . . . 16 (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
6058, 59ax-mp 5 . . . . . . . . . . . . . . 15 𝐺 ∈ Mnd
6160a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑋 ∧ (𝐹𝑦) = +∞) → 𝐺 ∈ Mnd)
62 simp2 1137 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑋 ∧ (𝐹𝑦) = +∞) → 𝑦𝑋)
6311ffvelcdmda 7021 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑋) → (𝐹𝑦) ∈ (0[,]+∞))
64633adant3 1132 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑋 ∧ (𝐹𝑦) = +∞) → (𝐹𝑦) ∈ (0[,]+∞))
65 df-ss 3918 . . . . . . . . . . . . . . . . . 18 ((0[,]+∞) ⊆ ℝ* ↔ ((0[,]+∞) ∩ ℝ*) = (0[,]+∞))
6620, 65mpbi 229 . . . . . . . . . . . . . . . . 17 ((0[,]+∞) ∩ ℝ*) = (0[,]+∞)
6766eqcomi 2746 . . . . . . . . . . . . . . . 16 (0[,]+∞) = ((0[,]+∞) ∩ ℝ*)
68 ovex 7374 . . . . . . . . . . . . . . . . 17 (0[,]+∞) ∈ V
69 xrsbas 20719 . . . . . . . . . . . . . . . . . 18 * = (Base‘ℝ*𝑠)
7021, 69ressbas 17044 . . . . . . . . . . . . . . . . 17 ((0[,]+∞) ∈ V → ((0[,]+∞) ∩ ℝ*) = (Base‘𝐺))
7168, 70ax-mp 5 . . . . . . . . . . . . . . . 16 ((0[,]+∞) ∩ ℝ*) = (Base‘𝐺)
7267, 71eqtri 2765 . . . . . . . . . . . . . . 15 (0[,]+∞) = (Base‘𝐺)
73 fveq2 6829 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
7472, 73gsumsn 19649 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ 𝑦𝑋 ∧ (𝐹𝑦) ∈ (0[,]+∞)) → (𝐺 Σg (𝑥 ∈ {𝑦} ↦ (𝐹𝑥))) = (𝐹𝑦))
7561, 62, 64, 74syl3anc 1371 . . . . . . . . . . . . 13 ((𝜑𝑦𝑋 ∧ (𝐹𝑦) = +∞) → (𝐺 Σg (𝑥 ∈ {𝑦} ↦ (𝐹𝑥))) = (𝐹𝑦))
76 simp3 1138 . . . . . . . . . . . . 13 ((𝜑𝑦𝑋 ∧ (𝐹𝑦) = +∞) → (𝐹𝑦) = +∞)
7756, 75, 763eqtrrd 2782 . . . . . . . . . . . 12 ((𝜑𝑦𝑋 ∧ (𝐹𝑦) = +∞) → +∞ = (𝐺 Σg (𝐹 ↾ {𝑦})))
78 reseq2 5922 . . . . . . . . . . . . . 14 (𝑥 = {𝑦} → (𝐹𝑥) = (𝐹 ↾ {𝑦}))
7978oveq2d 7357 . . . . . . . . . . . . 13 (𝑥 = {𝑦} → (𝐺 Σg (𝐹𝑥)) = (𝐺 Σg (𝐹 ↾ {𝑦})))
8079rspceeqv 3587 . . . . . . . . . . . 12 (({𝑦} ∈ (𝒫 𝑋 ∩ Fin) ∧ +∞ = (𝐺 Σg (𝐹 ↾ {𝑦}))) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ = (𝐺 Σg (𝐹𝑥)))
8145, 77, 80syl2anc 585 . . . . . . . . . . 11 ((𝜑𝑦𝑋 ∧ (𝐹𝑦) = +∞) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ = (𝐺 Σg (𝐹𝑥)))
82 pnfxr 11134 . . . . . . . . . . . . 13 +∞ ∈ ℝ*
8382a1i 11 . . . . . . . . . . . 12 ((𝜑𝑦𝑋 ∧ (𝐹𝑦) = +∞) → +∞ ∈ ℝ*)
8438elrnmpt 5901 . . . . . . . . . . . 12 (+∞ ∈ ℝ* → (+∞ ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ = (𝐺 Σg (𝐹𝑥))))
8583, 84syl 17 . . . . . . . . . . 11 ((𝜑𝑦𝑋 ∧ (𝐹𝑦) = +∞) → (+∞ ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ = (𝐺 Σg (𝐹𝑥))))
8681, 85mpbird 257 . . . . . . . . . 10 ((𝜑𝑦𝑋 ∧ (𝐹𝑦) = +∞) → +∞ ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))))
87 supxrpnf 13157 . . . . . . . . . 10 ((ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))) ⊆ ℝ* ∧ +∞ ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥)))) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < ) = +∞)
8840, 86, 87syl2anc 585 . . . . . . . . 9 ((𝜑𝑦𝑋 ∧ (𝐹𝑦) = +∞) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < ) = +∞)
89883exp 1119 . . . . . . . 8 (𝜑 → (𝑦𝑋 → ((𝐹𝑦) = +∞ → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < ) = +∞)))
9089adantr 482 . . . . . . 7 ((𝜑 ∧ +∞ ∈ ran 𝐹) → (𝑦𝑋 → ((𝐹𝑦) = +∞ → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < ) = +∞)))
9190rexlimdv 3147 . . . . . 6 ((𝜑 ∧ +∞ ∈ ran 𝐹) → (∃𝑦𝑋 (𝐹𝑦) = +∞ → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < ) = +∞))
9219, 91mpd 15 . . . . 5 ((𝜑 ∧ +∞ ∈ ran 𝐹) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < ) = +∞)
9314, 92eqtr4d 2780 . . . 4 ((𝜑 ∧ +∞ ∈ ran 𝐹) → (Σ^𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < ))
949adantr 482 . . . . . 6 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → 𝑋𝑉)
9511adantr 482 . . . . . . 7 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → 𝐹:𝑋⟶(0[,]+∞))
96 simpr 486 . . . . . . 7 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → ¬ +∞ ∈ ran 𝐹)
9795, 96fge0iccico 44297 . . . . . 6 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → 𝐹:𝑋⟶(0[,)+∞))
9894, 97sge0reval 44299 . . . . 5 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → (Σ^𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ*, < ))
9923, 27feqresmpt 6898 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹𝑥) = (𝑦𝑥 ↦ (𝐹𝑦)))
10099adantlr 713 . . . . . . . . . 10 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹𝑥) = (𝑦𝑥 ↦ (𝐹𝑦)))
101100oveq2d 7357 . . . . . . . . 9 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐺 Σg (𝐹𝑥)) = (𝐺 Σg (𝑦𝑥 ↦ (𝐹𝑦))))
10221fveq2i 6832 . . . . . . . . . . 11 (+g𝐺) = (+g‘(ℝ*𝑠s (0[,]+∞)))
103 eqid 2737 . . . . . . . . . . . . . 14 (ℝ*𝑠s (0[,]+∞)) = (ℝ*𝑠s (0[,]+∞))
104 xrsadd 20720 . . . . . . . . . . . . . 14 +𝑒 = (+g‘ℝ*𝑠)
105103, 104ressplusg 17097 . . . . . . . . . . . . 13 ((0[,]+∞) ∈ V → +𝑒 = (+g‘(ℝ*𝑠s (0[,]+∞))))
10668, 105ax-mp 5 . . . . . . . . . . . 12 +𝑒 = (+g‘(ℝ*𝑠s (0[,]+∞)))
107106eqcomi 2746 . . . . . . . . . . 11 (+g‘(ℝ*𝑠s (0[,]+∞))) = +𝑒
108102, 107eqtr2i 2766 . . . . . . . . . 10 +𝑒 = (+g𝐺)
10921oveq1i 7351 . . . . . . . . . . 11 (𝐺s (0[,)+∞)) = ((ℝ*𝑠s (0[,]+∞)) ↾s (0[,)+∞))
110 icossicc 13273 . . . . . . . . . . . . 13 (0[,)+∞) ⊆ (0[,]+∞)
11168, 110pm3.2i 472 . . . . . . . . . . . 12 ((0[,]+∞) ∈ V ∧ (0[,)+∞) ⊆ (0[,]+∞))
112 ressabs 17056 . . . . . . . . . . . 12 (((0[,]+∞) ∈ V ∧ (0[,)+∞) ⊆ (0[,]+∞)) → ((ℝ*𝑠s (0[,]+∞)) ↾s (0[,)+∞)) = (ℝ*𝑠s (0[,)+∞)))
113111, 112ax-mp 5 . . . . . . . . . . 11 ((ℝ*𝑠s (0[,]+∞)) ↾s (0[,)+∞)) = (ℝ*𝑠s (0[,)+∞))
114109, 113eqtr2i 2766 . . . . . . . . . 10 (ℝ*𝑠s (0[,)+∞)) = (𝐺s (0[,)+∞))
11558elexi 3461 . . . . . . . . . . 11 𝐺 ∈ V
116115a1i 11 . . . . . . . . . 10 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝐺 ∈ V)
117 simpr 486 . . . . . . . . . 10 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ (𝒫 𝑋 ∩ Fin))
118110a1i 11 . . . . . . . . . 10 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (0[,)+∞) ⊆ (0[,]+∞))
119 0xr 11127 . . . . . . . . . . . . 13 0 ∈ ℝ*
120119a1i 11 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → 0 ∈ ℝ*)
12182a1i 11 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → +∞ ∈ ℝ*)
12295ad2antrr 724 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → 𝐹:𝑋⟶(0[,]+∞))
12326sselda 3935 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦𝑥) → 𝑦𝑋)
124123adantll 712 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → 𝑦𝑋)
125122, 124ffvelcdmd 7022 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ (0[,]+∞))
12620, 125sselid 3933 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ ℝ*)
127 iccgelb 13240 . . . . . . . . . . . . 13 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ (𝐹𝑦) ∈ (0[,]+∞)) → 0 ≤ (𝐹𝑦))
128120, 121, 125, 127syl3anc 1371 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → 0 ≤ (𝐹𝑦))
129 id 22 . . . . . . . . . . . . . . . . . . . 20 ((𝐹𝑦) = +∞ → (𝐹𝑦) = +∞)
130129eqcomd 2743 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑦) = +∞ → +∞ = (𝐹𝑦))
131130adantl 483 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) ∧ (𝐹𝑦) = +∞) → +∞ = (𝐹𝑦))
13211ffund 6659 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → Fun 𝐹)
133132ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → Fun 𝐹)
13422, 123sylan 581 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → 𝑦𝑋)
13511fdmd 6666 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → dom 𝐹 = 𝑋)
136135eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑋 = dom 𝐹)
137136ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → 𝑋 = dom 𝐹)
138134, 137eleqtrd 2840 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → 𝑦 ∈ dom 𝐹)
139 fvelrn 7014 . . . . . . . . . . . . . . . . . . . 20 ((Fun 𝐹𝑦 ∈ dom 𝐹) → (𝐹𝑦) ∈ ran 𝐹)
140133, 138, 139syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ ran 𝐹)
141140adantr 482 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) ∧ (𝐹𝑦) = +∞) → (𝐹𝑦) ∈ ran 𝐹)
142131, 141eqeltrd 2838 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) ∧ (𝐹𝑦) = +∞) → +∞ ∈ ran 𝐹)
143142adantl3r 748 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) ∧ (𝐹𝑦) = +∞) → +∞ ∈ ran 𝐹)
14496ad3antrrr 728 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) ∧ (𝐹𝑦) = +∞) → ¬ +∞ ∈ ran 𝐹)
145143, 144pm2.65da 815 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → ¬ (𝐹𝑦) = +∞)
146145neqned 2948 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ≠ +∞)
147 ge0xrre 43457 . . . . . . . . . . . . . 14 (((𝐹𝑦) ∈ (0[,]+∞) ∧ (𝐹𝑦) ≠ +∞) → (𝐹𝑦) ∈ ℝ)
148125, 146, 147syl2anc 585 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ ℝ)
149148ltpnfd 12962 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) < +∞)
150120, 121, 126, 128, 149elicod 13234 . . . . . . . . . . 11 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ (0[,)+∞))
151 eqid 2737 . . . . . . . . . . 11 (𝑦𝑥 ↦ (𝐹𝑦)) = (𝑦𝑥 ↦ (𝐹𝑦))
152150, 151fmptd 7048 . . . . . . . . . 10 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝑦𝑥 ↦ (𝐹𝑦)):𝑥⟶(0[,)+∞))
153 0e0icopnf 13295 . . . . . . . . . . 11 0 ∈ (0[,)+∞)
154153a1i 11 . . . . . . . . . 10 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 0 ∈ (0[,)+∞))
155 eliccxr 13272 . . . . . . . . . . . 12 (𝑦 ∈ (0[,]+∞) → 𝑦 ∈ ℝ*)
156 xaddid2 13081 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ* → (0 +𝑒 𝑦) = 𝑦)
157 xaddid1 13080 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ* → (𝑦 +𝑒 0) = 𝑦)
158156, 157jca 513 . . . . . . . . . . . 12 (𝑦 ∈ ℝ* → ((0 +𝑒 𝑦) = 𝑦 ∧ (𝑦 +𝑒 0) = 𝑦))
159155, 158syl 17 . . . . . . . . . . 11 (𝑦 ∈ (0[,]+∞) → ((0 +𝑒 𝑦) = 𝑦 ∧ (𝑦 +𝑒 0) = 𝑦))
160159adantl 483 . . . . . . . . . 10 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ (0[,]+∞)) → ((0 +𝑒 𝑦) = 𝑦 ∧ (𝑦 +𝑒 0) = 𝑦))
16172, 108, 114, 116, 117, 118, 152, 154, 160gsumress 18463 . . . . . . . . 9 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐺 Σg (𝑦𝑥 ↦ (𝐹𝑦))) = ((ℝ*𝑠s (0[,)+∞)) Σg (𝑦𝑥 ↦ (𝐹𝑦))))
162 rege0subm 20759 . . . . . . . . . . . . 13 (0[,)+∞) ∈ (SubMnd‘ℂfld)
163162a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (0[,)+∞) ∈ (SubMnd‘ℂfld))
164 eqid 2737 . . . . . . . . . . . 12 (ℂflds (0[,)+∞)) = (ℂflds (0[,)+∞))
165117, 163, 152, 164gsumsubm 18570 . . . . . . . . . . 11 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (ℂfld Σg (𝑦𝑥 ↦ (𝐹𝑦))) = ((ℂflds (0[,)+∞)) Σg (𝑦𝑥 ↦ (𝐹𝑦))))
166 eqidd 2738 . . . . . . . . . . 11 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ((ℂflds (0[,)+∞)) Σg (𝑦𝑥 ↦ (𝐹𝑦))) = ((ℂflds (0[,)+∞)) Σg (𝑦𝑥 ↦ (𝐹𝑦))))
167 vex 3446 . . . . . . . . . . . . . 14 𝑥 ∈ V
168167mptex 7159 . . . . . . . . . . . . 13 (𝑦𝑥 ↦ (𝐹𝑦)) ∈ V
169168a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝑦𝑥 ↦ (𝐹𝑦)) ∈ V)
170 ovexd 7376 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (ℂflds (0[,)+∞)) ∈ V)
171 ovexd 7376 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (ℝ*𝑠s (0[,)+∞)) ∈ V)
172 rge0ssre 13293 . . . . . . . . . . . . . . . . 17 (0[,)+∞) ⊆ ℝ
173 ax-resscn 11033 . . . . . . . . . . . . . . . . 17 ℝ ⊆ ℂ
174172, 173sstri 3944 . . . . . . . . . . . . . . . 16 (0[,)+∞) ⊆ ℂ
175 cnfldbas 20706 . . . . . . . . . . . . . . . . 17 ℂ = (Base‘ℂfld)
176164, 175ressbas2 17046 . . . . . . . . . . . . . . . 16 ((0[,)+∞) ⊆ ℂ → (0[,)+∞) = (Base‘(ℂflds (0[,)+∞))))
177174, 176ax-mp 5 . . . . . . . . . . . . . . 15 (0[,)+∞) = (Base‘(ℂflds (0[,)+∞)))
178177eqcomi 2746 . . . . . . . . . . . . . 14 (Base‘(ℂflds (0[,)+∞))) = (0[,)+∞)
179110, 20sstri 3944 . . . . . . . . . . . . . . 15 (0[,)+∞) ⊆ ℝ*
180 eqid 2737 . . . . . . . . . . . . . . . 16 (ℝ*𝑠s (0[,)+∞)) = (ℝ*𝑠s (0[,)+∞))
181180, 69ressbas2 17046 . . . . . . . . . . . . . . 15 ((0[,)+∞) ⊆ ℝ* → (0[,)+∞) = (Base‘(ℝ*𝑠s (0[,)+∞))))
182179, 181ax-mp 5 . . . . . . . . . . . . . 14 (0[,)+∞) = (Base‘(ℝ*𝑠s (0[,)+∞)))
183178, 182eqtri 2765 . . . . . . . . . . . . 13 (Base‘(ℂflds (0[,)+∞))) = (Base‘(ℝ*𝑠s (0[,)+∞)))
184183a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (Base‘(ℂflds (0[,)+∞))) = (Base‘(ℝ*𝑠s (0[,)+∞))))
185 rge0srg 20774 . . . . . . . . . . . . . . 15 (ℂflds (0[,)+∞)) ∈ SRing
186185a1i 11 . . . . . . . . . . . . . 14 ((𝑠 ∈ (Base‘(ℂflds (0[,)+∞))) ∧ 𝑡 ∈ (Base‘(ℂflds (0[,)+∞)))) → (ℂflds (0[,)+∞)) ∈ SRing)
187 simpl 484 . . . . . . . . . . . . . 14 ((𝑠 ∈ (Base‘(ℂflds (0[,)+∞))) ∧ 𝑡 ∈ (Base‘(ℂflds (0[,)+∞)))) → 𝑠 ∈ (Base‘(ℂflds (0[,)+∞))))
188 simpr 486 . . . . . . . . . . . . . 14 ((𝑠 ∈ (Base‘(ℂflds (0[,)+∞))) ∧ 𝑡 ∈ (Base‘(ℂflds (0[,)+∞)))) → 𝑡 ∈ (Base‘(ℂflds (0[,)+∞))))
189 eqid 2737 . . . . . . . . . . . . . . 15 (Base‘(ℂflds (0[,)+∞))) = (Base‘(ℂflds (0[,)+∞)))
190 eqid 2737 . . . . . . . . . . . . . . 15 (+g‘(ℂflds (0[,)+∞))) = (+g‘(ℂflds (0[,)+∞)))
191189, 190srgacl 19854 . . . . . . . . . . . . . 14 (((ℂflds (0[,)+∞)) ∈ SRing ∧ 𝑠 ∈ (Base‘(ℂflds (0[,)+∞))) ∧ 𝑡 ∈ (Base‘(ℂflds (0[,)+∞)))) → (𝑠(+g‘(ℂflds (0[,)+∞)))𝑡) ∈ (Base‘(ℂflds (0[,)+∞))))
192186, 187, 188, 191syl3anc 1371 . . . . . . . . . . . . 13 ((𝑠 ∈ (Base‘(ℂflds (0[,)+∞))) ∧ 𝑡 ∈ (Base‘(ℂflds (0[,)+∞)))) → (𝑠(+g‘(ℂflds (0[,)+∞)))𝑡) ∈ (Base‘(ℂflds (0[,)+∞))))
193192adantl 483 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ (𝑠 ∈ (Base‘(ℂflds (0[,)+∞))) ∧ 𝑡 ∈ (Base‘(ℂflds (0[,)+∞))))) → (𝑠(+g‘(ℂflds (0[,)+∞)))𝑡) ∈ (Base‘(ℂflds (0[,)+∞))))
194172a1i 11 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (Base‘(ℂflds (0[,)+∞))) → (0[,)+∞) ⊆ ℝ)
195 id 22 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (Base‘(ℂflds (0[,)+∞))) → 𝑠 ∈ (Base‘(ℂflds (0[,)+∞))))
196195, 178eleqtrdi 2848 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (Base‘(ℂflds (0[,)+∞))) → 𝑠 ∈ (0[,)+∞))
197194, 196sseldd 3936 . . . . . . . . . . . . . . 15 (𝑠 ∈ (Base‘(ℂflds (0[,)+∞))) → 𝑠 ∈ ℝ)
198197adantr 482 . . . . . . . . . . . . . 14 ((𝑠 ∈ (Base‘(ℂflds (0[,)+∞))) ∧ 𝑡 ∈ (Base‘(ℂflds (0[,)+∞)))) → 𝑠 ∈ ℝ)
199172a1i 11 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (Base‘(ℂflds (0[,)+∞))) → (0[,)+∞) ⊆ ℝ)
200 id 22 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ (Base‘(ℂflds (0[,)+∞))) → 𝑡 ∈ (Base‘(ℂflds (0[,)+∞))))
201200, 178eleqtrdi 2848 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (Base‘(ℂflds (0[,)+∞))) → 𝑡 ∈ (0[,)+∞))
202199, 201sseldd 3936 . . . . . . . . . . . . . . 15 (𝑡 ∈ (Base‘(ℂflds (0[,)+∞))) → 𝑡 ∈ ℝ)
203202adantl 483 . . . . . . . . . . . . . 14 ((𝑠 ∈ (Base‘(ℂflds (0[,)+∞))) ∧ 𝑡 ∈ (Base‘(ℂflds (0[,)+∞)))) → 𝑡 ∈ ℝ)
204 rexadd 13071 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠 +𝑒 𝑡) = (𝑠 + 𝑡))
205204eqcomd 2743 . . . . . . . . . . . . . . 15 ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠 + 𝑡) = (𝑠 +𝑒 𝑡))
206162elexi 3461 . . . . . . . . . . . . . . . . . . . 20 (0[,)+∞) ∈ V
207 cnfldadd 20707 . . . . . . . . . . . . . . . . . . . . 21 + = (+g‘ℂfld)
208164, 207ressplusg 17097 . . . . . . . . . . . . . . . . . . . 20 ((0[,)+∞) ∈ V → + = (+g‘(ℂflds (0[,)+∞))))
209206, 208ax-mp 5 . . . . . . . . . . . . . . . . . . 19 + = (+g‘(ℂflds (0[,)+∞)))
210209, 207eqtr3i 2767 . . . . . . . . . . . . . . . . . 18 (+g‘(ℂflds (0[,)+∞))) = (+g‘ℂfld)
211210, 207eqtr4i 2768 . . . . . . . . . . . . . . . . 17 (+g‘(ℂflds (0[,)+∞))) = +
212211oveqi 7354 . . . . . . . . . . . . . . . 16 (𝑠(+g‘(ℂflds (0[,)+∞)))𝑡) = (𝑠 + 𝑡)
213212a1i 11 . . . . . . . . . . . . . . 15 ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠(+g‘(ℂflds (0[,)+∞)))𝑡) = (𝑠 + 𝑡))
214180, 104ressplusg 17097 . . . . . . . . . . . . . . . . . . 19 ((0[,)+∞) ∈ V → +𝑒 = (+g‘(ℝ*𝑠s (0[,)+∞))))
215206, 214ax-mp 5 . . . . . . . . . . . . . . . . . 18 +𝑒 = (+g‘(ℝ*𝑠s (0[,)+∞)))
216215eqcomi 2746 . . . . . . . . . . . . . . . . 17 (+g‘(ℝ*𝑠s (0[,)+∞))) = +𝑒
217216oveqi 7354 . . . . . . . . . . . . . . . 16 (𝑠(+g‘(ℝ*𝑠s (0[,)+∞)))𝑡) = (𝑠 +𝑒 𝑡)
218217a1i 11 . . . . . . . . . . . . . . 15 ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠(+g‘(ℝ*𝑠s (0[,)+∞)))𝑡) = (𝑠 +𝑒 𝑡))
219205, 213, 2183eqtr4d 2787 . . . . . . . . . . . . . 14 ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠(+g‘(ℂflds (0[,)+∞)))𝑡) = (𝑠(+g‘(ℝ*𝑠s (0[,)+∞)))𝑡))
220198, 203, 219syl2anc 585 . . . . . . . . . . . . 13 ((𝑠 ∈ (Base‘(ℂflds (0[,)+∞))) ∧ 𝑡 ∈ (Base‘(ℂflds (0[,)+∞)))) → (𝑠(+g‘(ℂflds (0[,)+∞)))𝑡) = (𝑠(+g‘(ℝ*𝑠s (0[,)+∞)))𝑡))
221220adantl 483 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ (𝑠 ∈ (Base‘(ℂflds (0[,)+∞))) ∧ 𝑡 ∈ (Base‘(ℂflds (0[,)+∞))))) → (𝑠(+g‘(ℂflds (0[,)+∞)))𝑡) = (𝑠(+g‘(ℝ*𝑠s (0[,)+∞)))𝑡))
222 funmpt 6526 . . . . . . . . . . . . 13 Fun (𝑦𝑥 ↦ (𝐹𝑦))
223222a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Fun (𝑦𝑥 ↦ (𝐹𝑦)))
224150, 177eleqtrdi 2848 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ (Base‘(ℂflds (0[,)+∞))))
225224ralrimiva 3140 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ∀𝑦𝑥 (𝐹𝑦) ∈ (Base‘(ℂflds (0[,)+∞))))
226151rnmptss 7056 . . . . . . . . . . . . 13 (∀𝑦𝑥 (𝐹𝑦) ∈ (Base‘(ℂflds (0[,)+∞))) → ran (𝑦𝑥 ↦ (𝐹𝑦)) ⊆ (Base‘(ℂflds (0[,)+∞))))
227225, 226syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ran (𝑦𝑥 ↦ (𝐹𝑦)) ⊆ (Base‘(ℂflds (0[,)+∞))))
228169, 170, 171, 184, 193, 221, 223, 227gsumpropd2 18461 . . . . . . . . . . 11 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ((ℂflds (0[,)+∞)) Σg (𝑦𝑥 ↦ (𝐹𝑦))) = ((ℝ*𝑠s (0[,)+∞)) Σg (𝑦𝑥 ↦ (𝐹𝑦))))
229165, 166, 2283eqtrd 2781 . . . . . . . . . 10 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (ℂfld Σg (𝑦𝑥 ↦ (𝐹𝑦))) = ((ℝ*𝑠s (0[,)+∞)) Σg (𝑦𝑥 ↦ (𝐹𝑦))))
23030adantl 483 . . . . . . . . . . 11 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ Fin)
231148recnd 11108 . . . . . . . . . . 11 ((((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ ℂ)
232230, 231gsumfsum 20770 . . . . . . . . . 10 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (ℂfld Σg (𝑦𝑥 ↦ (𝐹𝑦))) = Σ𝑦𝑥 (𝐹𝑦))
233229, 232eqtr3d 2779 . . . . . . . . 9 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ((ℝ*𝑠s (0[,)+∞)) Σg (𝑦𝑥 ↦ (𝐹𝑦))) = Σ𝑦𝑥 (𝐹𝑦))
234101, 161, 2333eqtrrd 2782 . . . . . . . 8 (((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑦𝑥 (𝐹𝑦) = (𝐺 Σg (𝐹𝑥)))
235234mpteq2dva 5196 . . . . . . 7 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) = (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))))
236235rneqd 5883 . . . . . 6 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) = ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))))
237236supeq1d 9307 . . . . 5 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ*, < ) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < ))
23898, 237eqtrd 2777 . . . 4 ((𝜑 ∧ ¬ +∞ ∈ ran 𝐹) → (Σ^𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < ))
23993, 238pm2.61dan 811 . . 3 (𝜑 → (Σ^𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < ))
24021, 9, 11, 1xrge0tsms 24102 . . 3 (𝜑 → (𝐺 tsums 𝐹) = {sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < )})
241239, 240eleq12d 2832 . 2 (𝜑 → ((Σ^𝐹) ∈ (𝐺 tsums 𝐹) ↔ sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < ) ∈ {sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑥))), ℝ*, < )}))
2428, 241mpbird 257 1 (𝜑 → (Σ^𝐹) ∈ (𝐺 tsums 𝐹))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  w3a 1087   = wceq 1541  wcel 2106  wne 2941  wral 3062  wrex 3071  Vcvv 3442  cin 3900  wss 3901  𝒫 cpw 4551  {csn 4577   class class class wbr 5096  cmpt 5179  dom cdm 5624  ran crn 5625  cres 5626  Fun wfun 6477   Fn wfn 6478  wf 6479  cfv 6483  (class class class)co 7341  Fincfn 8808  supcsup 9301  cc 10974  cr 10975  0cc0 10976   + caddc 10979  +∞cpnf 11111  *cxr 11113   < clt 11114  cle 11115   +𝑒 cxad 12951  [,)cico 13186  [,]cicc 13187  Σcsu 15496  Basecbs 17009  s cress 17038  +gcplusg 17059   Σg cgsu 17248  *𝑠cxrs 17308  Mndcmnd 18482  SubMndcsubmnd 18526  CMndccmn 19481  SRingcsrg 19835  fldccnfld 20702   tsums ctsu 23382  Σ^csumge0 44289
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5233  ax-sep 5247  ax-nul 5254  ax-pow 5312  ax-pr 5376  ax-un 7654  ax-inf2 9502  ax-cnex 11032  ax-resscn 11033  ax-1cn 11034  ax-icn 11035  ax-addcl 11036  ax-addrcl 11037  ax-mulcl 11038  ax-mulrcl 11039  ax-mulcom 11040  ax-addass 11041  ax-mulass 11042  ax-distr 11043  ax-i2m1 11044  ax-1ne0 11045  ax-1rid 11046  ax-rnegex 11047  ax-rrecex 11048  ax-cnre 11049  ax-pre-lttri 11050  ax-pre-lttrn 11051  ax-pre-ltadd 11052  ax-pre-mulgt0 11053  ax-pre-sup 11054  ax-addf 11055  ax-mulf 11056
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3444  df-sbc 3731  df-csb 3847  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3920  df-nul 4274  df-if 4478  df-pw 4553  df-sn 4578  df-pr 4580  df-tp 4582  df-op 4584  df-uni 4857  df-int 4899  df-iun 4947  df-iin 4948  df-br 5097  df-opab 5159  df-mpt 5180  df-tr 5214  df-id 5522  df-eprel 5528  df-po 5536  df-so 5537  df-fr 5579  df-se 5580  df-we 5581  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6242  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6435  df-fun 6485  df-fn 6486  df-f 6487  df-f1 6488  df-fo 6489  df-f1o 6490  df-fv 6491  df-isom 6492  df-riota 7297  df-ov 7344  df-oprab 7345  df-mpo 7346  df-of 7599  df-om 7785  df-1st 7903  df-2nd 7904  df-supp 8052  df-frecs 8171  df-wrecs 8202  df-recs 8276  df-rdg 8315  df-1o 8371  df-er 8573  df-map 8692  df-en 8809  df-dom 8810  df-sdom 8811  df-fin 8812  df-fsupp 9231  df-fi 9272  df-sup 9303  df-inf 9304  df-oi 9371  df-card 9800  df-pnf 11116  df-mnf 11117  df-xr 11118  df-ltxr 11119  df-le 11120  df-sub 11312  df-neg 11313  df-div 11738  df-nn 12079  df-2 12141  df-3 12142  df-4 12143  df-5 12144  df-6 12145  df-7 12146  df-8 12147  df-9 12148  df-n0 12339  df-z 12425  df-dec 12543  df-uz 12688  df-q 12794  df-rp 12836  df-xadd 12954  df-ioo 13188  df-ioc 13189  df-ico 13190  df-icc 13191  df-fz 13345  df-fzo 13488  df-seq 13827  df-exp 13888  df-hash 14150  df-cj 14909  df-re 14910  df-im 14911  df-sqrt 15045  df-abs 15046  df-clim 15296  df-sum 15497  df-struct 16945  df-sets 16962  df-slot 16980  df-ndx 16992  df-base 17010  df-ress 17039  df-plusg 17072  df-mulr 17073  df-starv 17074  df-tset 17078  df-ple 17079  df-ds 17081  df-unif 17082  df-rest 17230  df-topn 17231  df-0g 17249  df-gsum 17250  df-topgen 17251  df-ordt 17309  df-xrs 17310  df-mre 17392  df-mrc 17393  df-acs 17395  df-ps 18381  df-tsr 18382  df-mgm 18423  df-sgrp 18472  df-mnd 18483  df-submnd 18528  df-grp 18676  df-minusg 18677  df-mulg 18797  df-cntz 19019  df-cmn 19483  df-abl 19484  df-mgp 19815  df-ur 19832  df-srg 19836  df-ring 19879  df-cring 19880  df-fbas 20699  df-fg 20700  df-cnfld 20703  df-top 22148  df-topon 22165  df-topsp 22187  df-bases 22201  df-ntr 22276  df-nei 22354  df-cn 22483  df-haus 22571  df-fil 23102  df-fm 23194  df-flim 23195  df-flf 23196  df-tsms 23383  df-sumge0 44290
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator