| Step | Hyp | Ref
| Expression |
| 1 | | fex 7246 |
. . . 4
⊢ ((𝐹:𝐴⟶(0[,)+∞) ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
| 2 | 1 | ancoms 458 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → 𝐹 ∈ V) |
| 3 | | ovexd 7466 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(ℂfld ↾s (0[,)+∞)) ∈
V) |
| 4 | | ovexd 7466 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(ℝ*𝑠 ↾s (0[,)+∞))
∈ V) |
| 5 | | rge0ssre 13496 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℝ |
| 6 | | ax-resscn 11212 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
| 7 | 5, 6 | sstri 3993 |
. . . . . 6
⊢
(0[,)+∞) ⊆ ℂ |
| 8 | | eqid 2737 |
. . . . . . 7
⊢
(ℂfld ↾s (0[,)+∞)) =
(ℂfld ↾s (0[,)+∞)) |
| 9 | | cnfldbas 21368 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
| 10 | 8, 9 | ressbas2 17283 |
. . . . . 6
⊢
((0[,)+∞) ⊆ ℂ → (0[,)+∞) =
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
| 11 | 7, 10 | ax-mp 5 |
. . . . 5
⊢
(0[,)+∞) = (Base‘(ℂfld ↾s
(0[,)+∞))) |
| 12 | | icossxr 13472 |
. . . . . 6
⊢
(0[,)+∞) ⊆ ℝ* |
| 13 | | eqid 2737 |
. . . . . . 7
⊢
(ℝ*𝑠 ↾s
(0[,)+∞)) = (ℝ*𝑠 ↾s
(0[,)+∞)) |
| 14 | | xrsbas 21396 |
. . . . . . 7
⊢
ℝ* =
(Base‘ℝ*𝑠) |
| 15 | 13, 14 | ressbas2 17283 |
. . . . . 6
⊢
((0[,)+∞) ⊆ ℝ* → (0[,)+∞) =
(Base‘(ℝ*𝑠 ↾s
(0[,)+∞)))) |
| 16 | 12, 15 | ax-mp 5 |
. . . . 5
⊢
(0[,)+∞) = (Base‘(ℝ*𝑠
↾s (0[,)+∞))) |
| 17 | 11, 16 | eqtr3i 2767 |
. . . 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 2852 |
. . . 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 2852 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑦 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))))
→ 𝑦 ∈
(0[,)+∞)) |
| 23 | | ge0addcl 13500 |
. . . . 5
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ (𝑥 + 𝑦) ∈
(0[,)+∞)) |
| 24 | | ovex 7464 |
. . . . . . 7
⊢
(0[,)+∞) ∈ V |
| 25 | | cnfldadd 21370 |
. . . . . . . 8
⊢ + =
(+g‘ℂfld) |
| 26 | 8, 25 | ressplusg 17334 |
. . . . . . 7
⊢
((0[,)+∞) ∈ V → + =
(+g‘(ℂfld ↾s
(0[,)+∞)))) |
| 27 | 24, 26 | ax-mp 5 |
. . . . . 6
⊢ + =
(+g‘(ℂfld ↾s
(0[,)+∞))) |
| 28 | 27 | oveqi 7444 |
. . . . 5
⊢ (𝑥 + 𝑦) = (𝑥(+g‘(ℂfld
↾s (0[,)+∞)))𝑦) |
| 29 | 23, 28, 11 | 3eltr3g 2857 |
. . . 4
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ (𝑥(+g‘(ℂfld
↾s (0[,)+∞)))𝑦) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
| 30 | 20, 22, 29 | syl2anc 584 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑦 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))))
→ (𝑥(+g‘(ℂfld
↾s (0[,)+∞)))𝑦) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
| 31 | | simpl 482 |
. . . . . . 7
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ 𝑥 ∈
(0[,)+∞)) |
| 32 | 5, 31 | sselid 3981 |
. . . . . 6
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ 𝑥 ∈
ℝ) |
| 33 | | simpr 484 |
. . . . . . 7
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ 𝑦 ∈
(0[,)+∞)) |
| 34 | 5, 33 | sselid 3981 |
. . . . . 6
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ 𝑦 ∈
ℝ) |
| 35 | | rexadd 13274 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 +𝑒 𝑦) = (𝑥 + 𝑦)) |
| 36 | 35 | eqcomd 2743 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) = (𝑥 +𝑒 𝑦)) |
| 37 | 32, 34, 36 | syl2anc 584 |
. . . . 5
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ (𝑥 + 𝑦) = (𝑥 +𝑒 𝑦)) |
| 38 | | xrsadd 21397 |
. . . . . . . 8
⊢
+𝑒 =
(+g‘ℝ*𝑠) |
| 39 | 13, 38 | ressplusg 17334 |
. . . . . . 7
⊢
((0[,)+∞) ∈ V → +𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,)+∞)))) |
| 40 | 24, 39 | ax-mp 5 |
. . . . . 6
⊢
+𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,)+∞))) |
| 41 | 40 | oveqi 7444 |
. . . . 5
⊢ (𝑥 +𝑒 𝑦) = (𝑥(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑦) |
| 42 | 37, 28, 41 | 3eqtr3g 2800 |
. . . 4
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ (𝑥(+g‘(ℂfld
↾s (0[,)+∞)))𝑦) = (𝑥(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑦)) |
| 43 | 20, 22, 42 | syl2anc 584 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑦 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))))
→ (𝑥(+g‘(ℂfld
↾s (0[,)+∞)))𝑦) = (𝑥(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑦)) |
| 44 | | simpr 484 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → 𝐹:𝐴⟶(0[,)+∞)) |
| 45 | 44 | ffund 6740 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → Fun 𝐹) |
| 46 | 44 | frnd 6744 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → ran 𝐹 ⊆
(0[,)+∞)) |
| 47 | 46, 11 | sseqtrdi 4024 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → ran 𝐹 ⊆
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
| 48 | 2, 3, 4, 18, 30, 43, 45, 47 | gsumpropd2 18693 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
((ℂfld ↾s (0[,)+∞))
Σg 𝐹) =
((ℝ*𝑠 ↾s (0[,)+∞))
Σg 𝐹)) |
| 49 | | cnfldex 21367 |
. . . 4
⊢
ℂfld ∈ V |
| 50 | 49 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
ℂfld ∈ V) |
| 51 | | simpl 482 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → 𝐴 ∈ 𝑉) |
| 52 | 7 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(0[,)+∞) ⊆ ℂ) |
| 53 | | 0e0icopnf 13498 |
. . . 4
⊢ 0 ∈
(0[,)+∞) |
| 54 | 53 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → 0 ∈
(0[,)+∞)) |
| 55 | | simpr 484 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ ℂ) → 𝑥 ∈
ℂ) |
| 56 | 55 | addlidd 11462 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ ℂ) → (0 +
𝑥) = 𝑥) |
| 57 | 55 | addridd 11461 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ ℂ) → (𝑥 + 0) = 𝑥) |
| 58 | 56, 57 | jca 511 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ ℂ) → ((0 +
𝑥) = 𝑥 ∧ (𝑥 + 0) = 𝑥)) |
| 59 | 9, 25, 8, 50, 51, 52, 44, 54, 58 | gsumress 18695 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(ℂfld Σg 𝐹) = ((ℂfld
↾s (0[,)+∞)) Σg 𝐹)) |
| 60 | | xrge0base 33016 |
. . 3
⊢
(0[,]+∞) = (Base‘(ℝ*𝑠
↾s (0[,]+∞))) |
| 61 | | xrge0plusg 33018 |
. . 3
⊢
+𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,]+∞))) |
| 62 | | ovex 7464 |
. . . . 5
⊢
(0[,]+∞) ∈ V |
| 63 | | ressress 17293 |
. . . . 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 4209 |
. . . . . 6
⊢
((0[,]+∞) ∩ (0[,)+∞)) = ((0[,)+∞) ∩
(0[,]+∞)) |
| 66 | | icossicc 13476 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
| 67 | | dfss 3970 |
. . . . . . 7
⊢
((0[,)+∞) ⊆ (0[,]+∞) ↔ (0[,)+∞) =
((0[,)+∞) ∩ (0[,]+∞))) |
| 68 | 66, 67 | mpbi 230 |
. . . . . 6
⊢
(0[,)+∞) = ((0[,)+∞) ∩ (0[,]+∞)) |
| 69 | 65, 68 | eqtr4i 2768 |
. . . . 5
⊢
((0[,]+∞) ∩ (0[,)+∞)) = (0[,)+∞) |
| 70 | 69 | oveq2i 7442 |
. . . 4
⊢
(ℝ*𝑠 ↾s
((0[,]+∞) ∩ (0[,)+∞))) =
(ℝ*𝑠 ↾s
(0[,)+∞)) |
| 71 | 64, 70 | eqtr2i 2766 |
. . 3
⊢
(ℝ*𝑠 ↾s
(0[,)+∞)) = ((ℝ*𝑠 ↾s
(0[,]+∞)) ↾s (0[,)+∞)) |
| 72 | | ovexd 7466 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(ℝ*𝑠 ↾s (0[,]+∞))
∈ V) |
| 73 | 66 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(0[,)+∞) ⊆ (0[,]+∞)) |
| 74 | | iccssxr 13470 |
. . . . . 6
⊢
(0[,]+∞) ⊆ ℝ* |
| 75 | | simpr 484 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) →
𝑥 ∈
(0[,]+∞)) |
| 76 | 74, 75 | sselid 3981 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) →
𝑥 ∈
ℝ*) |
| 77 | | xaddlid 13284 |
. . . . 5
⊢ (𝑥 ∈ ℝ*
→ (0 +𝑒 𝑥) = 𝑥) |
| 78 | 76, 77 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) →
(0 +𝑒 𝑥)
= 𝑥) |
| 79 | | xaddrid 13283 |
. . . . 5
⊢ (𝑥 ∈ ℝ*
→ (𝑥
+𝑒 0) = 𝑥) |
| 80 | 76, 79 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) →
(𝑥 +𝑒 0)
= 𝑥) |
| 81 | 78, 80 | jca 511 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) →
((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥)) |
| 82 | 60, 61, 71, 72, 51, 73, 44, 54, 81 | gsumress 18695 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg 𝐹) =
((ℝ*𝑠 ↾s (0[,)+∞))
Σg 𝐹)) |
| 83 | 48, 59, 82 | 3eqtr4d 2787 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(ℂfld Σg 𝐹) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg 𝐹)) |