Definition df-itg1 25808

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 25803	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11110	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1569	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6536	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5664	. . . . . 6 class ran 𝑔
8		cfn 8945	. . . . . 6 class Fin
9	7, 8	wcel 2146	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5662	. . . . . . . 8 class ◡𝑔
11		cc0 11111	. . . . . . . . . 10 class 0
12	11	csn 4591	. . . . . . . . 9 class {0}
13	3, 12	cdif 3903	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5666	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25651	. . . . . . 7 class vol
16	14, 15	cfv 6540	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2146	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1103	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25802	. . . 4 class MblFn
20	18, 4, 19	crab 3418	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1569	. . . . . 6 class 𝑓
22	21	crn 5664	. . . . 5 class ran 𝑓
23	22, 12	cdif 3903	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1569	. . . . 5 class 𝑥
26	21	ccnv 5662	. . . . . . 7 class ◡𝑓
27	25	csn 4591	. . . . . . 7 class {𝑥}
28	26, 27	cima 5666	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6540	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11116	. . . . 5 class ·
31	25, 29, 30	co 7416	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15756	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5194	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1570	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is used by:  isi1f  25862  itg1val  25871