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 23312
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 23307 . 2 class 1
2 vf . . 3 setvar 𝑓
3 cr 9887 . . . . . 6 class
4 vg . . . . . . 7 setvar 𝑔
54cv 1479 . . . . . 6 class 𝑔
63, 3, 5wf 5848 . . . . 5 wff 𝑔:ℝ⟶ℝ
75crn 5080 . . . . . 6 class ran 𝑔
8 cfn 7907 . . . . . 6 class Fin
97, 8wcel 1987 . . . . 5 wff ran 𝑔 ∈ Fin
105ccnv 5078 . . . . . . . 8 class 𝑔
11 cc0 9888 . . . . . . . . . 10 class 0
1211csn 4153 . . . . . . . . 9 class {0}
133, 12cdif 3556 . . . . . . . 8 class (ℝ ∖ {0})
1410, 13cima 5082 . . . . . . 7 class (𝑔 “ (ℝ ∖ {0}))
15 cvol 23155 . . . . . . 7 class vol
1614, 15cfv 5852 . . . . . 6 class (vol‘(𝑔 “ (ℝ ∖ {0})))
1716, 3wcel 1987 . . . . 5 wff (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
186, 9, 17w3a 1036 . . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19 cmbf 23306 . . . 4 class MblFn
2018, 4, 19crab 2911 . . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
212cv 1479 . . . . . 6 class 𝑓
2221crn 5080 . . . . 5 class ran 𝑓
2322, 12cdif 3556 . . . 4 class (ran 𝑓 ∖ {0})
24 vx . . . . . 6 setvar 𝑥
2524cv 1479 . . . . 5 class 𝑥
2621ccnv 5078 . . . . . . 7 class 𝑓
2725csn 4153 . . . . . . 7 class {𝑥}
2826, 27cima 5082 . . . . . 6 class (𝑓 “ {𝑥})
2928, 15cfv 5852 . . . . 5 class (vol‘(𝑓 “ {𝑥}))
30 cmul 9893 . . . . 5 class ·
3125, 29, 30co 6610 . . . 4 class (𝑥 · (vol‘(𝑓 “ {𝑥})))
3223, 31, 24csu 14358 . . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥})))
332, 20, 32cmpt 4678 . 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥}))))
341, 33wceq 1480 1 wff 1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥}))))
Colors of variables: wff setvar class
This definition is referenced by:  isi1f  23364  itg1val  23373
  Copyright terms: Public domain W3C validator