Definition df-itg1 25605

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 25600	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11028	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1546	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6481	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5619	. . . . . 6 class ran 𝑔
8		cfn 8883	. . . . . 6 class Fin
9	7, 8	wcel 2119	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5617	. . . . . . . 8 class ◡𝑔
11		cc0 11029	. . . . . . . . . 10 class 0
12	11	csn 4555	. . . . . . . . 9 class {0}
13	3, 12	cdif 3880	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5621	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25448	. . . . . . 7 class vol
16	14, 15	cfv 6485	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2119	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1092	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25599	. . . 4 class MblFn
20	18, 4, 19	crab 3391	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1546	. . . . . 6 class 𝑓
22	21	crn 5619	. . . . 5 class ran 𝑓
23	22, 12	cdif 3880	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1546	. . . . 5 class 𝑥
26	21	ccnv 5617	. . . . . . 7 class ◡𝑓
27	25	csn 4555	. . . . . . 7 class {𝑥}
28	26, 27	cima 5621	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6485	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11034	. . . . 5 class ·
31	25, 29, 30	co 7356	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15639	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5153	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1547	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  25659  itg1val  25668