MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-itg1 Structured version   Visualization version   GIF version

Definition df-itg1 23609
Description: Define the Lebesgue integral for simple functions. A simple function is a finite linear combination of indicator functions for finitely measurable sets, whose assigned value is the sum of the measures of the sets times their respective weights. (Contributed by Mario Carneiro, 18-Jun-2014.)
Assertion
Ref Expression
df-itg1 1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥}))))
Distinct variable group:   𝑓,𝑔,𝑥

Detailed syntax breakdown of Definition df-itg1
StepHypRef Expression
1 citg1 23604 . 2 class 1
2 vf . . 3 setvar 𝑓
3 cr 10138 . . . . . 6 class
4 vg . . . . . . 7 setvar 𝑔
54cv 1630 . . . . . 6 class 𝑔
63, 3, 5wf 6028 . . . . 5 wff 𝑔:ℝ⟶ℝ
75crn 5251 . . . . . 6 class ran 𝑔
8 cfn 8110 . . . . . 6 class Fin
97, 8wcel 2145 . . . . 5 wff ran 𝑔 ∈ Fin
105ccnv 5249 . . . . . . . 8 class 𝑔
11 cc0 10139 . . . . . . . . . 10 class 0
1211csn 4317 . . . . . . . . 9 class {0}
133, 12cdif 3721 . . . . . . . 8 class (ℝ ∖ {0})
1410, 13cima 5253 . . . . . . 7 class (𝑔 “ (ℝ ∖ {0}))
15 cvol 23452 . . . . . . 7 class vol
1614, 15cfv 6032 . . . . . 6 class (vol‘(𝑔 “ (ℝ ∖ {0})))
1716, 3wcel 2145 . . . . 5 wff (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
186, 9, 17w3a 1071 . . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19 cmbf 23603 . . . 4 class MblFn
2018, 4, 19crab 3065 . . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
212cv 1630 . . . . . 6 class 𝑓
2221crn 5251 . . . . 5 class ran 𝑓
2322, 12cdif 3721 . . . 4 class (ran 𝑓 ∖ {0})
24 vx . . . . . 6 setvar 𝑥
2524cv 1630 . . . . 5 class 𝑥
2621ccnv 5249 . . . . . . 7 class 𝑓
2725csn 4317 . . . . . . 7 class {𝑥}
2826, 27cima 5253 . . . . . 6 class (𝑓 “ {𝑥})
2928, 15cfv 6032 . . . . 5 class (vol‘(𝑓 “ {𝑥}))
30 cmul 10144 . . . . 5 class ·
3125, 29, 30co 6794 . . . 4 class (𝑥 · (vol‘(𝑓 “ {𝑥})))
3223, 31, 24csu 14625 . . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥})))
332, 20, 32cmpt 4864 . 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥}))))
341, 33wceq 1631 1 wff 1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥}))))
Colors of variables: wff setvar class
This definition is referenced by:  isi1f  23662  itg1val  23671
  Copyright terms: Public domain W3C validator