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 23624
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 23619 . 2 class 1
2 vf . . 3 setvar 𝑓
3 cr 10230 . . . . . 6 class
4 vg . . . . . . 7 setvar 𝑔
54cv 1636 . . . . . 6 class 𝑔
63, 3, 5wf 6107 . . . . 5 wff 𝑔:ℝ⟶ℝ
75crn 5325 . . . . . 6 class ran 𝑔
8 cfn 8202 . . . . . 6 class Fin
97, 8wcel 2157 . . . . 5 wff ran 𝑔 ∈ Fin
105ccnv 5323 . . . . . . . 8 class 𝑔
11 cc0 10231 . . . . . . . . . 10 class 0
1211csn 4381 . . . . . . . . 9 class {0}
133, 12cdif 3777 . . . . . . . 8 class (ℝ ∖ {0})
1410, 13cima 5327 . . . . . . 7 class (𝑔 “ (ℝ ∖ {0}))
15 cvol 23467 . . . . . . 7 class vol
1614, 15cfv 6111 . . . . . 6 class (vol‘(𝑔 “ (ℝ ∖ {0})))
1716, 3wcel 2157 . . . . 5 wff (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
186, 9, 17w3a 1100 . . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19 cmbf 23618 . . . 4 class MblFn
2018, 4, 19crab 3111 . . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
212cv 1636 . . . . . 6 class 𝑓
2221crn 5325 . . . . 5 class ran 𝑓
2322, 12cdif 3777 . . . 4 class (ran 𝑓 ∖ {0})
24 vx . . . . . 6 setvar 𝑥
2524cv 1636 . . . . 5 class 𝑥
2621ccnv 5323 . . . . . . 7 class 𝑓
2725csn 4381 . . . . . . 7 class {𝑥}
2826, 27cima 5327 . . . . . 6 class (𝑓 “ {𝑥})
2928, 15cfv 6111 . . . . 5 class (vol‘(𝑓 “ {𝑥}))
30 cmul 10236 . . . . 5 class ·
3125, 29, 30co 6884 . . . 4 class (𝑥 · (vol‘(𝑓 “ {𝑥})))
3223, 31, 24csu 14659 . . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥})))
332, 20, 32cmpt 4934 . 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥}))))
341, 33wceq 1637 1 wff 1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥}))))
Colors of variables: wff setvar class
This definition is referenced by:  isi1f  23678  itg1val  23687
  Copyright terms: Public domain W3C validator