Definition df-itg1 25670

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 25665	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11066	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1558	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6512	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5644	. . . . . 6 class ran 𝑔
8		cfn 8921	. . . . . 6 class Fin
9	7, 8	wcel 2141	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5642	. . . . . . . 8 class ◡𝑔
11		cc0 11067	. . . . . . . . . 10 class 0
12	11	csn 4579	. . . . . . . . 9 class {0}
13	3, 12	cdif 3899	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5646	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25513	. . . . . . 7 class vol
16	14, 15	cfv 6516	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2141	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1097	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25664	. . . 4 class MblFn
20	18, 4, 19	crab 3413	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1558	. . . . . 6 class 𝑓
22	21	crn 5644	. . . . 5 class ran 𝑓
23	22, 12	cdif 3899	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1558	. . . . 5 class 𝑥
26	21	ccnv 5642	. . . . . . 7 class ◡𝑓
27	25	csn 4579	. . . . . . 7 class {𝑥}
28	26, 27	cima 5646	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6516	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11072	. . . . 5 class ·
31	25, 29, 30	co 7391	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15704	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5178	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1559	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  25724  itg1val  25733