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 25593
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 25588 . 2 class 1
2 vf . . 3 setvar 𝑓
3 cr 11139 . . . . . 6 class
4 vg . . . . . . 7 setvar 𝑔
54cv 1532 . . . . . 6 class 𝑔
63, 3, 5wf 6545 . . . . 5 wff 𝑔:ℝ⟶ℝ
75crn 5679 . . . . . 6 class ran 𝑔
8 cfn 8964 . . . . . 6 class Fin
97, 8wcel 2098 . . . . 5 wff ran 𝑔 ∈ Fin
105ccnv 5677 . . . . . . . 8 class 𝑔
11 cc0 11140 . . . . . . . . . 10 class 0
1211csn 4630 . . . . . . . . 9 class {0}
133, 12cdif 3941 . . . . . . . 8 class (ℝ ∖ {0})
1410, 13cima 5681 . . . . . . 7 class (𝑔 “ (ℝ ∖ {0}))
15 cvol 25436 . . . . . . 7 class vol
1614, 15cfv 6549 . . . . . 6 class (vol‘(𝑔 “ (ℝ ∖ {0})))
1716, 3wcel 2098 . . . . 5 wff (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
186, 9, 17w3a 1084 . . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19 cmbf 25587 . . . 4 class MblFn
2018, 4, 19crab 3418 . . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
212cv 1532 . . . . . 6 class 𝑓
2221crn 5679 . . . . 5 class ran 𝑓
2322, 12cdif 3941 . . . 4 class (ran 𝑓 ∖ {0})
24 vx . . . . . 6 setvar 𝑥
2524cv 1532 . . . . 5 class 𝑥
2621ccnv 5677 . . . . . . 7 class 𝑓
2725csn 4630 . . . . . . 7 class {𝑥}
2826, 27cima 5681 . . . . . 6 class (𝑓 “ {𝑥})
2928, 15cfv 6549 . . . . 5 class (vol‘(𝑓 “ {𝑥}))
30 cmul 11145 . . . . 5 class ·
3125, 29, 30co 7419 . . . 4 class (𝑥 · (vol‘(𝑓 “ {𝑥})))
3223, 31, 24csu 15668 . . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥})))
332, 20, 32cmpt 5232 . 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥}))))
341, 33wceq 1533 1 wff 1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥}))))
Colors of variables: wff setvar class
This definition is referenced by:  isi1f  25647  itg1val  25656
  Copyright terms: Public domain W3C validator