Definition df-itg1 25668

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 25663	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11151	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1535	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6558	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5689	. . . . . 6 class ran 𝑔
8		cfn 8983	. . . . . 6 class Fin
9	7, 8	wcel 2105	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5687	. . . . . . . 8 class ◡𝑔
11		cc0 11152	. . . . . . . . . 10 class 0
12	11	csn 4630	. . . . . . . . 9 class {0}
13	3, 12	cdif 3959	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5691	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25511	. . . . . . 7 class vol
16	14, 15	cfv 6562	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2105	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1086	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25662	. . . 4 class MblFn
20	18, 4, 19	crab 3432	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1535	. . . . . 6 class 𝑓
22	21	crn 5689	. . . . 5 class ran 𝑓
23	22, 12	cdif 3959	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1535	. . . . 5 class 𝑥
26	21	ccnv 5687	. . . . . . 7 class ◡𝑓
27	25	csn 4630	. . . . . . 7 class {𝑥}
28	26, 27	cima 5691	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6562	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11157	. . . . 5 class ·
31	25, 29, 30	co 7430	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15718	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5230	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1536	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  25722  itg1val  25731