Step | Hyp | Ref
| Expression |
1 | | fex 7002 |
. . . 4
⊢ ((𝐹:𝐴⟶(0[,)+∞) ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
2 | 1 | ancoms 462 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → 𝐹 ∈ V) |
3 | | ovexd 7208 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(ℂfld ↾s (0[,)+∞)) ∈
V) |
4 | | ovexd 7208 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(ℝ*𝑠 ↾s (0[,)+∞))
∈ V) |
5 | | rge0ssre 12933 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℝ |
6 | | ax-resscn 10675 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
7 | 5, 6 | sstri 3887 |
. . . . . 6
⊢
(0[,)+∞) ⊆ ℂ |
8 | | eqid 2739 |
. . . . . . 7
⊢
(ℂfld ↾s (0[,)+∞)) =
(ℂfld ↾s (0[,)+∞)) |
9 | | cnfldbas 20224 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
10 | 8, 9 | ressbas2 16661 |
. . . . . 6
⊢
((0[,)+∞) ⊆ ℂ → (0[,)+∞) =
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
11 | 7, 10 | ax-mp 5 |
. . . . 5
⊢
(0[,)+∞) = (Base‘(ℂfld ↾s
(0[,)+∞))) |
12 | | icossxr 12909 |
. . . . . 6
⊢
(0[,)+∞) ⊆ ℝ* |
13 | | eqid 2739 |
. . . . . . 7
⊢
(ℝ*𝑠 ↾s
(0[,)+∞)) = (ℝ*𝑠 ↾s
(0[,)+∞)) |
14 | | xrsbas 20236 |
. . . . . . 7
⊢
ℝ* =
(Base‘ℝ*𝑠) |
15 | 13, 14 | ressbas2 16661 |
. . . . . 6
⊢
((0[,)+∞) ⊆ ℝ* → (0[,)+∞) =
(Base‘(ℝ*𝑠 ↾s
(0[,)+∞)))) |
16 | 12, 15 | ax-mp 5 |
. . . . 5
⊢
(0[,)+∞) = (Base‘(ℝ*𝑠
↾s (0[,)+∞))) |
17 | 11, 16 | eqtr3i 2764 |
. . . 4
⊢
(Base‘(ℂfld ↾s (0[,)+∞)))
= (Base‘(ℝ*𝑠 ↾s
(0[,)+∞))) |
18 | 17 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(Base‘(ℂfld ↾s (0[,)+∞))) =
(Base‘(ℝ*𝑠 ↾s
(0[,)+∞)))) |
19 | | simprl 771 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑦 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))))
→ 𝑥 ∈
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
20 | 19, 11 | eleqtrrdi 2845 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑦 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))))
→ 𝑥 ∈
(0[,)+∞)) |
21 | | simprr 773 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑦 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))))
→ 𝑦 ∈
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
22 | 21, 11 | eleqtrrdi 2845 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑦 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))))
→ 𝑦 ∈
(0[,)+∞)) |
23 | | ge0addcl 12937 |
. . . . 5
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ (𝑥 + 𝑦) ∈
(0[,)+∞)) |
24 | | ovex 7206 |
. . . . . . 7
⊢
(0[,)+∞) ∈ V |
25 | | cnfldadd 20225 |
. . . . . . . 8
⊢ + =
(+g‘ℂfld) |
26 | 8, 25 | ressplusg 16718 |
. . . . . . 7
⊢
((0[,)+∞) ∈ V → + =
(+g‘(ℂfld ↾s
(0[,)+∞)))) |
27 | 24, 26 | ax-mp 5 |
. . . . . 6
⊢ + =
(+g‘(ℂfld ↾s
(0[,)+∞))) |
28 | 27 | oveqi 7186 |
. . . . 5
⊢ (𝑥 + 𝑦) = (𝑥(+g‘(ℂfld
↾s (0[,)+∞)))𝑦) |
29 | 23, 28, 11 | 3eltr3g 2850 |
. . . 4
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ (𝑥(+g‘(ℂfld
↾s (0[,)+∞)))𝑦) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
30 | 20, 22, 29 | syl2anc 587 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑦 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))))
→ (𝑥(+g‘(ℂfld
↾s (0[,)+∞)))𝑦) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
31 | | simpl 486 |
. . . . . . 7
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ 𝑥 ∈
(0[,)+∞)) |
32 | 5, 31 | sseldi 3876 |
. . . . . 6
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ 𝑥 ∈
ℝ) |
33 | | simpr 488 |
. . . . . . 7
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ 𝑦 ∈
(0[,)+∞)) |
34 | 5, 33 | sseldi 3876 |
. . . . . 6
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ 𝑦 ∈
ℝ) |
35 | | rexadd 12711 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 +𝑒 𝑦) = (𝑥 + 𝑦)) |
36 | 35 | eqcomd 2745 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) = (𝑥 +𝑒 𝑦)) |
37 | 32, 34, 36 | syl2anc 587 |
. . . . 5
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ (𝑥 + 𝑦) = (𝑥 +𝑒 𝑦)) |
38 | | xrsadd 20237 |
. . . . . . . 8
⊢
+𝑒 =
(+g‘ℝ*𝑠) |
39 | 13, 38 | ressplusg 16718 |
. . . . . . 7
⊢
((0[,)+∞) ∈ V → +𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,)+∞)))) |
40 | 24, 39 | ax-mp 5 |
. . . . . 6
⊢
+𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,)+∞))) |
41 | 40 | oveqi 7186 |
. . . . 5
⊢ (𝑥 +𝑒 𝑦) = (𝑥(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑦) |
42 | 37, 28, 41 | 3eqtr3g 2797 |
. . . 4
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ (𝑥(+g‘(ℂfld
↾s (0[,)+∞)))𝑦) = (𝑥(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑦)) |
43 | 20, 22, 42 | syl2anc 587 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑦 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))))
→ (𝑥(+g‘(ℂfld
↾s (0[,)+∞)))𝑦) = (𝑥(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑦)) |
44 | | simpr 488 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → 𝐹:𝐴⟶(0[,)+∞)) |
45 | 44 | ffund 6509 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → Fun 𝐹) |
46 | 44 | frnd 6513 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → ran 𝐹 ⊆
(0[,)+∞)) |
47 | 46, 11 | sseqtrdi 3928 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → ran 𝐹 ⊆
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
48 | 2, 3, 4, 18, 30, 43, 45, 47 | gsumpropd2 18009 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
((ℂfld ↾s (0[,)+∞))
Σg 𝐹) =
((ℝ*𝑠 ↾s (0[,)+∞))
Σg 𝐹)) |
49 | | cnfldex 20223 |
. . . 4
⊢
ℂfld ∈ V |
50 | 49 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
ℂfld ∈ V) |
51 | | simpl 486 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → 𝐴 ∈ 𝑉) |
52 | 7 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(0[,)+∞) ⊆ ℂ) |
53 | | 0e0icopnf 12935 |
. . . 4
⊢ 0 ∈
(0[,)+∞) |
54 | 53 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → 0 ∈
(0[,)+∞)) |
55 | | simpr 488 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ ℂ) → 𝑥 ∈
ℂ) |
56 | 55 | addid2d 10922 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ ℂ) → (0 +
𝑥) = 𝑥) |
57 | 55 | addid1d 10921 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ ℂ) → (𝑥 + 0) = 𝑥) |
58 | 56, 57 | jca 515 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ ℂ) → ((0 +
𝑥) = 𝑥 ∧ (𝑥 + 0) = 𝑥)) |
59 | 9, 25, 8, 50, 51, 52, 44, 54, 58 | gsumress 18011 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(ℂfld Σg 𝐹) = ((ℂfld
↾s (0[,)+∞)) Σg 𝐹)) |
60 | | xrge0base 30874 |
. . 3
⊢
(0[,]+∞) = (Base‘(ℝ*𝑠
↾s (0[,]+∞))) |
61 | | xrge0plusg 30876 |
. . 3
⊢
+𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,]+∞))) |
62 | | ovex 7206 |
. . . . 5
⊢
(0[,]+∞) ∈ V |
63 | | ressress 16668 |
. . . . 5
⊢
(((0[,]+∞) ∈ V ∧ (0[,)+∞) ∈ V) →
((ℝ*𝑠 ↾s (0[,]+∞))
↾s (0[,)+∞)) = (ℝ*𝑠
↾s ((0[,]+∞) ∩ (0[,)+∞)))) |
64 | 62, 24, 63 | mp2an 692 |
. . . 4
⊢
((ℝ*𝑠 ↾s
(0[,]+∞)) ↾s (0[,)+∞)) =
(ℝ*𝑠 ↾s ((0[,]+∞)
∩ (0[,)+∞))) |
65 | | incom 4092 |
. . . . . 6
⊢
((0[,]+∞) ∩ (0[,)+∞)) = ((0[,)+∞) ∩
(0[,]+∞)) |
66 | | icossicc 12913 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
67 | | dfss 3862 |
. . . . . . 7
⊢
((0[,)+∞) ⊆ (0[,]+∞) ↔ (0[,)+∞) =
((0[,)+∞) ∩ (0[,]+∞))) |
68 | 66, 67 | mpbi 233 |
. . . . . 6
⊢
(0[,)+∞) = ((0[,)+∞) ∩ (0[,]+∞)) |
69 | 65, 68 | eqtr4i 2765 |
. . . . 5
⊢
((0[,]+∞) ∩ (0[,)+∞)) = (0[,)+∞) |
70 | 69 | oveq2i 7184 |
. . . 4
⊢
(ℝ*𝑠 ↾s
((0[,]+∞) ∩ (0[,)+∞))) =
(ℝ*𝑠 ↾s
(0[,)+∞)) |
71 | 64, 70 | eqtr2i 2763 |
. . 3
⊢
(ℝ*𝑠 ↾s
(0[,)+∞)) = ((ℝ*𝑠 ↾s
(0[,]+∞)) ↾s (0[,)+∞)) |
72 | | ovexd 7208 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(ℝ*𝑠 ↾s (0[,]+∞))
∈ V) |
73 | 66 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(0[,)+∞) ⊆ (0[,]+∞)) |
74 | | iccssxr 12907 |
. . . . . 6
⊢
(0[,]+∞) ⊆ ℝ* |
75 | | simpr 488 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) →
𝑥 ∈
(0[,]+∞)) |
76 | 74, 75 | sseldi 3876 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) →
𝑥 ∈
ℝ*) |
77 | | xaddid2 12721 |
. . . . 5
⊢ (𝑥 ∈ ℝ*
→ (0 +𝑒 𝑥) = 𝑥) |
78 | 76, 77 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) →
(0 +𝑒 𝑥)
= 𝑥) |
79 | | xaddid1 12720 |
. . . . 5
⊢ (𝑥 ∈ ℝ*
→ (𝑥
+𝑒 0) = 𝑥) |
80 | 76, 79 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) →
(𝑥 +𝑒 0)
= 𝑥) |
81 | 78, 80 | jca 515 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) →
((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥)) |
82 | 60, 61, 71, 72, 51, 73, 44, 54, 81 | gsumress 18011 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg 𝐹) =
((ℝ*𝑠 ↾s (0[,)+∞))
Σg 𝐹)) |
83 | 48, 59, 82 | 3eqtr4d 2784 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(ℂfld Σg 𝐹) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg 𝐹)) |