Step | Hyp | Ref
| Expression |
1 | | fex 6394 |
. . . 4
⊢ ((𝐹:𝐴⟶(0[,)+∞) ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
2 | 1 | ancoms 468 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → 𝐹 ∈ V) |
3 | | ovex 6577 |
. . . 4
⊢
(ℂfld ↾s (0[,)+∞)) ∈
V |
4 | 3 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(ℂfld ↾s (0[,)+∞)) ∈
V) |
5 | | ovex 6577 |
. . . 4
⊢
(ℝ*𝑠 ↾s
(0[,)+∞)) ∈ V |
6 | 5 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(ℝ*𝑠 ↾s (0[,)+∞))
∈ V) |
7 | | rge0ssre 12151 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℝ |
8 | | ax-resscn 9872 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
9 | 7, 8 | sstri 3577 |
. . . . . 6
⊢
(0[,)+∞) ⊆ ℂ |
10 | | eqid 2610 |
. . . . . . 7
⊢
(ℂfld ↾s (0[,)+∞)) =
(ℂfld ↾s (0[,)+∞)) |
11 | | cnfldbas 19571 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
12 | 10, 11 | ressbas2 15758 |
. . . . . 6
⊢
((0[,)+∞) ⊆ ℂ → (0[,)+∞) =
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
13 | 9, 12 | ax-mp 5 |
. . . . 5
⊢
(0[,)+∞) = (Base‘(ℂfld ↾s
(0[,)+∞))) |
14 | | icossxr 12129 |
. . . . . 6
⊢
(0[,)+∞) ⊆ ℝ* |
15 | | eqid 2610 |
. . . . . . 7
⊢
(ℝ*𝑠 ↾s
(0[,)+∞)) = (ℝ*𝑠 ↾s
(0[,)+∞)) |
16 | | xrsbas 19581 |
. . . . . . 7
⊢
ℝ* =
(Base‘ℝ*𝑠) |
17 | 15, 16 | ressbas2 15758 |
. . . . . 6
⊢
((0[,)+∞) ⊆ ℝ* → (0[,)+∞) =
(Base‘(ℝ*𝑠 ↾s
(0[,)+∞)))) |
18 | 14, 17 | ax-mp 5 |
. . . . 5
⊢
(0[,)+∞) = (Base‘(ℝ*𝑠
↾s (0[,)+∞))) |
19 | 13, 18 | eqtr3i 2634 |
. . . 4
⊢
(Base‘(ℂfld ↾s (0[,)+∞)))
= (Base‘(ℝ*𝑠 ↾s
(0[,)+∞))) |
20 | 19 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(Base‘(ℂfld ↾s (0[,)+∞))) =
(Base‘(ℝ*𝑠 ↾s
(0[,)+∞)))) |
21 | | simprl 790 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑦 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))))
→ 𝑥 ∈
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
22 | 21, 13 | syl6eleqr 2699 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑦 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))))
→ 𝑥 ∈
(0[,)+∞)) |
23 | | simprr 792 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑦 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))))
→ 𝑦 ∈
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
24 | 23, 13 | syl6eleqr 2699 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑦 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))))
→ 𝑦 ∈
(0[,)+∞)) |
25 | | ge0addcl 12155 |
. . . . 5
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ (𝑥 + 𝑦) ∈
(0[,)+∞)) |
26 | | ovex 6577 |
. . . . . . 7
⊢
(0[,)+∞) ∈ V |
27 | | cnfldadd 19572 |
. . . . . . . 8
⊢ + =
(+g‘ℂfld) |
28 | 10, 27 | ressplusg 15818 |
. . . . . . 7
⊢
((0[,)+∞) ∈ V → + =
(+g‘(ℂfld ↾s
(0[,)+∞)))) |
29 | 26, 28 | ax-mp 5 |
. . . . . 6
⊢ + =
(+g‘(ℂfld ↾s
(0[,)+∞))) |
30 | 29 | oveqi 6562 |
. . . . 5
⊢ (𝑥 + 𝑦) = (𝑥(+g‘(ℂfld
↾s (0[,)+∞)))𝑦) |
31 | 25, 30, 13 | 3eltr3g 2704 |
. . . 4
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ (𝑥(+g‘(ℂfld
↾s (0[,)+∞)))𝑦) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
32 | 22, 24, 31 | syl2anc 691 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑦 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))))
→ (𝑥(+g‘(ℂfld
↾s (0[,)+∞)))𝑦) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
33 | | simpl 472 |
. . . . . . 7
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ 𝑥 ∈
(0[,)+∞)) |
34 | 7, 33 | sseldi 3566 |
. . . . . 6
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ 𝑥 ∈
ℝ) |
35 | | simpr 476 |
. . . . . . 7
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ 𝑦 ∈
(0[,)+∞)) |
36 | 7, 35 | sseldi 3566 |
. . . . . 6
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ 𝑦 ∈
ℝ) |
37 | | rexadd 11937 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 +𝑒 𝑦) = (𝑥 + 𝑦)) |
38 | 37 | eqcomd 2616 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) = (𝑥 +𝑒 𝑦)) |
39 | 34, 36, 38 | syl2anc 691 |
. . . . 5
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ (𝑥 + 𝑦) = (𝑥 +𝑒 𝑦)) |
40 | | xrsadd 19582 |
. . . . . . . 8
⊢
+𝑒 =
(+g‘ℝ*𝑠) |
41 | 15, 40 | ressplusg 15818 |
. . . . . . 7
⊢
((0[,)+∞) ∈ V → +𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,)+∞)))) |
42 | 26, 41 | ax-mp 5 |
. . . . . 6
⊢
+𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,)+∞))) |
43 | 42 | oveqi 6562 |
. . . . 5
⊢ (𝑥 +𝑒 𝑦) = (𝑥(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑦) |
44 | 39, 30, 43 | 3eqtr3g 2667 |
. . . 4
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ (𝑥(+g‘(ℂfld
↾s (0[,)+∞)))𝑦) = (𝑥(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑦)) |
45 | 22, 24, 44 | syl2anc 691 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑦 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))))
→ (𝑥(+g‘(ℂfld
↾s (0[,)+∞)))𝑦) = (𝑥(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑦)) |
46 | | simpr 476 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → 𝐹:𝐴⟶(0[,)+∞)) |
47 | | ffun 5961 |
. . . 4
⊢ (𝐹:𝐴⟶(0[,)+∞) → Fun 𝐹) |
48 | 46, 47 | syl 17 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → Fun 𝐹) |
49 | | frn 5966 |
. . . . 5
⊢ (𝐹:𝐴⟶(0[,)+∞) → ran 𝐹 ⊆
(0[,)+∞)) |
50 | 46, 49 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → ran 𝐹 ⊆
(0[,)+∞)) |
51 | 50, 13 | syl6sseq 3614 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → ran 𝐹 ⊆
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
52 | 2, 4, 6, 20, 32, 45, 48, 51 | gsumpropd2 17097 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
((ℂfld ↾s (0[,)+∞))
Σg 𝐹) =
((ℝ*𝑠 ↾s (0[,)+∞))
Σg 𝐹)) |
53 | | cnfldex 19570 |
. . . 4
⊢
ℂfld ∈ V |
54 | 53 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
ℂfld ∈ V) |
55 | | simpl 472 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → 𝐴 ∈ 𝑉) |
56 | 9 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(0[,)+∞) ⊆ ℂ) |
57 | | 0e0icopnf 12153 |
. . . 4
⊢ 0 ∈
(0[,)+∞) |
58 | 57 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → 0 ∈
(0[,)+∞)) |
59 | | simpr 476 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ ℂ) → 𝑥 ∈
ℂ) |
60 | 59 | addid2d 10116 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ ℂ) → (0 +
𝑥) = 𝑥) |
61 | 59 | addid1d 10115 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ ℂ) → (𝑥 + 0) = 𝑥) |
62 | 60, 61 | jca 553 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ ℂ) → ((0 +
𝑥) = 𝑥 ∧ (𝑥 + 0) = 𝑥)) |
63 | 11, 27, 10, 54, 55, 56, 46, 58, 62 | gsumress 17099 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(ℂfld Σg 𝐹) = ((ℂfld
↾s (0[,)+∞)) Σg 𝐹)) |
64 | | xrge0base 29016 |
. . 3
⊢
(0[,]+∞) = (Base‘(ℝ*𝑠
↾s (0[,]+∞))) |
65 | | xrge0plusg 29018 |
. . 3
⊢
+𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,]+∞))) |
66 | | ovex 6577 |
. . . . 5
⊢
(0[,]+∞) ∈ V |
67 | | ressress 15765 |
. . . . 5
⊢
(((0[,]+∞) ∈ V ∧ (0[,)+∞) ∈ V) →
((ℝ*𝑠 ↾s (0[,]+∞))
↾s (0[,)+∞)) = (ℝ*𝑠
↾s ((0[,]+∞) ∩ (0[,)+∞)))) |
68 | 66, 26, 67 | mp2an 704 |
. . . 4
⊢
((ℝ*𝑠 ↾s
(0[,]+∞)) ↾s (0[,)+∞)) =
(ℝ*𝑠 ↾s ((0[,]+∞)
∩ (0[,)+∞))) |
69 | | incom 3767 |
. . . . . 6
⊢
((0[,]+∞) ∩ (0[,)+∞)) = ((0[,)+∞) ∩
(0[,]+∞)) |
70 | | icossicc 12131 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
71 | | dfss 3555 |
. . . . . . 7
⊢
((0[,)+∞) ⊆ (0[,]+∞) ↔ (0[,)+∞) =
((0[,)+∞) ∩ (0[,]+∞))) |
72 | 70, 71 | mpbi 219 |
. . . . . 6
⊢
(0[,)+∞) = ((0[,)+∞) ∩ (0[,]+∞)) |
73 | 69, 72 | eqtr4i 2635 |
. . . . 5
⊢
((0[,]+∞) ∩ (0[,)+∞)) = (0[,)+∞) |
74 | 73 | oveq2i 6560 |
. . . 4
⊢
(ℝ*𝑠 ↾s
((0[,]+∞) ∩ (0[,)+∞))) =
(ℝ*𝑠 ↾s
(0[,)+∞)) |
75 | 68, 74 | eqtr2i 2633 |
. . 3
⊢
(ℝ*𝑠 ↾s
(0[,)+∞)) = ((ℝ*𝑠 ↾s
(0[,]+∞)) ↾s (0[,)+∞)) |
76 | | ovex 6577 |
. . . 4
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ V |
77 | 76 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(ℝ*𝑠 ↾s (0[,]+∞))
∈ V) |
78 | 70 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(0[,)+∞) ⊆ (0[,]+∞)) |
79 | | iccssxr 12127 |
. . . . . 6
⊢
(0[,]+∞) ⊆ ℝ* |
80 | | simpr 476 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) →
𝑥 ∈
(0[,]+∞)) |
81 | 79, 80 | sseldi 3566 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) →
𝑥 ∈
ℝ*) |
82 | | xaddid2 11947 |
. . . . 5
⊢ (𝑥 ∈ ℝ*
→ (0 +𝑒 𝑥) = 𝑥) |
83 | 81, 82 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) →
(0 +𝑒 𝑥)
= 𝑥) |
84 | | xaddid1 11946 |
. . . . 5
⊢ (𝑥 ∈ ℝ*
→ (𝑥
+𝑒 0) = 𝑥) |
85 | 81, 84 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) →
(𝑥 +𝑒 0)
= 𝑥) |
86 | 83, 85 | jca 553 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) →
((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥)) |
87 | 64, 65, 75, 77, 55, 78, 46, 58, 86 | gsumress 17099 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg 𝐹) =
((ℝ*𝑠 ↾s (0[,)+∞))
Σg 𝐹)) |
88 | 52, 63, 87 | 3eqtr4d 2654 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(ℂfld Σg 𝐹) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg 𝐹)) |