Metamath Proof Explorer

Definition df-itg1

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)

Ref Expression
Assertion df-itg1 ⊢ ∫ 1 = f ∈ g ∈ MblFn | g : ℝ ⟶ ℝ ∧ ran ⁡ g ∈ Fin ∧ vol ⁡ g -1 ℝ ∖ 0 ∈ ℝ ⟼ ∑ x ∈ ran ⁡ f ∖ 0 x ⁢ vol ⁡ f -1 x

Detailed syntax breakdown

Step Hyp Ref Expression
0 citg1 class ∫ 1
1 vf setvar f
2 vg setvar g
3 cmbf class MblFn
4 2 cv setvar g
5 cr class ℝ
6 5 5 4 wf wff g : ℝ ⟶ ℝ
7 4 crn class ran ⁡ g
8 cfn class Fin
9 7 8 wcel wff ran ⁡ g ∈ Fin
10 cvol class vol
11 4 ccnv class g -1
12 cc0 class 0
13 12 csn class 0
14 5 13 cdif class ℝ ∖ 0
15 11 14 cima class g -1 ℝ ∖ 0
16 15 10 cfv class vol ⁡ g -1 ℝ ∖ 0
17 16 5 wcel wff vol ⁡ g -1 ℝ ∖ 0 ∈ ℝ
18 6 9 17 w3a wff g : ℝ ⟶ ℝ ∧ ran ⁡ g ∈ Fin ∧ vol ⁡ g -1 ℝ ∖ 0 ∈ ℝ
19 18 2 3 crab class g ∈ MblFn | g : ℝ ⟶ ℝ ∧ ran ⁡ g ∈ Fin ∧ vol ⁡ g -1 ℝ ∖ 0 ∈ ℝ
20 vx setvar x
21 1 cv setvar f
22 21 crn class ran ⁡ f
23 22 13 cdif class ran ⁡ f ∖ 0
24 20 cv setvar x
25 cmul class ×
26 21 ccnv class f -1
27 24 csn class x
28 26 27 cima class f -1 x
29 28 10 cfv class vol ⁡ f -1 x
30 24 29 25 co class x ⁢ vol ⁡ f -1 x
31 23 30 20 csu class ∑ x ∈ ran ⁡ f ∖ 0 x ⁢ vol ⁡ f -1 x
32 1 19 31 cmpt class f ∈ g ∈ MblFn | g : ℝ ⟶ ℝ ∧ ran ⁡ g ∈ Fin ∧ vol ⁡ g -1 ℝ ∖ 0 ∈ ℝ ⟼ ∑ x ∈ ran ⁡ f ∖ 0 x ⁢ vol ⁡ f -1 x
33 0 32 wceq wff ∫ 1 = f ∈ g ∈ MblFn | g : ℝ ⟶ ℝ ∧ ran ⁡ g ∈ Fin ∧ vol ⁡ g -1 ℝ ∖ 0 ∈ ℝ ⟼ ∑ x ∈ ran ⁡ f ∖ 0 x ⁢ vol ⁡ f -1 x