Definition df-itg1 25521

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 25516	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11067	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1539	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6507	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5639	. . . . . 6 class ran 𝑔
8		cfn 8918	. . . . . 6 class Fin
9	7, 8	wcel 2109	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5637	. . . . . . . 8 class ◡𝑔
11		cc0 11068	. . . . . . . . . 10 class 0
12	11	csn 4589	. . . . . . . . 9 class {0}
13	3, 12	cdif 3911	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5641	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25364	. . . . . . 7 class vol
16	14, 15	cfv 6511	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2109	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1086	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25515	. . . 4 class MblFn
20	18, 4, 19	crab 3405	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1539	. . . . . 6 class 𝑓
22	21	crn 5639	. . . . 5 class ran 𝑓
23	22, 12	cdif 3911	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1539	. . . . 5 class 𝑥
26	21	ccnv 5637	. . . . . . 7 class ◡𝑓
27	25	csn 4589	. . . . . . 7 class {𝑥}
28	26, 27	cima 5641	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6511	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11073	. . . . 5 class ·
31	25, 29, 30	co 7387	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15652	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5188	. 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  25575  itg1val  25584