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 25655
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 25650 . 2 class 1
2 vf . . 3 setvar 𝑓
3 cr 11154 . . . . . 6 class
4 vg . . . . . . 7 setvar 𝑔
54cv 1539 . . . . . 6 class 𝑔
63, 3, 5wf 6557 . . . . 5 wff 𝑔:ℝ⟶ℝ
75crn 5686 . . . . . 6 class ran 𝑔
8 cfn 8985 . . . . . 6 class Fin
97, 8wcel 2108 . . . . 5 wff ran 𝑔 ∈ Fin
105ccnv 5684 . . . . . . . 8 class 𝑔
11 cc0 11155 . . . . . . . . . 10 class 0
1211csn 4626 . . . . . . . . 9 class {0}
133, 12cdif 3948 . . . . . . . 8 class (ℝ ∖ {0})
1410, 13cima 5688 . . . . . . 7 class (𝑔 “ (ℝ ∖ {0}))
15 cvol 25498 . . . . . . 7 class vol
1614, 15cfv 6561 . . . . . 6 class (vol‘(𝑔 “ (ℝ ∖ {0})))
1716, 3wcel 2108 . . . . 5 wff (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
186, 9, 17w3a 1087 . . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19 cmbf 25649 . . . 4 class MblFn
2018, 4, 19crab 3436 . . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
212cv 1539 . . . . . 6 class 𝑓
2221crn 5686 . . . . 5 class ran 𝑓
2322, 12cdif 3948 . . . 4 class (ran 𝑓 ∖ {0})
24 vx . . . . . 6 setvar 𝑥
2524cv 1539 . . . . 5 class 𝑥
2621ccnv 5684 . . . . . . 7 class 𝑓
2725csn 4626 . . . . . . 7 class {𝑥}
2826, 27cima 5688 . . . . . 6 class (𝑓 “ {𝑥})
2928, 15cfv 6561 . . . . 5 class (vol‘(𝑓 “ {𝑥}))
30 cmul 11160 . . . . 5 class ·
3125, 29, 30co 7431 . . . 4 class (𝑥 · (vol‘(𝑓 “ {𝑥})))
3223, 31, 24csu 15722 . . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥})))
332, 20, 32cmpt 5225 . 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥}))))
341, 33wceq 1540 1 wff 1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥}))))
Colors of variables: wff setvar class
This definition is referenced by:  isi1f  25709  itg1val  25718
  Copyright terms: Public domain W3C validator