Definition df-itg1 25674

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 25669	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11183	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1536	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6569	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5701	. . . . . 6 class ran 𝑔
8		cfn 9003	. . . . . 6 class Fin
9	7, 8	wcel 2108	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5699	. . . . . . . 8 class ◡𝑔
11		cc0 11184	. . . . . . . . . 10 class 0
12	11	csn 4648	. . . . . . . . 9 class {0}
13	3, 12	cdif 3973	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5703	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25517	. . . . . . 7 class vol
16	14, 15	cfv 6573	. . . . . 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 25668	. . . 4 class MblFn
20	18, 4, 19	crab 3443	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1536	. . . . . 6 class 𝑓
22	21	crn 5701	. . . . 5 class ran 𝑓
23	22, 12	cdif 3973	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1536	. . . . 5 class 𝑥
26	21	ccnv 5699	. . . . . . 7 class ◡𝑓
27	25	csn 4648	. . . . . . 7 class {𝑥}
28	26, 27	cima 5703	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6573	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11189	. . . . 5 class ·
31	25, 29, 30	co 7448	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15734	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5249	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1537	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  25728  itg1val  25737