Definition df-itg1 25369

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 25364	. 2 class ∫1
2		vf	. . 3 setvar 𝑓
3		cr 11111	. . . . . 6 class ℝ
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1538	. . . . . 6 class 𝑔
6	3, 3, 5	wf 6538	. . . . 5 wff 𝑔:ℝ⟶ℝ
7	5	crn 5676	. . . . . 6 class ran 𝑔
8		cfn 8941	. . . . . 6 class Fin
9	7, 8	wcel 2104	. . . . 5 wff ran 𝑔 ∈ Fin
10	5	ccnv 5674	. . . . . . . 8 class ◡𝑔
11		cc0 11112	. . . . . . . . . 10 class 0
12	11	csn 4627	. . . . . . . . 9 class {0}
13	3, 12	cdif 3944	. . . . . . . 8 class (ℝ ∖ {0})
14	10, 13	cima 5678	. . . . . . 7 class (◡𝑔 “ (ℝ ∖ {0}))
15		cvol 25212	. . . . . . 7 class vol
16	14, 15	cfv 6542	. . . . . 6 class (vol‘(◡𝑔 “ (ℝ ∖ {0})))
17	16, 3	wcel 2104	. . . . 5 wff (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ
18	6, 9, 17	w3a 1085	. . . 4 wff (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)
19		cmbf 25363	. . . 4 class MblFn
20	18, 4, 19	crab 3430	. . 3 class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)}
21	2	cv 1538	. . . . . 6 class 𝑓
22	21	crn 5676	. . . . 5 class ran 𝑓
23	22, 12	cdif 3944	. . . 4 class (ran 𝑓 ∖ {0})
24		vx	. . . . . 6 setvar 𝑥
25	24	cv 1538	. . . . 5 class 𝑥
26	21	ccnv 5674	. . . . . . 7 class ◡𝑓
27	25	csn 4627	. . . . . . 7 class {𝑥}
28	26, 27	cima 5678	. . . . . 6 class (◡𝑓 “ {𝑥})
29	28, 15	cfv 6542	. . . . 5 class (vol‘(◡𝑓 “ {𝑥}))
30		cmul 11117	. . . . 5 class ·
31	25, 29, 30	co 7411	. . . 4 class (𝑥 · (vol‘(◡𝑓 “ {𝑥})))
32	23, 31, 24	csu 15636	. . 3 class Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥})))
33	2, 20, 32	cmpt 5230	. 2 class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
34	1, 33	wceq 1539	1 wff ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))

This definition is referenced by:  isi1f  25423  itg1val  25432