Proof of Theorem gsumge0cl
Step | Hyp | Ref
| Expression |
1 | | iccssxr 13018 |
. . . . 5
⊢
(0[,]+∞) ⊆ ℝ* |
2 | | df-ss 3883 |
. . . . 5
⊢
((0[,]+∞) ⊆ ℝ* ↔ ((0[,]+∞) ∩
ℝ*) = (0[,]+∞)) |
3 | 1, 2 | mpbi 233 |
. . . 4
⊢
((0[,]+∞) ∩ ℝ*) =
(0[,]+∞) |
4 | 3 | eqcomi 2746 |
. . 3
⊢
(0[,]+∞) = ((0[,]+∞) ∩
ℝ*) |
5 | | ovex 7246 |
. . . 4
⊢
(0[,]+∞) ∈ V |
6 | | gsumge0cl.1 |
. . . . 5
⊢ 𝐺 =
(ℝ*𝑠 ↾s
(0[,]+∞)) |
7 | | xrsbas 20379 |
. . . . 5
⊢
ℝ* =
(Base‘ℝ*𝑠) |
8 | 6, 7 | ressbas 16790 |
. . . 4
⊢
((0[,]+∞) ∈ V → ((0[,]+∞) ∩
ℝ*) = (Base‘𝐺)) |
9 | 5, 8 | ax-mp 5 |
. . 3
⊢
((0[,]+∞) ∩ ℝ*) = (Base‘𝐺) |
10 | 4, 9 | eqtri 2765 |
. 2
⊢
(0[,]+∞) = (Base‘𝐺) |
11 | | eqid 2737 |
. . . . . 6
⊢
(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) =
(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) |
12 | 11 | xrs1cmn 20403 |
. . . . 5
⊢
(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ∈ CMnd |
13 | | cmnmnd 19186 |
. . . . 5
⊢
((ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ∈ CMnd →
(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ∈ Mnd) |
14 | 12, 13 | ax-mp 5 |
. . . 4
⊢
(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ∈ Mnd |
15 | | xrge0cmn 20405 |
. . . . . 6
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ CMnd |
16 | 6, 15 | eqeltri 2834 |
. . . . 5
⊢ 𝐺 ∈ CMnd |
17 | | cmnmnd 19186 |
. . . . 5
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
18 | 16, 17 | ax-mp 5 |
. . . 4
⊢ 𝐺 ∈ Mnd |
19 | 14, 18 | pm3.2i 474 |
. . 3
⊢
((ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ∈ Mnd ∧ 𝐺 ∈ Mnd) |
20 | | eliccxr 13023 |
. . . . . . 7
⊢ (𝑥 ∈ (0[,]+∞) →
𝑥 ∈
ℝ*) |
21 | | mnfxr 10890 |
. . . . . . . . . 10
⊢ -∞
∈ ℝ* |
22 | 21 | a1i 11 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0[,]+∞) →
-∞ ∈ ℝ*) |
23 | | 0xr 10880 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
24 | 23 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0[,]+∞) → 0
∈ ℝ*) |
25 | | mnflt0 12717 |
. . . . . . . . . . 11
⊢ -∞
< 0 |
26 | 25 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0[,]+∞) →
-∞ < 0) |
27 | | pnfxr 10887 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
28 | 27 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0[,]+∞) →
+∞ ∈ ℝ*) |
29 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0[,]+∞) →
𝑥 ∈
(0[,]+∞)) |
30 | | iccgelb 12991 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
𝑥 ∈ (0[,]+∞))
→ 0 ≤ 𝑥) |
31 | 24, 28, 29, 30 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0[,]+∞) → 0
≤ 𝑥) |
32 | 22, 24, 20, 26, 31 | xrltletrd 12751 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0[,]+∞) →
-∞ < 𝑥) |
33 | 22, 20, 32 | xrgtned 42534 |
. . . . . . . 8
⊢ (𝑥 ∈ (0[,]+∞) →
𝑥 ≠
-∞) |
34 | | nelsn 4581 |
. . . . . . . 8
⊢ (𝑥 ≠ -∞ → ¬
𝑥 ∈
{-∞}) |
35 | 33, 34 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ (0[,]+∞) →
¬ 𝑥 ∈
{-∞}) |
36 | 20, 35 | eldifd 3877 |
. . . . . 6
⊢ (𝑥 ∈ (0[,]+∞) →
𝑥 ∈
(ℝ* ∖ {-∞})) |
37 | 36 | rgen 3071 |
. . . . 5
⊢
∀𝑥 ∈
(0[,]+∞)𝑥 ∈
(ℝ* ∖ {-∞}) |
38 | | dfss3 3888 |
. . . . 5
⊢
((0[,]+∞) ⊆ (ℝ* ∖ {-∞}) ↔
∀𝑥 ∈
(0[,]+∞)𝑥 ∈
(ℝ* ∖ {-∞})) |
39 | 37, 38 | mpbir 234 |
. . . 4
⊢
(0[,]+∞) ⊆ (ℝ* ∖
{-∞}) |
40 | | 0e0iccpnf 13047 |
. . . 4
⊢ 0 ∈
(0[,]+∞) |
41 | 39, 40 | pm3.2i 474 |
. . 3
⊢
((0[,]+∞) ⊆ (ℝ* ∖ {-∞}) ∧ 0
∈ (0[,]+∞)) |
42 | | difss 4046 |
. . . . 5
⊢
(ℝ* ∖ {-∞}) ⊆
ℝ* |
43 | 11, 7 | ressbas2 16791 |
. . . . 5
⊢
((ℝ* ∖ {-∞}) ⊆ ℝ*
→ (ℝ* ∖ {-∞}) =
(Base‘(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})))) |
44 | 42, 43 | ax-mp 5 |
. . . 4
⊢
(ℝ* ∖ {-∞}) =
(Base‘(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞}))) |
45 | 11 | xrs10 20402 |
. . . 4
⊢ 0 =
(0g‘(ℝ*𝑠
↾s (ℝ* ∖ {-∞}))) |
46 | | xrex 12583 |
. . . . . . 7
⊢
ℝ* ∈ V |
47 | | difexg 5220 |
. . . . . . 7
⊢
(ℝ* ∈ V → (ℝ* ∖
{-∞}) ∈ V) |
48 | 46, 47 | ax-mp 5 |
. . . . . 6
⊢
(ℝ* ∖ {-∞}) ∈ V |
49 | 41 | simpli 487 |
. . . . . 6
⊢
(0[,]+∞) ⊆ (ℝ* ∖
{-∞}) |
50 | | ressabs 16800 |
. . . . . 6
⊢
(((ℝ* ∖ {-∞}) ∈ V ∧ (0[,]+∞)
⊆ (ℝ* ∖ {-∞})) →
((ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ↾s (0[,]+∞)) =
(ℝ*𝑠 ↾s
(0[,]+∞))) |
51 | 48, 49, 50 | mp2an 692 |
. . . . 5
⊢
((ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ↾s (0[,]+∞)) =
(ℝ*𝑠 ↾s
(0[,]+∞)) |
52 | 6 | eqcomi 2746 |
. . . . 5
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) = 𝐺 |
53 | 51, 52 | eqtr2i 2766 |
. . . 4
⊢ 𝐺 =
((ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ↾s
(0[,]+∞)) |
54 | 44, 45, 53 | submnd0 18202 |
. . 3
⊢
((((ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ∈ Mnd ∧ 𝐺 ∈ Mnd) ∧ ((0[,]+∞) ⊆
(ℝ* ∖ {-∞}) ∧ 0 ∈ (0[,]+∞))) →
0 = (0g‘𝐺)) |
55 | 19, 41, 54 | mp2an 692 |
. 2
⊢ 0 =
(0g‘𝐺) |
56 | 16 | a1i 11 |
. 2
⊢ (𝜑 → 𝐺 ∈ CMnd) |
57 | | gsumge0cl.2 |
. 2
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
58 | | gsumge0cl.3 |
. 2
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) |
59 | | gsumge0cl.4 |
. 2
⊢ (𝜑 → 𝐹 finSupp 0) |
60 | 10, 55, 56, 57, 58, 59 | gsumcl 19300 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) ∈
(0[,]+∞)) |