Definition df-itg1 25934

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 25929	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11192	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1569	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6533	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5652	. . . . . 6 class ran 𝑔
8		cfn 8966	. . . . . 6 class Fin
9	7, 8	wcel 2145	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5650	. . . . . . . 8 class ◡𝑔
11		cc0 11193	. . . . . . . . . 10 class 0
12	11	csn 4584	. . . . . . . . 9 class {0}
13	3, 12	cdif 3896	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5654	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25777	. . . . . . 7 class vol
16	14, 15	cfv 6537	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2145	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1103	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25928	. . . 4 class MblFn
20	18, 4, 19	crab 3413	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1569	. . . . . 6 class 𝑓
22	21	crn 5652	. . . . 5 class ran 𝑓
23	22, 12	cdif 3896	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1569	. . . . 5 class 𝑥
26	21	ccnv 5650	. . . . . . 7 class ◡𝑓
27	25	csn 4584	. . . . . . 7 class {𝑥}
28	26, 27	cima 5654	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6537	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11198	. . . . 5 class ·
31	25, 29, 30	co 7418	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15846	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5186	. 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 used by:  isi1f  25988  itg1val  25997