Definition df-itg1 25537

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 25532	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11027	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1539	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6482	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5624	. . . . . 6 class ran 𝑔
8		cfn 8879	. . . . . 6 class Fin
9	7, 8	wcel 2109	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5622	. . . . . . . 8 class ◡𝑔
11		cc0 11028	. . . . . . . . . 10 class 0
12	11	csn 4579	. . . . . . . . 9 class {0}
13	3, 12	cdif 3902	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5626	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25380	. . . . . . 7 class vol
16	14, 15	cfv 6486	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2109	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1086	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25531	. . . 4 class MblFn
20	18, 4, 19	crab 3396	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1539	. . . . . 6 class 𝑓
22	21	crn 5624	. . . . 5 class ran 𝑓
23	22, 12	cdif 3902	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1539	. . . . 5 class 𝑥
26	21	ccnv 5622	. . . . . . 7 class ◡𝑓
27	25	csn 4579	. . . . . . 7 class {𝑥}
28	26, 27	cima 5626	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6486	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11033	. . . . 5 class ·
31	25, 29, 30	co 7353	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15611	. . 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  25591  itg1val  25600