Definition df-itg1 25577

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 25572	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11025	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1540	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6488	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5625	. . . . . 6 class ran 𝑔
8		cfn 8883	. . . . . 6 class Fin
9	7, 8	wcel 2113	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5623	. . . . . . . 8 class ◡𝑔
11		cc0 11026	. . . . . . . . . 10 class 0
12	11	csn 4580	. . . . . . . . 9 class {0}
13	3, 12	cdif 3898	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5627	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25420	. . . . . . 7 class vol
16	14, 15	cfv 6492	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2113	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1086	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25571	. . . 4 class MblFn
20	18, 4, 19	crab 3399	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1540	. . . . . 6 class 𝑓
22	21	crn 5625	. . . . 5 class ran 𝑓
23	22, 12	cdif 3898	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1540	. . . . 5 class 𝑥
26	21	ccnv 5623	. . . . . . 7 class ◡𝑓
27	25	csn 4580	. . . . . . 7 class {𝑥}
28	26, 27	cima 5627	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6492	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11031	. . . . 5 class ·
31	25, 29, 30	co 7358	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15609	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5179	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1541	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  25631  itg1val  25640