Definition df-itg1 25947

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 25942	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11203	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1568	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6535	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5651	. . . . . 6 class ran 𝑔
8		cfn 8977	. . . . . 6 class Fin
9	7, 8	wcel 2144	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5649	. . . . . . . 8 class ◡𝑔
11		cc0 11204	. . . . . . . . . 10 class 0
12	11	csn 4584	. . . . . . . . 9 class {0}
13	3, 12	cdif 4045	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5653	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25790	. . . . . . 7 class vol
16	14, 15	cfv 6539	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2144	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1103	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25941	. . . 4 class MblFn
20	18, 4, 19	crab 3412	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1568	. . . . . 6 class 𝑓
22	21	crn 5651	. . . . 5 class ran 𝑓
23	22, 12	cdif 4045	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1568	. . . . 5 class 𝑥
26	21	ccnv 5649	. . . . . . 7 class ◡𝑓
27	25	csn 4584	. . . . . . 7 class {𝑥}
28	26, 27	cima 5653	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6539	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11209	. . . . 5 class ·
31	25, 29, 30	co 7421	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15859	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5185	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1569	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is used by:  isi1f  26001  itg1val  26010