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 24228
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 24223 . 2 class 1
2 vf . . 3 setvar 𝑓
3 cr 10529 . . . . . 6 class
4 vg . . . . . . 7 setvar 𝑔
54cv 1537 . . . . . 6 class 𝑔
63, 3, 5wf 6324 . . . . 5 wff 𝑔:ℝ⟶ℝ
75crn 5524 . . . . . 6 class ran 𝑔
8 cfn 8496 . . . . . 6 class Fin
97, 8wcel 2112 . . . . 5 wff ran 𝑔 ∈ Fin
105ccnv 5522 . . . . . . . 8 class 𝑔
11 cc0 10530 . . . . . . . . . 10 class 0
1211csn 4528 . . . . . . . . 9 class {0}
133, 12cdif 3881 . . . . . . . 8 class (ℝ ∖ {0})
1410, 13cima 5526 . . . . . . 7 class (𝑔 “ (ℝ ∖ {0}))
15 cvol 24071 . . . . . . 7 class vol
1614, 15cfv 6328 . . . . . 6 class (vol‘(𝑔 “ (ℝ ∖ {0})))
1716, 3wcel 2112 . . . . 5 wff (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
186, 9, 17w3a 1084 . . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19 cmbf 24222 . . . 4 class MblFn
2018, 4, 19crab 3113 . . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
212cv 1537 . . . . . 6 class 𝑓
2221crn 5524 . . . . 5 class ran 𝑓
2322, 12cdif 3881 . . . 4 class (ran 𝑓 ∖ {0})
24 vx . . . . . 6 setvar 𝑥
2524cv 1537 . . . . 5 class 𝑥
2621ccnv 5522 . . . . . . 7 class 𝑓
2725csn 4528 . . . . . . 7 class {𝑥}
2826, 27cima 5526 . . . . . 6 class (𝑓 “ {𝑥})
2928, 15cfv 6328 . . . . 5 class (vol‘(𝑓 “ {𝑥}))
30 cmul 10535 . . . . 5 class ·
3125, 29, 30co 7139 . . . 4 class (𝑥 · (vol‘(𝑓 “ {𝑥})))
3223, 31, 24csu 15038 . . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥})))
332, 20, 32cmpt 5113 . 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥}))))
341, 33wceq 1538 1 wff 1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥}))))
Colors of variables: wff setvar class
This definition is referenced by:  isi1f  24282  itg1val  24291
  Copyright terms: Public domain W3C validator