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 24148
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 24143 . 2 class 1
2 vf . . 3 setvar 𝑓
3 cr 10524 . . . . . 6 class
4 vg . . . . . . 7 setvar 𝑔
54cv 1527 . . . . . 6 class 𝑔
63, 3, 5wf 6344 . . . . 5 wff 𝑔:ℝ⟶ℝ
75crn 5549 . . . . . 6 class ran 𝑔
8 cfn 8497 . . . . . 6 class Fin
97, 8wcel 2105 . . . . 5 wff ran 𝑔 ∈ Fin
105ccnv 5547 . . . . . . . 8 class 𝑔
11 cc0 10525 . . . . . . . . . 10 class 0
1211csn 4557 . . . . . . . . 9 class {0}
133, 12cdif 3930 . . . . . . . 8 class (ℝ ∖ {0})
1410, 13cima 5551 . . . . . . 7 class (𝑔 “ (ℝ ∖ {0}))
15 cvol 23991 . . . . . . 7 class vol
1614, 15cfv 6348 . . . . . 6 class (vol‘(𝑔 “ (ℝ ∖ {0})))
1716, 3wcel 2105 . . . . 5 wff (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
186, 9, 17w3a 1079 . . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19 cmbf 24142 . . . 4 class MblFn
2018, 4, 19crab 3139 . . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
212cv 1527 . . . . . 6 class 𝑓
2221crn 5549 . . . . 5 class ran 𝑓
2322, 12cdif 3930 . . . 4 class (ran 𝑓 ∖ {0})
24 vx . . . . . 6 setvar 𝑥
2524cv 1527 . . . . 5 class 𝑥
2621ccnv 5547 . . . . . . 7 class 𝑓
2725csn 4557 . . . . . . 7 class {𝑥}
2826, 27cima 5551 . . . . . 6 class (𝑓 “ {𝑥})
2928, 15cfv 6348 . . . . 5 class (vol‘(𝑓 “ {𝑥}))
30 cmul 10530 . . . . 5 class ·
3125, 29, 30co 7145 . . . 4 class (𝑥 · (vol‘(𝑓 “ {𝑥})))
3223, 31, 24csu 15030 . . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥})))
332, 20, 32cmpt 5137 . 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥}))))
341, 33wceq 1528 1 wff 1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥}))))
Colors of variables: wff setvar class
This definition is referenced by:  isi1f  24202  itg1val  24211
  Copyright terms: Public domain W3C validator