Definition df-itg1 23904

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 23899	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 10382	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1521	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6221	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5444	. . . . . 6 class ran 𝑔
8		cfn 8357	. . . . . 6 class Fin
9	7, 8	wcel 2081	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5442	. . . . . . . 8 class ◡𝑔
11		cc0 10383	. . . . . . . . . 10 class 0
12	11	csn 4472	. . . . . . . . 9 class {0}
13	3, 12	cdif 3856	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5446	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 23747	. . . . . . 7 class vol
16	14, 15	cfv 6225	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2081	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1080	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 23898	. . . 4 class MblFn
20	18, 4, 19	crab 3109	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1521	. . . . . 6 class 𝑓
22	21	crn 5444	. . . . 5 class ran 𝑓
23	22, 12	cdif 3856	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1521	. . . . 5 class 𝑥
26	21	ccnv 5442	. . . . . . 7 class ◡𝑓
27	25	csn 4472	. . . . . . 7 class {𝑥}
28	26, 27	cima 5446	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6225	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 10388	. . . . 5 class ·
31	25, 29, 30	co 7016	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 14876	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5041	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1522	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  23958  itg1val  23967