Definition df-itg1 24793

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 24788	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 10879	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1538	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6433	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5591	. . . . . 6 class ran 𝑔
8		cfn 8742	. . . . . 6 class Fin
9	7, 8	wcel 2107	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5589	. . . . . . . 8 class ◡𝑔
11		cc0 10880	. . . . . . . . . 10 class 0
12	11	csn 4562	. . . . . . . . 9 class {0}
13	3, 12	cdif 3885	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5593	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 24636	. . . . . . 7 class vol
16	14, 15	cfv 6437	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2107	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1086	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 24787	. . . 4 class MblFn
20	18, 4, 19	crab 3069	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1538	. . . . . 6 class 𝑓
22	21	crn 5591	. . . . 5 class ran 𝑓
23	22, 12	cdif 3885	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1538	. . . . 5 class 𝑥
26	21	ccnv 5589	. . . . . . 7 class ◡𝑓
27	25	csn 4562	. . . . . . 7 class {𝑥}
28	26, 27	cima 5593	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6437	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 10885	. . . . 5 class ·
31	25, 29, 30	co 7284	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15406	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5158	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1539	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  24847  itg1val  24856