Definition df-itg1 25136

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 25131	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11108	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1540	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6539	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5677	. . . . . 6 class ran 𝑔
8		cfn 8938	. . . . . 6 class Fin
9	7, 8	wcel 2106	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5675	. . . . . . . 8 class ◡𝑔
11		cc0 11109	. . . . . . . . . 10 class 0
12	11	csn 4628	. . . . . . . . 9 class {0}
13	3, 12	cdif 3945	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5679	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 24979	. . . . . . 7 class vol
16	14, 15	cfv 6543	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2106	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1087	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25130	. . . 4 class MblFn
20	18, 4, 19	crab 3432	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1540	. . . . . 6 class 𝑓
22	21	crn 5677	. . . . 5 class ran 𝑓
23	22, 12	cdif 3945	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1540	. . . . 5 class 𝑥
26	21	ccnv 5675	. . . . . . 7 class ◡𝑓
27	25	csn 4628	. . . . . . 7 class {𝑥}
28	26, 27	cima 5679	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6543	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11114	. . . . 5 class ·
31	25, 29, 30	co 7408	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15631	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5231	. 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  25190  itg1val  25199