Definition df-itg1 24471

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 24466	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 10693	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1542	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6354	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5537	. . . . . 6 class ran 𝑔
8		cfn 8604	. . . . . 6 class Fin
9	7, 8	wcel 2112	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5535	. . . . . . . 8 class ◡𝑔
11		cc0 10694	. . . . . . . . . 10 class 0
12	11	csn 4527	. . . . . . . . 9 class {0}
13	3, 12	cdif 3850	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5539	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 24314	. . . . . . 7 class vol
16	14, 15	cfv 6358	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2112	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1089	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 24465	. . . 4 class MblFn
20	18, 4, 19	crab 3055	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1542	. . . . . 6 class 𝑓
22	21	crn 5537	. . . . 5 class ran 𝑓
23	22, 12	cdif 3850	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1542	. . . . 5 class 𝑥
26	21	ccnv 5535	. . . . . . 7 class ◡𝑓
27	25	csn 4527	. . . . . . 7 class {𝑥}
28	26, 27	cima 5539	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6358	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 10699	. . . . 5 class ·
31	25, 29, 30	co 7191	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15214	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5120	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1543	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  24525  itg1val  24534