Definition df-itg1 25597

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 25592	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11028	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1541	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6488	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5625	. . . . . 6 class ran 𝑔
8		cfn 8886	. . . . . 6 class Fin
9	7, 8	wcel 2114	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5623	. . . . . . . 8 class ◡𝑔
11		cc0 11029	. . . . . . . . . 10 class 0
12	11	csn 4568	. . . . . . . . 9 class {0}
13	3, 12	cdif 3887	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5627	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25440	. . . . . . 7 class vol
16	14, 15	cfv 6492	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2114	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1087	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25591	. . . 4 class MblFn
20	18, 4, 19	crab 3390	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1541	. . . . . 6 class 𝑓
22	21	crn 5625	. . . . 5 class ran 𝑓
23	22, 12	cdif 3887	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1541	. . . . 5 class 𝑥
26	21	ccnv 5623	. . . . . . 7 class ◡𝑓
27	25	csn 4568	. . . . . . 7 class {𝑥}
28	26, 27	cima 5627	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6492	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11034	. . . . 5 class ·
31	25, 29, 30	co 7360	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15639	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5167	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1542	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  25651  itg1val  25660