Definition df-itg1 25497

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 25492	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11043	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1539	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6495	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5632	. . . . . 6 class ran 𝑔
8		cfn 8895	. . . . . 6 class Fin
9	7, 8	wcel 2109	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5630	. . . . . . . 8 class ◡𝑔
11		cc0 11044	. . . . . . . . . 10 class 0
12	11	csn 4585	. . . . . . . . 9 class {0}
13	3, 12	cdif 3908	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5634	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25340	. . . . . . 7 class vol
16	14, 15	cfv 6499	. . . . . 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 25491	. . . 4 class MblFn
20	18, 4, 19	crab 3402	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1539	. . . . . 6 class 𝑓
22	21	crn 5632	. . . . 5 class ran 𝑓
23	22, 12	cdif 3908	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1539	. . . . 5 class 𝑥
26	21	ccnv 5630	. . . . . . 7 class ◡𝑓
27	25	csn 4585	. . . . . . 7 class {𝑥}
28	26, 27	cima 5634	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6499	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11049	. . . . 5 class ·
31	25, 29, 30	co 7369	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15628	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5183	. 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  25551  itg1val  25560