Definition df-itg1 25760

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 25755	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11100	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1569	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6534	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5664	. . . . . 6 class ran 𝑔
8		cfn 8944	. . . . . 6 class Fin
9	7, 8	wcel 2143	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5662	. . . . . . . 8 class ◡𝑔
11		cc0 11101	. . . . . . . . . 10 class 0
12	11	csn 4590	. . . . . . . . 9 class {0}
13	3, 12	cdif 3903	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5666	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25603	. . . . . . 7 class vol
16	14, 15	cfv 6538	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2143	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1103	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25754	. . . 4 class MblFn
20	18, 4, 19	crab 3416	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1569	. . . . . 6 class 𝑓
22	21	crn 5664	. . . . 5 class ran 𝑓
23	22, 12	cdif 3903	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1569	. . . . 5 class 𝑥
26	21	ccnv 5662	. . . . . . 7 class ◡𝑓
27	25	csn 4590	. . . . . . 7 class {𝑥}
28	26, 27	cima 5666	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6538	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11106	. . . . 5 class ·
31	25, 29, 30	co 7412	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15739	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5193	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1570	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  25814  itg1val  25823