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 23904
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 23899 . 2 class 1
2 vf . . 3 setvar 𝑓
3 cr 10382 . . . . . 6 class
4 vg . . . . . . 7 setvar 𝑔
54cv 1521 . . . . . 6 class 𝑔
63, 3, 5wf 6221 . . . . 5 wff 𝑔:ℝ⟶ℝ
75crn 5444 . . . . . 6 class ran 𝑔
8 cfn 8357 . . . . . 6 class Fin
97, 8wcel 2081 . . . . 5 wff ran 𝑔 ∈ Fin
105ccnv 5442 . . . . . . . 8 class 𝑔
11 cc0 10383 . . . . . . . . . 10 class 0
1211csn 4472 . . . . . . . . 9 class {0}
133, 12cdif 3856 . . . . . . . 8 class (ℝ ∖ {0})
1410, 13cima 5446 . . . . . . 7 class (𝑔 “ (ℝ ∖ {0}))
15 cvol 23747 . . . . . . 7 class vol
1614, 15cfv 6225 . . . . . 6 class (vol‘(𝑔 “ (ℝ ∖ {0})))
1716, 3wcel 2081 . . . . 5 wff (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
186, 9, 17w3a 1080 . . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19 cmbf 23898 . . . 4 class MblFn
2018, 4, 19crab 3109 . . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
212cv 1521 . . . . . 6 class 𝑓
2221crn 5444 . . . . 5 class ran 𝑓
2322, 12cdif 3856 . . . 4 class (ran 𝑓 ∖ {0})
24 vx . . . . . 6 setvar 𝑥
2524cv 1521 . . . . 5 class 𝑥
2621ccnv 5442 . . . . . . 7 class 𝑓
2725csn 4472 . . . . . . 7 class {𝑥}
2826, 27cima 5446 . . . . . 6 class (𝑓 “ {𝑥})
2928, 15cfv 6225 . . . . 5 class (vol‘(𝑓 “ {𝑥}))
30 cmul 10388 . . . . 5 class ·
3125, 29, 30co 7016 . . . 4 class (𝑥 · (vol‘(𝑓 “ {𝑥})))
3223, 31, 24csu 14876 . . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥})))
332, 20, 32cmpt 5041 . 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥}))))
341, 33wceq 1522 1 wff 1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(𝑓 “ {𝑥}))))
Colors of variables: wff setvar class
This definition is referenced by:  isi1f  23958  itg1val  23967
  Copyright terms: Public domain W3C validator