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∖0x⁢vol⁡f-1x

Detailed syntax breakdown

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