Definition df-itg1 23195

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 23190	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 9814	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1474	. . . . . 6 class 𝑔
6	3, 3, 5	wf 5800	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5039	. . . . . 6 class ran 𝑔
8		cfn 7841	. . . . . 6 class Fin
9	7, 8	wcel 1977	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5037	. . . . . . . 8 class ◡𝑔
11		cc0 9815	. . . . . . . . . 10 class 0
12	11	csn 4125	. . . . . . . . 9 class {0}
13	3, 12	cdif 3537	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5041	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 23039	. . . . . . 7 class vol
16	14, 15	cfv 5804	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 1977	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1031	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 23189	. . . 4 class MblFn
20	18, 4, 19	crab 2900	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1474	. . . . . 6 class 𝑓
22	21	crn 5039	. . . . 5 class ran 𝑓
23	22, 12	cdif 3537	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1474	. . . . 5 class 𝑥
26	21	ccnv 5037	. . . . . . 7 class ◡𝑓
27	25	csn 4125	. . . . . . 7 class {𝑥}
28	26, 27	cima 5041	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 5804	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 9820	. . . . 5 class ·
31	25, 29, 30	co 6549	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 14264	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 4643	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1475	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  23247  itg1val  23256