Definition df-itg1 25589

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 25584	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11037	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1541	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6496	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5633	. . . . . 6 class ran 𝑔
8		cfn 8895	. . . . . 6 class Fin
9	7, 8	wcel 2114	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5631	. . . . . . . 8 class ◡𝑔
11		cc0 11038	. . . . . . . . . 10 class 0
12	11	csn 4582	. . . . . . . . 9 class {0}
13	3, 12	cdif 3900	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5635	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25432	. . . . . . 7 class vol
16	14, 15	cfv 6500	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2114	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1087	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25583	. . . 4 class MblFn
20	18, 4, 19	crab 3401	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1541	. . . . . 6 class 𝑓
22	21	crn 5633	. . . . 5 class ran 𝑓
23	22, 12	cdif 3900	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1541	. . . . 5 class 𝑥
26	21	ccnv 5631	. . . . . . 7 class ◡𝑓
27	25	csn 4582	. . . . . . 7 class {𝑥}
28	26, 27	cima 5635	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6500	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11043	. . . . 5 class ·
31	25, 29, 30	co 7368	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15621	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5181	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1542	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  25643  itg1val  25652