Definition df-itg1 23609

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 23604	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 10138	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1630	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6028	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5251	. . . . . 6 class ran 𝑔
8		cfn 8110	. . . . . 6 class Fin
9	7, 8	wcel 2145	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5249	. . . . . . . 8 class ◡𝑔
11		cc0 10139	. . . . . . . . . 10 class 0
12	11	csn 4317	. . . . . . . . 9 class {0}
13	3, 12	cdif 3721	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5253	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 23452	. . . . . . 7 class vol
16	14, 15	cfv 6032	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2145	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1071	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 23603	. . . 4 class MblFn
20	18, 4, 19	crab 3065	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1630	. . . . . 6 class 𝑓
22	21	crn 5251	. . . . 5 class ran 𝑓
23	22, 12	cdif 3721	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1630	. . . . 5 class 𝑥
26	21	ccnv 5249	. . . . . . 7 class ◡𝑓
27	25	csn 4317	. . . . . . 7 class {𝑥}
28	26, 27	cima 5253	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6032	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 10144	. . . . 5 class ·
31	25, 29, 30	co 6794	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 14625	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 4864	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1631	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  23662  itg1val  23671