Definition df-itg1 25651

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 25646	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11058	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1549	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6502	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5637	. . . . . 6 class ran 𝑔
8		cfn 8912	. . . . . 6 class Fin
9	7, 8	wcel 2132	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5635	. . . . . . . 8 class ◡𝑔
11		cc0 11059	. . . . . . . . . 10 class 0
12	11	csn 4572	. . . . . . . . 9 class {0}
13	3, 12	cdif 3892	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5639	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25494	. . . . . . 7 class vol
16	14, 15	cfv 6506	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2132	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1095	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25645	. . . 4 class MblFn
20	18, 4, 19	crab 3404	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1549	. . . . . 6 class 𝑓
22	21	crn 5637	. . . . 5 class ran 𝑓
23	22, 12	cdif 3892	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1549	. . . . 5 class 𝑥
26	21	ccnv 5635	. . . . . . 7 class ◡𝑓
27	25	csn 4572	. . . . . . 7 class {𝑥}
28	26, 27	cima 5639	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6506	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11064	. . . . 5 class ·
31	25, 29, 30	co 7381	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15685	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5171	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1550	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  25705  itg1val  25714