Definition df-itg1 24891

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

Step	Hyp	Ref	Expression
1		citg1 24886	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 10972	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1539	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6476	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5622	. . . . . 6 class ran 𝑔
8		cfn 8805	. . . . . 6 class Fin
9	7, 8	wcel 2105	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5620	. . . . . . . 8 class ◡𝑔
11		cc0 10973	. . . . . . . . . 10 class 0
12	11	csn 4574	. . . . . . . . 9 class {0}
13	3, 12	cdif 3895	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5624	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 24734	. . . . . . 7 class vol
16	14, 15	cfv 6480	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2105	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1086	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 24885	. . . 4 class MblFn
20	18, 4, 19	crab 3403	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1539	. . . . . 6 class 𝑓
22	21	crn 5622	. . . . 5 class ran 𝑓
23	22, 12	cdif 3895	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1539	. . . . 5 class 𝑥
26	21	ccnv 5620	. . . . . . 7 class ◡𝑓
27	25	csn 4574	. . . . . . 7 class {𝑥}
28	26, 27	cima 5624	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6480	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 10978	. . . . 5 class ·
31	25, 29, 30	co 7338	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15497	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5176	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1540	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  24945  itg1val  24954