Metamath Proof Explorer

Theorem esumpfinvallem

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

Ref Expression
Assertion esumpfinvallem ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) → ( ℂfld Σg 𝐹 ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg 𝐹 ) )

Proof

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