Definition df-itg1 25655

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 25650	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11154	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1539	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6557	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5686	. . . . . 6 class ran 𝑔
8		cfn 8985	. . . . . 6 class Fin
9	7, 8	wcel 2108	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5684	. . . . . . . 8 class ◡𝑔
11		cc0 11155	. . . . . . . . . 10 class 0
12	11	csn 4626	. . . . . . . . 9 class {0}
13	3, 12	cdif 3948	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5688	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25498	. . . . . . 7 class vol
16	14, 15	cfv 6561	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2108	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1087	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25649	. . . 4 class MblFn
20	18, 4, 19	crab 3436	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1539	. . . . . 6 class 𝑓
22	21	crn 5686	. . . . 5 class ran 𝑓
23	22, 12	cdif 3948	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1539	. . . . 5 class 𝑥
26	21	ccnv 5684	. . . . . . 7 class ◡𝑓
27	25	csn 4626	. . . . . . 7 class {𝑥}
28	26, 27	cima 5688	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6561	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11160	. . . . 5 class ·
31	25, 29, 30	co 7431	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15722	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5225	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1540	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  25709  itg1val  25718