Definition df-itg1 23624

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 23619	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 10230	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1636	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6107	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5325	. . . . . 6 class ran 𝑔
8		cfn 8202	. . . . . 6 class Fin
9	7, 8	wcel 2157	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5323	. . . . . . . 8 class ◡𝑔
11		cc0 10231	. . . . . . . . . 10 class 0
12	11	csn 4381	. . . . . . . . 9 class {0}
13	3, 12	cdif 3777	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5327	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 23467	. . . . . . 7 class vol
16	14, 15	cfv 6111	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2157	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1100	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 23618	. . . 4 class MblFn
20	18, 4, 19	crab 3111	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1636	. . . . . 6 class 𝑓
22	21	crn 5325	. . . . 5 class ran 𝑓
23	22, 12	cdif 3777	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1636	. . . . 5 class 𝑥
26	21	ccnv 5323	. . . . . . 7 class ◡𝑓
27	25	csn 4381	. . . . . . 7 class {𝑥}
28	26, 27	cima 5327	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6111	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 10236	. . . . 5 class ·
31	25, 29, 30	co 6884	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 14659	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 4934	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1637	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  23678  itg1val  23687