Step | Hyp | Ref
| Expression |
1 | | iccssxr 13162 |
. . . . . . 7
⊢
(0[,]+∞) ⊆ ℝ* |
2 | | xrge0gsumle.g |
. . . . . . . . . 10
⊢ 𝐺 =
(ℝ*𝑠 ↾s
(0[,]+∞)) |
3 | | xrsbas 20614 |
. . . . . . . . . 10
⊢
ℝ* =
(Base‘ℝ*𝑠) |
4 | 2, 3 | ressbas2 16949 |
. . . . . . . . 9
⊢
((0[,]+∞) ⊆ ℝ* → (0[,]+∞) =
(Base‘𝐺)) |
5 | 1, 4 | ax-mp 5 |
. . . . . . . 8
⊢
(0[,]+∞) = (Base‘𝐺) |
6 | | eqid 2738 |
. . . . . . . . . 10
⊢
(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) =
(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) |
7 | 6 | xrge0subm 20639 |
. . . . . . . . 9
⊢
(0[,]+∞) ∈
(SubMnd‘(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞}))) |
8 | | xrex 12727 |
. . . . . . . . . . . . 13
⊢
ℝ* ∈ V |
9 | 8 | difexi 5252 |
. . . . . . . . . . . 12
⊢
(ℝ* ∖ {-∞}) ∈ V |
10 | | simpl 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ 0 ≤ 𝑥) →
𝑥 ∈
ℝ*) |
11 | | ge0nemnf 12907 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ 0 ≤ 𝑥) →
𝑥 ≠
-∞) |
12 | 10, 11 | jca 512 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ*
∧ 0 ≤ 𝑥) →
(𝑥 ∈
ℝ* ∧ 𝑥
≠ -∞)) |
13 | | elxrge0 13189 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (0[,]+∞) ↔
(𝑥 ∈
ℝ* ∧ 0 ≤ 𝑥)) |
14 | | eldifsn 4720 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (ℝ*
∖ {-∞}) ↔ (𝑥 ∈ ℝ* ∧ 𝑥 ≠
-∞)) |
15 | 12, 13, 14 | 3imtr4i 292 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (0[,]+∞) →
𝑥 ∈
(ℝ* ∖ {-∞})) |
16 | 15 | ssriv 3925 |
. . . . . . . . . . . 12
⊢
(0[,]+∞) ⊆ (ℝ* ∖
{-∞}) |
17 | | ressabs 16959 |
. . . . . . . . . . . 12
⊢
(((ℝ* ∖ {-∞}) ∈ V ∧ (0[,]+∞)
⊆ (ℝ* ∖ {-∞})) →
((ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ↾s (0[,]+∞)) =
(ℝ*𝑠 ↾s
(0[,]+∞))) |
18 | 9, 16, 17 | mp2an 689 |
. . . . . . . . . . 11
⊢
((ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ↾s (0[,]+∞)) =
(ℝ*𝑠 ↾s
(0[,]+∞)) |
19 | 2, 18 | eqtr4i 2769 |
. . . . . . . . . 10
⊢ 𝐺 =
((ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ↾s
(0[,]+∞)) |
20 | 6 | xrs10 20637 |
. . . . . . . . . 10
⊢ 0 =
(0g‘(ℝ*𝑠
↾s (ℝ* ∖ {-∞}))) |
21 | 19, 20 | subm0 18454 |
. . . . . . . . 9
⊢
((0[,]+∞) ∈
(SubMnd‘(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞}))) → 0 =
(0g‘𝐺)) |
22 | 7, 21 | ax-mp 5 |
. . . . . . . 8
⊢ 0 =
(0g‘𝐺) |
23 | | xrge0cmn 20640 |
. . . . . . . . . 10
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ CMnd |
24 | 2, 23 | eqeltri 2835 |
. . . . . . . . 9
⊢ 𝐺 ∈ CMnd |
25 | 24 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐺 ∈ CMnd) |
26 | | elfpw 9121 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑠 ⊆ 𝐴 ∧ 𝑠 ∈ Fin)) |
27 | 26 | simprbi 497 |
. . . . . . . . 9
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) → 𝑠 ∈ Fin) |
28 | 27 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑠 ∈ Fin) |
29 | | xrge0gsumle.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞)) |
30 | 26 | simplbi 498 |
. . . . . . . . 9
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) → 𝑠 ⊆ 𝐴) |
31 | | fssres 6640 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶(0[,]+∞) ∧ 𝑠 ⊆ 𝐴) → (𝐹 ↾ 𝑠):𝑠⟶(0[,]+∞)) |
32 | 29, 30, 31 | syl2an 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑠):𝑠⟶(0[,]+∞)) |
33 | | c0ex 10969 |
. . . . . . . . . 10
⊢ 0 ∈
V |
34 | 33 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 0 ∈
V) |
35 | 32, 28, 34 | fdmfifsupp 9138 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑠) finSupp 0) |
36 | 5, 22, 25, 28, 32, 35 | gsumcl 19516 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑠)) ∈ (0[,]+∞)) |
37 | 1, 36 | sselid 3919 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑠)) ∈
ℝ*) |
38 | 37 | fmpttd 6989 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))):(𝒫 𝐴 ∩
Fin)⟶ℝ*) |
39 | 38 | frnd 6608 |
. . . 4
⊢ (𝜑 → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) ⊆
ℝ*) |
40 | | 0ss 4330 |
. . . . . . 7
⊢ ∅
⊆ 𝐴 |
41 | | 0fin 8954 |
. . . . . . 7
⊢ ∅
∈ Fin |
42 | | elfpw 9121 |
. . . . . . 7
⊢ (∅
∈ (𝒫 𝐴 ∩
Fin) ↔ (∅ ⊆ 𝐴 ∧ ∅ ∈ Fin)) |
43 | 40, 41, 42 | mpbir2an 708 |
. . . . . 6
⊢ ∅
∈ (𝒫 𝐴 ∩
Fin) |
44 | | 0cn 10967 |
. . . . . 6
⊢ 0 ∈
ℂ |
45 | | eqid 2738 |
. . . . . . 7
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) = (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) |
46 | | reseq2 5886 |
. . . . . . . . . 10
⊢ (𝑠 = ∅ → (𝐹 ↾ 𝑠) = (𝐹 ↾ ∅)) |
47 | | res0 5895 |
. . . . . . . . . 10
⊢ (𝐹 ↾ ∅) =
∅ |
48 | 46, 47 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (𝑠 = ∅ → (𝐹 ↾ 𝑠) = ∅) |
49 | 48 | oveq2d 7291 |
. . . . . . . 8
⊢ (𝑠 = ∅ → (𝐺 Σg
(𝐹 ↾ 𝑠)) = (𝐺 Σg
∅)) |
50 | 22 | gsum0 18368 |
. . . . . . . 8
⊢ (𝐺 Σg
∅) = 0 |
51 | 49, 50 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝑠 = ∅ → (𝐺 Σg
(𝐹 ↾ 𝑠)) = 0) |
52 | 45, 51 | elrnmpt1s 5866 |
. . . . . 6
⊢ ((∅
∈ (𝒫 𝐴 ∩
Fin) ∧ 0 ∈ ℂ) → 0 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))) |
53 | 43, 44, 52 | mp2an 689 |
. . . . 5
⊢ 0 ∈
ran (𝑠 ∈ (𝒫
𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) |
54 | 53 | a1i 11 |
. . . 4
⊢ (𝜑 → 0 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠)))) |
55 | 39, 54 | sseldd 3922 |
. . 3
⊢ (𝜑 → 0 ∈
ℝ*) |
56 | 24 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ CMnd) |
57 | | xrge0gsumle.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ (𝒫 𝐴 ∩ Fin)) |
58 | 57 | elin2d 4133 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ Fin) |
59 | | diffi 8962 |
. . . . . 6
⊢ (𝐵 ∈ Fin → (𝐵 ∖ 𝐶) ∈ Fin) |
60 | 58, 59 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐵 ∖ 𝐶) ∈ Fin) |
61 | | elfpw 9121 |
. . . . . . . . 9
⊢ (𝐵 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝐵 ⊆ 𝐴 ∧ 𝐵 ∈ Fin)) |
62 | 61 | simplbi 498 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝒫 𝐴 ∩ Fin) → 𝐵 ⊆ 𝐴) |
63 | 57, 62 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
64 | 63 | ssdifssd 4077 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∖ 𝐶) ⊆ 𝐴) |
65 | 29, 64 | fssresd 6641 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ (𝐵 ∖ 𝐶)):(𝐵 ∖ 𝐶)⟶(0[,]+∞)) |
66 | 33 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ∈
V) |
67 | 65, 60, 66 | fdmfifsupp 9138 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ (𝐵 ∖ 𝐶)) finSupp 0) |
68 | 5, 22, 56, 60, 65, 67 | gsumcl 19516 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐵 ∖ 𝐶))) ∈ (0[,]+∞)) |
69 | 1, 68 | sselid 3919 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐵 ∖ 𝐶))) ∈
ℝ*) |
70 | | xrge0gsumle.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ⊆ 𝐵) |
71 | 58, 70 | ssfid 9042 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ Fin) |
72 | 70, 63 | sstrd 3931 |
. . . . . 6
⊢ (𝜑 → 𝐶 ⊆ 𝐴) |
73 | 29, 72 | fssresd 6641 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶(0[,]+∞)) |
74 | 73, 71, 66 | fdmfifsupp 9138 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ 𝐶) finSupp 0) |
75 | 5, 22, 56, 71, 73, 74 | gsumcl 19516 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝐶)) ∈ (0[,]+∞)) |
76 | 1, 75 | sselid 3919 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝐶)) ∈
ℝ*) |
77 | | elxrge0 13189 |
. . . . 5
⊢ ((𝐺 Σg
(𝐹 ↾ (𝐵 ∖ 𝐶))) ∈ (0[,]+∞) ↔ ((𝐺 Σg
(𝐹 ↾ (𝐵 ∖ 𝐶))) ∈ ℝ* ∧ 0 ≤
(𝐺
Σg (𝐹 ↾ (𝐵 ∖ 𝐶))))) |
78 | 77 | simprbi 497 |
. . . 4
⊢ ((𝐺 Σg
(𝐹 ↾ (𝐵 ∖ 𝐶))) ∈ (0[,]+∞) → 0 ≤
(𝐺
Σg (𝐹 ↾ (𝐵 ∖ 𝐶)))) |
79 | 68, 78 | syl 17 |
. . 3
⊢ (𝜑 → 0 ≤ (𝐺 Σg (𝐹 ↾ (𝐵 ∖ 𝐶)))) |
80 | | xleadd2a 12988 |
. . 3
⊢ (((0
∈ ℝ* ∧ (𝐺 Σg (𝐹 ↾ (𝐵 ∖ 𝐶))) ∈ ℝ* ∧ (𝐺 Σg
(𝐹 ↾ 𝐶)) ∈ ℝ*)
∧ 0 ≤ (𝐺
Σg (𝐹 ↾ (𝐵 ∖ 𝐶)))) → ((𝐺 Σg (𝐹 ↾ 𝐶)) +𝑒 0) ≤ ((𝐺 Σg
(𝐹 ↾ 𝐶)) +𝑒 (𝐺 Σg
(𝐹 ↾ (𝐵 ∖ 𝐶))))) |
81 | 55, 69, 76, 79, 80 | syl31anc 1372 |
. 2
⊢ (𝜑 → ((𝐺 Σg (𝐹 ↾ 𝐶)) +𝑒 0) ≤ ((𝐺 Σg
(𝐹 ↾ 𝐶)) +𝑒 (𝐺 Σg
(𝐹 ↾ (𝐵 ∖ 𝐶))))) |
82 | 76 | xaddid1d 12977 |
. 2
⊢ (𝜑 → ((𝐺 Σg (𝐹 ↾ 𝐶)) +𝑒 0) = (𝐺 Σg
(𝐹 ↾ 𝐶))) |
83 | | ovex 7308 |
. . . . 5
⊢
(0[,]+∞) ∈ V |
84 | | xrsadd 20615 |
. . . . . 6
⊢
+𝑒 =
(+g‘ℝ*𝑠) |
85 | 2, 84 | ressplusg 17000 |
. . . . 5
⊢
((0[,]+∞) ∈ V → +𝑒 =
(+g‘𝐺)) |
86 | 83, 85 | ax-mp 5 |
. . . 4
⊢
+𝑒 = (+g‘𝐺) |
87 | 29, 63 | fssresd 6641 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶(0[,]+∞)) |
88 | 87, 58, 66 | fdmfifsupp 9138 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ 𝐵) finSupp 0) |
89 | | disjdif 4405 |
. . . . 5
⊢ (𝐶 ∩ (𝐵 ∖ 𝐶)) = ∅ |
90 | 89 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝐶 ∩ (𝐵 ∖ 𝐶)) = ∅) |
91 | | undif2 4410 |
. . . . 5
⊢ (𝐶 ∪ (𝐵 ∖ 𝐶)) = (𝐶 ∪ 𝐵) |
92 | | ssequn1 4114 |
. . . . . 6
⊢ (𝐶 ⊆ 𝐵 ↔ (𝐶 ∪ 𝐵) = 𝐵) |
93 | 70, 92 | sylib 217 |
. . . . 5
⊢ (𝜑 → (𝐶 ∪ 𝐵) = 𝐵) |
94 | 91, 93 | eqtr2id 2791 |
. . . 4
⊢ (𝜑 → 𝐵 = (𝐶 ∪ (𝐵 ∖ 𝐶))) |
95 | 5, 22, 86, 56, 57, 87, 88, 90, 94 | gsumsplit 19529 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝐵)) = ((𝐺 Σg ((𝐹 ↾ 𝐵) ↾ 𝐶)) +𝑒 (𝐺 Σg ((𝐹 ↾ 𝐵) ↾ (𝐵 ∖ 𝐶))))) |
96 | 70 | resabs1d 5922 |
. . . . 5
⊢ (𝜑 → ((𝐹 ↾ 𝐵) ↾ 𝐶) = (𝐹 ↾ 𝐶)) |
97 | 96 | oveq2d 7291 |
. . . 4
⊢ (𝜑 → (𝐺 Σg ((𝐹 ↾ 𝐵) ↾ 𝐶)) = (𝐺 Σg (𝐹 ↾ 𝐶))) |
98 | | difss 4066 |
. . . . . 6
⊢ (𝐵 ∖ 𝐶) ⊆ 𝐵 |
99 | | resabs1 5921 |
. . . . . 6
⊢ ((𝐵 ∖ 𝐶) ⊆ 𝐵 → ((𝐹 ↾ 𝐵) ↾ (𝐵 ∖ 𝐶)) = (𝐹 ↾ (𝐵 ∖ 𝐶))) |
100 | 98, 99 | mp1i 13 |
. . . . 5
⊢ (𝜑 → ((𝐹 ↾ 𝐵) ↾ (𝐵 ∖ 𝐶)) = (𝐹 ↾ (𝐵 ∖ 𝐶))) |
101 | 100 | oveq2d 7291 |
. . . 4
⊢ (𝜑 → (𝐺 Σg ((𝐹 ↾ 𝐵) ↾ (𝐵 ∖ 𝐶))) = (𝐺 Σg (𝐹 ↾ (𝐵 ∖ 𝐶)))) |
102 | 97, 101 | oveq12d 7293 |
. . 3
⊢ (𝜑 → ((𝐺 Σg ((𝐹 ↾ 𝐵) ↾ 𝐶)) +𝑒 (𝐺 Σg ((𝐹 ↾ 𝐵) ↾ (𝐵 ∖ 𝐶)))) = ((𝐺 Σg (𝐹 ↾ 𝐶)) +𝑒 (𝐺 Σg (𝐹 ↾ (𝐵 ∖ 𝐶))))) |
103 | 95, 102 | eqtr2d 2779 |
. 2
⊢ (𝜑 → ((𝐺 Σg (𝐹 ↾ 𝐶)) +𝑒 (𝐺 Σg (𝐹 ↾ (𝐵 ∖ 𝐶)))) = (𝐺 Σg (𝐹 ↾ 𝐵))) |
104 | 81, 82, 103 | 3brtr3d 5105 |
1
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝐶)) ≤ (𝐺 Σg (𝐹 ↾ 𝐵))) |