Definition df-itg1 25593

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 25588	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11139	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1532	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6545	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5679	. . . . . 6 class ran 𝑔
8		cfn 8964	. . . . . 6 class Fin
9	7, 8	wcel 2098	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5677	. . . . . . . 8 class ◡𝑔
11		cc0 11140	. . . . . . . . . 10 class 0
12	11	csn 4630	. . . . . . . . 9 class {0}
13	3, 12	cdif 3941	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5681	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25436	. . . . . . 7 class vol
16	14, 15	cfv 6549	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2098	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1084	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25587	. . . 4 class MblFn
20	18, 4, 19	crab 3418	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1532	. . . . . 6 class 𝑓
22	21	crn 5679	. . . . 5 class ran 𝑓
23	22, 12	cdif 3941	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1532	. . . . 5 class 𝑥
26	21	ccnv 5677	. . . . . . 7 class ◡𝑓
27	25	csn 4630	. . . . . . 7 class {𝑥}
28	26, 27	cima 5681	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6549	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11145	. . . . 5 class ·
31	25, 29, 30	co 7419	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15668	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5232	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1533	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  25647  itg1val  25656