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 23434
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 23429 . 2 class 1
2 vf . . 3 setvar 𝑓
3 cr 9973 . . . . . 6 class
4 vg . . . . . . 7 setvar 𝑔
54cv 1522 . . . . . 6 class 𝑔
63, 3, 5wf 5922 . . . . 5 wff 𝑔:ℝ⟶ℝ
75crn 5144 . . . . . 6 class ran 𝑔
8 cfn 7997 . . . . . 6 class Fin
97, 8wcel 2030 . . . . 5 wff ran 𝑔 ∈ Fin
105ccnv 5142 . . . . . . . 8 class 𝑔
11 cc0 9974 . . . . . . . . . 10 class 0
1211csn 4210 . . . . . . . . 9 class {0}
133, 12cdif 3604 . . . . . . . 8 class (ℝ ∖ {0})
1410, 13cima 5146 . . . . . . 7 class (𝑔 “ (ℝ ∖ {0}))
15 cvol 23278 . . . . . . 7 class vol
1614, 15cfv 5926 . . . . . 6 class (vol‘(𝑔 “ (ℝ ∖ {0})))
1716, 3wcel 2030 . . . . 5 wff (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
186, 9, 17w3a 1054 . . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19 cmbf 23428 . . . 4 class MblFn
2018, 4, 19crab 2945 . . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
212cv 1522 . . . . . 6 class 𝑓
2221crn 5144 . . . . 5 class ran 𝑓
2322, 12cdif 3604 . . . 4 class (ran 𝑓 ∖ {0})
24 vx . . . . . 6 setvar 𝑥
2524cv 1522 . . . . 5 class 𝑥
2621ccnv 5142 . . . . . . 7 class 𝑓
2725csn 4210 . . . . . . 7 class {𝑥}
2826, 27cima 5146 . . . . . 6 class (𝑓 “ {𝑥})
2928, 15cfv 5926 . . . . 5 class (vol‘(𝑓 “ {𝑥}))
30 cmul 9979 . . . . 5 class ·
3125, 29, 30co 6690 . . . 4 class (𝑥 · (vol‘(𝑓 “ {𝑥})))
3223, 31, 24csu 14460 . . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥})))
332, 20, 32cmpt 4762 . 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥}))))
341, 33wceq 1523 1 wff 1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥}))))
Colors of variables: wff setvar class
This definition is referenced by:  isi1f  23486  itg1val  23495
  Copyright terms: Public domain W3C validator