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+∞→∑ℂfldF=∑ℝ𝑠*↾𝑠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 addlidd ⊢A∈V∧F:A⟶0+∞∧x∈ℂ→0+x=x
57 55 addridd ⊢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+∞→∑ℂfldF=∑ℂ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 xaddlid ⊢x∈ℝ*→0+𝑒x=x
78 76 77 syl ⊢A∈V∧F:A⟶0+∞∧x∈0+∞→0+𝑒x=x
79 xaddrid ⊢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+∞→∑ℂfldF=∑ℝ𝑠*↾𝑠0+∞F