Definition df-itg1 24689

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 24684	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 10801	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1538	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6414	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5581	. . . . . 6 class ran 𝑔
8		cfn 8691	. . . . . 6 class Fin
9	7, 8	wcel 2108	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5579	. . . . . . . 8 class ◡𝑔
11		cc0 10802	. . . . . . . . . 10 class 0
12	11	csn 4558	. . . . . . . . 9 class {0}
13	3, 12	cdif 3880	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5583	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 24532	. . . . . . 7 class vol
16	14, 15	cfv 6418	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2108	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1085	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 24683	. . . 4 class MblFn
20	18, 4, 19	crab 3067	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1538	. . . . . 6 class 𝑓
22	21	crn 5581	. . . . 5 class ran 𝑓
23	22, 12	cdif 3880	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1538	. . . . 5 class 𝑥
26	21	ccnv 5579	. . . . . . 7 class ◡𝑓
27	25	csn 4558	. . . . . . 7 class {𝑥}
28	26, 27	cima 5583	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6418	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 10807	. . . . 5 class ·
31	25, 29, 30	co 7255	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15325	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5153	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1539	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  24743  itg1val  24752