Definition df-itg1 25568

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 25563	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11016	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1540	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6485	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5622	. . . . . 6 class ran 𝑔
8		cfn 8879	. . . . . 6 class Fin
9	7, 8	wcel 2113	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5620	. . . . . . . 8 class ◡𝑔
11		cc0 11017	. . . . . . . . . 10 class 0
12	11	csn 4577	. . . . . . . . 9 class {0}
13	3, 12	cdif 3895	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5624	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25411	. . . . . . 7 class vol
16	14, 15	cfv 6489	. . . . . 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 25562	. . . 4 class MblFn
20	18, 4, 19	crab 3396	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1540	. . . . . 6 class 𝑓
22	21	crn 5622	. . . . 5 class ran 𝑓
23	22, 12	cdif 3895	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1540	. . . . 5 class 𝑥
26	21	ccnv 5620	. . . . . . 7 class ◡𝑓
27	25	csn 4577	. . . . . . 7 class {𝑥}
28	26, 27	cima 5624	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6489	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11022	. . . . 5 class ·
31	25, 29, 30	co 7355	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15600	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5176	. 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  25622  itg1val  25631