Definition df-itg1 25528

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 25523	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11074	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1539	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6510	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5642	. . . . . 6 class ran 𝑔
8		cfn 8921	. . . . . 6 class Fin
9	7, 8	wcel 2109	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5640	. . . . . . . 8 class ◡𝑔
11		cc0 11075	. . . . . . . . . 10 class 0
12	11	csn 4592	. . . . . . . . 9 class {0}
13	3, 12	cdif 3914	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5644	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25371	. . . . . . 7 class vol
16	14, 15	cfv 6514	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2109	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1086	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25522	. . . 4 class MblFn
20	18, 4, 19	crab 3408	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1539	. . . . . 6 class 𝑓
22	21	crn 5642	. . . . 5 class ran 𝑓
23	22, 12	cdif 3914	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1539	. . . . 5 class 𝑥
26	21	ccnv 5640	. . . . . . 7 class ◡𝑓
27	25	csn 4592	. . . . . . 7 class {𝑥}
28	26, 27	cima 5644	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6514	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11080	. . . . 5 class ·
31	25, 29, 30	co 7390	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15659	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5191	. 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  25582  itg1val  25591