Definition df-itg1 25543

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 25538	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11000	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1540	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6472	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5612	. . . . . 6 class ran 𝑔
8		cfn 8864	. . . . . 6 class Fin
9	7, 8	wcel 2111	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5610	. . . . . . . 8 class ◡𝑔
11		cc0 11001	. . . . . . . . . 10 class 0
12	11	csn 4571	. . . . . . . . 9 class {0}
13	3, 12	cdif 3894	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5614	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25386	. . . . . . 7 class vol
16	14, 15	cfv 6476	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2111	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1086	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25537	. . . 4 class MblFn
20	18, 4, 19	crab 3395	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1540	. . . . . 6 class 𝑓
22	21	crn 5612	. . . . 5 class ran 𝑓
23	22, 12	cdif 3894	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1540	. . . . 5 class 𝑥
26	21	ccnv 5610	. . . . . . 7 class ◡𝑓
27	25	csn 4571	. . . . . . 7 class {𝑥}
28	26, 27	cima 5614	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6476	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11006	. . . . 5 class ·
31	25, 29, 30	co 7341	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15588	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5167	. 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  25597  itg1val  25606