Definition df-itg1 25571

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 25566	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11126	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1539	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6526	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5655	. . . . . 6 class ran 𝑔
8		cfn 8957	. . . . . 6 class Fin
9	7, 8	wcel 2108	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5653	. . . . . . . 8 class ◡𝑔
11		cc0 11127	. . . . . . . . . 10 class 0
12	11	csn 4601	. . . . . . . . 9 class {0}
13	3, 12	cdif 3923	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5657	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25414	. . . . . . 7 class vol
16	14, 15	cfv 6530	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2108	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1086	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25565	. . . 4 class MblFn
20	18, 4, 19	crab 3415	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1539	. . . . . 6 class 𝑓
22	21	crn 5655	. . . . 5 class ran 𝑓
23	22, 12	cdif 3923	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1539	. . . . 5 class 𝑥
26	21	ccnv 5653	. . . . . . 7 class ◡𝑓
27	25	csn 4601	. . . . . . 7 class {𝑥}
28	26, 27	cima 5657	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6530	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11132	. . . . 5 class ·
31	25, 29, 30	co 7403	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15700	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5201	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1540	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  25625  itg1val  25634