Definition df-itg1 25744

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 25739	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11095	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1566	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6529	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5660	. . . . . 6 class ran 𝑔
8		cfn 8939	. . . . . 6 class Fin
9	7, 8	wcel 2149	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5658	. . . . . . . 8 class ◡𝑔
11		cc0 11096	. . . . . . . . . 10 class 0
12	11	csn 4591	. . . . . . . . 9 class {0}
13	3, 12	cdif 3910	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5662	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25587	. . . . . . 7 class vol
16	14, 15	cfv 6533	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2149	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1101	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25738	. . . 4 class MblFn
20	18, 4, 19	crab 3423	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1566	. . . . . 6 class 𝑓
22	21	crn 5660	. . . . 5 class ran 𝑓
23	22, 12	cdif 3910	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1566	. . . . 5 class 𝑥
26	21	ccnv 5658	. . . . . . 7 class ◡𝑓
27	25	csn 4591	. . . . . . 7 class {𝑥}
28	26, 27	cima 5662	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6533	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11101	. . . . 5 class ·
31	25, 29, 30	co 7408	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15733	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5193	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1567	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  25798  itg1val  25807