Metamath Proof Explorer

Theorem esumpfinvallem

Description: Lemma for esumpfinval . (Contributed by Thierry Arnoux, 28-Jun-2017)

Ref Expression
Assertion esumpfinvallem ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → ∑ ℂ fld F = ∑ ℝ 𝑠 * ↾ 𝑠 0 +∞ F

Proof

Step Hyp Ref Expression
1 fex ⊢ F : A ⟶ 0 +∞ ∧ A ∈ V → F ∈ V
2 1 ancoms ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → F ∈ V
3 ovexd ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → ℂ fld ↾ 𝑠 0 +∞ ∈ V
4 ovexd ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ V
5 rge0ssre ⊢ 0 +∞ ⊆ ℝ
6 ax-resscn ⊢ ℝ ⊆ ℂ
7 5 6 sstri ⊢ 0 +∞ ⊆ ℂ
8 eqid ⊢ ℂ fld ↾ 𝑠 0 +∞ = ℂ fld ↾ 𝑠 0 +∞
9 cnfldbas ⊢ ℂ = Base ℂ fld
10 8 9 ressbas2 ⊢ 0 +∞ ⊆ ℂ → 0 +∞ = Base ℂ fld ↾ 𝑠 0 +∞
11 7 10 ax-mp ⊢ 0 +∞ = Base ℂ fld ↾ 𝑠 0 +∞
12 icossxr ⊢ 0 +∞ ⊆ ℝ *
13 eqid ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ = ℝ 𝑠 * ↾ 𝑠 0 +∞
14 xrsbas ⊢ ℝ * = Base ℝ 𝑠 *
15 13 14 ressbas2 ⊢ 0 +∞ ⊆ ℝ * → 0 +∞ = Base ℝ 𝑠 * ↾ 𝑠 0 +∞
16 12 15 ax-mp ⊢ 0 +∞ = Base ℝ 𝑠 * ↾ 𝑠 0 +∞
17 11 16 eqtr3i ⊢ Base ℂ fld ↾ 𝑠 0 +∞ = Base ℝ 𝑠 * ↾ 𝑠 0 +∞
18 17 a1i ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → Base ℂ fld ↾ 𝑠 0 +∞ = Base ℝ 𝑠 * ↾ 𝑠 0 +∞
19 simprl ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ ∧ x ∈ Base ℂ fld ↾ 𝑠 0 +∞ ∧ y ∈ Base ℂ fld ↾ 𝑠 0 +∞ → x ∈ Base ℂ fld ↾ 𝑠 0 +∞
20 19 11 eleqtrrdi ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ ∧ x ∈ Base ℂ fld ↾ 𝑠 0 +∞ ∧ y ∈ Base ℂ fld ↾ 𝑠 0 +∞ → x ∈ 0 +∞
21 simprr ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ ∧ x ∈ Base ℂ fld ↾ 𝑠 0 +∞ ∧ y ∈ Base ℂ fld ↾ 𝑠 0 +∞ → y ∈ Base ℂ fld ↾ 𝑠 0 +∞
22 21 11 eleqtrrdi ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ ∧ x ∈ Base ℂ fld ↾ 𝑠 0 +∞ ∧ y ∈ Base ℂ fld ↾ 𝑠 0 +∞ → y ∈ 0 +∞
23 ge0addcl ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x + y ∈ 0 +∞
24 ovex ⊢ 0 +∞ ∈ V
25 cnfldadd ⊢ + = + ℂ fld
26 8 25 ressplusg ⊢ 0 +∞ ∈ V → + = + ℂ fld ↾ 𝑠 0 +∞
27 24 26 ax-mp ⊢ + = + ℂ fld ↾ 𝑠 0 +∞
28 27 oveqi ⊢ x + y = x + ℂ fld ↾ 𝑠 0 +∞ y
29 23 28 11 3eltr3g ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x + ℂ fld ↾ 𝑠 0 +∞ y ∈ Base ℂ fld ↾ 𝑠 0 +∞
30 20 22 29 syl2anc ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ ∧ x ∈ Base ℂ fld ↾ 𝑠 0 +∞ ∧ y ∈ Base ℂ fld ↾ 𝑠 0 +∞ → x + ℂ fld ↾ 𝑠 0 +∞ y ∈ Base ℂ fld ↾ 𝑠 0 +∞
31 simpl ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x ∈ 0 +∞
32 5 31 sselid ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x ∈ ℝ
33 simpr ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → y ∈ 0 +∞
34 5 33 sselid ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → y ∈ ℝ
35 rexadd ⊢ x ∈ ℝ ∧ y ∈ ℝ → x + 𝑒 y = x + y
36 35 eqcomd ⊢ x ∈ ℝ ∧ y ∈ ℝ → x + y = x + 𝑒 y
37 32 34 36 syl2anc ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x + y = x + 𝑒 y
38 xrsadd ⊢ + 𝑒 = + ℝ 𝑠 *
39 13 38 ressplusg ⊢ 0 +∞ ∈ V → + 𝑒 = + ℝ 𝑠 * ↾ 𝑠 0 +∞
40 24 39 ax-mp ⊢ + 𝑒 = + ℝ 𝑠 * ↾ 𝑠 0 +∞
41 40 oveqi ⊢ x + 𝑒 y = x + ℝ 𝑠 * ↾ 𝑠 0 +∞ y
42 37 28 41 3eqtr3g ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x + ℂ fld ↾ 𝑠 0 +∞ y = x + ℝ 𝑠 * ↾ 𝑠 0 +∞ y
43 20 22 42 syl2anc ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ ∧ x ∈ Base ℂ fld ↾ 𝑠 0 +∞ ∧ y ∈ Base ℂ fld ↾ 𝑠 0 +∞ → x + ℂ fld ↾ 𝑠 0 +∞ y = x + ℝ 𝑠 * ↾ 𝑠 0 +∞ y
44 simpr ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → F : A ⟶ 0 +∞
45 44 ffund ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → Fun ⁡ F
46 44 frnd ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → ran ⁡ F ⊆ 0 +∞
47 46 11 sseqtrdi ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → ran ⁡ F ⊆ Base ℂ fld ↾ 𝑠 0 +∞
48 2 3 4 18 30 43 45 47 gsumpropd2 ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → ∑ ℂ fld ↾ 𝑠 0 +∞ F = ∑ ℝ 𝑠 * ↾ 𝑠 0 +∞ F
49 cnfldex ⊢ ℂ fld ∈ V
50 49 a1i ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → ℂ fld ∈ V
51 simpl ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → A ∈ V
52 7 a1i ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → 0 +∞ ⊆ ℂ
53 0e0icopnf ⊢ 0 ∈ 0 +∞
54 53 a1i ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → 0 ∈ 0 +∞
55 simpr ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ ∧ x ∈ ℂ → x ∈ ℂ
56 55 addid2d ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ ∧ x ∈ ℂ → 0 + x = x
57 55 addid1d ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ ∧ x ∈ ℂ → x + 0 = x
58 56 57 jca ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ ∧ x ∈ ℂ → 0 + x = x ∧ x + 0 = x
59 9 25 8 50 51 52 44 54 58 gsumress ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → ∑ ℂ fld F = ∑ ℂ fld ↾ 𝑠 0 +∞ F
60 xrge0base ⊢ 0 +∞ = Base ℝ 𝑠 * ↾ 𝑠 0 +∞
61 xrge0plusg ⊢ + 𝑒 = + ℝ 𝑠 * ↾ 𝑠 0 +∞
62 ovex ⊢ 0 +∞ ∈ V
63 ressress ⊢ 0 +∞ ∈ V ∧ 0 +∞ ∈ V → ℝ 𝑠 * ↾ 𝑠 0 +∞ ↾ 𝑠 0 +∞ = ℝ 𝑠 * ↾ 𝑠 0 +∞ ∩ 0 +∞
64 62 24 63 mp2an ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ↾ 𝑠 0 +∞ = ℝ 𝑠 * ↾ 𝑠 0 +∞ ∩ 0 +∞
65 incom ⊢ 0 +∞ ∩ 0 +∞ = 0 +∞ ∩ 0 +∞
66 icossicc ⊢ 0 +∞ ⊆ 0 +∞
67 dfss ⊢ 0 +∞ ⊆ 0 +∞ ↔ 0 +∞ = 0 +∞ ∩ 0 +∞
68 66 67 mpbi ⊢ 0 +∞ = 0 +∞ ∩ 0 +∞
69 65 68 eqtr4i ⊢ 0 +∞ ∩ 0 +∞ = 0 +∞
70 69 oveq2i ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∩ 0 +∞ = ℝ 𝑠 * ↾ 𝑠 0 +∞
71 64 70 eqtr2i ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ = ℝ 𝑠 * ↾ 𝑠 0 +∞ ↾ 𝑠 0 +∞
72 ovexd ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ V
73 66 a1i ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → 0 +∞ ⊆ 0 +∞
74 iccssxr ⊢ 0 +∞ ⊆ ℝ *
75 simpr ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ ∧ x ∈ 0 +∞ → x ∈ 0 +∞
76 74 75 sselid ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ ∧ x ∈ 0 +∞ → x ∈ ℝ *
77 xaddid2 ⊢ x ∈ ℝ * → 0 + 𝑒 x = x
78 76 77 syl ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ ∧ x ∈ 0 +∞ → 0 + 𝑒 x = x
79 xaddid1 ⊢ x ∈ ℝ * → x + 𝑒 0 = x
80 76 79 syl ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ ∧ x ∈ 0 +∞ → x + 𝑒 0 = x
81 78 80 jca ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ ∧ x ∈ 0 +∞ → 0 + 𝑒 x = x ∧ x + 𝑒 0 = x
82 60 61 71 72 51 73 44 54 81 gsumress ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → ∑ ℝ 𝑠 * ↾ 𝑠 0 +∞ F = ∑ ℝ 𝑠 * ↾ 𝑠 0 +∞ F
83 48 59 82 3eqtr4d ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → ∑ ℂ fld F = ∑ ℝ 𝑠 * ↾ 𝑠 0 +∞ F