Definition df-itg1 25985

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 25980	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11236	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1569	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6560	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5657	. . . . . 6 class ran 𝑔
8		cfn 9009	. . . . . 6 class Fin
9	7, 8	wcel 2147	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5655	. . . . . . . 8 class ◡𝑔
11		cc0 11237	. . . . . . . . . 10 class 0
12	11	csn 4588	. . . . . . . . 9 class {0}
13	3, 12	cdif 4048	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5659	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25828	. . . . . . 7 class vol
16	14, 15	cfv 6564	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2147	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1103	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25979	. . . 4 class MblFn
20	18, 4, 19	crab 3416	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1569	. . . . . 6 class 𝑓
22	21	crn 5657	. . . . 5 class ran 𝑓
23	22, 12	cdif 4048	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1569	. . . . 5 class 𝑥
26	21	ccnv 5655	. . . . . . 7 class ◡𝑓
27	25	csn 4588	. . . . . . 7 class {𝑥}
28	26, 27	cima 5659	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6564	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11242	. . . . 5 class ·
31	25, 29, 30	co 7449	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15894	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5190	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1570	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is used by:  isi1f  26039  itg1val  26048