Definition df-itg1 25612

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 25607	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11035	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1546	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6488	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5626	. . . . . 6 class ran 𝑔
8		cfn 8890	. . . . . 6 class Fin
9	7, 8	wcel 2119	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5624	. . . . . . . 8 class ◡𝑔
11		cc0 11036	. . . . . . . . . 10 class 0
12	11	csn 4562	. . . . . . . . 9 class {0}
13	3, 12	cdif 3887	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5628	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25455	. . . . . . 7 class vol
16	14, 15	cfv 6492	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2119	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1092	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25606	. . . 4 class MblFn
20	18, 4, 19	crab 3392	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1546	. . . . . 6 class 𝑓
22	21	crn 5626	. . . . 5 class ran 𝑓
23	22, 12	cdif 3887	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1546	. . . . 5 class 𝑥
26	21	ccnv 5624	. . . . . . 7 class ◡𝑓
27	25	csn 4562	. . . . . . 7 class {𝑥}
28	26, 27	cima 5628	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6492	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11041	. . . . 5 class ·
31	25, 29, 30	co 7363	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15646	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5160	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1547	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  25666  itg1val  25675