Definition df-itg1 23389

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	|- S.1 = ( f e. { g e. MblFn | ( g : RR --> RR /\ ran g e. Fin /\ ( vol ` ( `' g " ( RR \ { 0 } ) ) ) e. RR ) } |-> sum_ x e. ( ran f \ { 0 } ) ( x x. ( vol ` ( `' f " { x } ) ) ) )

Distinct variable group:   f, g, x

Detailed syntax breakdown of Definition df-itg1

Step	Hyp	Ref	Expression
1		citg1 23384	. 2 class S.1
2		vf	. . 3 setvar f
3		cr 9935	. . . . . 6 class RR
4		vg	. . . . . . 7 setvar g
5	4	cv 1482	. . . . . 6 class g
6	3, 3, 5	wf 5884	. . . . 5 wff g : RR --> RR
7	5	crn 5115	. . . . . 6 class ran g
8		cfn 7955	. . . . . 6 class Fin
9	7, 8	wcel 1990	. . . . 5 wff ran g e. Fin
10	5	ccnv 5113	. . . . . . . 8 class `' g
11		cc0 9936	. . . . . . . . . 10 class 0
12	11	csn 4177	. . . . . . . . 9 class { 0 }
13	3, 12	cdif 3571	. . . . . . . 8 class ( RR \ { 0 } )
14	10, 13	cima 5117	. . . . . . 7 class ( `' g " ( RR \ { 0 } ) )
15		cvol 23232	. . . . . . 7 class vol
16	14, 15	cfv 5888	. . . . . 6 class ( vol ` ( `' g " ( RR \ { 0 } ) ) )
17	16, 3	wcel 1990	. . . . 5 wff ( vol ` ( `' g " ( RR \ { 0 } ) ) ) e. RR
18	6, 9, 17	w3a 1037	. . . 4 wff ( g : RR --> RR /\ ran g e. Fin /\ ( vol ` ( `' g " ( RR \ { 0 } ) ) ) e. RR )
19		cmbf 23383	. . . 4 class MblFn
20	18, 4, 19	crab 2916	. . 3 class { g e. MblFn | ( g : RR --> RR /\ ran g e. Fin /\ ( vol ` ( `' g " ( RR \ { 0 } ) ) ) e. RR ) }
21	2	cv 1482	. . . . . 6 class f
22	21	crn 5115	. . . . 5 class ran f
23	22, 12	cdif 3571	. . . 4 class ( ran f \ { 0 } )
24		vx	. . . . . 6 setvar x
25	24	cv 1482	. . . . 5 class x
26	21	ccnv 5113	. . . . . . 7 class `' f
27	25	csn 4177	. . . . . . 7 class { x }
28	26, 27	cima 5117	. . . . . 6 class ( `' f " { x } )
29	28, 15	cfv 5888	. . . . 5 class ( vol ` ( `' f " { x } ) )
30		cmul 9941	. . . . 5 class x.
31	25, 29, 30	co 6650	. . . 4 class ( x x. ( vol ` ( `' f " { x } ) ) )
32	23, 31, 24	csu 14416	. . 3 class sum_ x e. ( ran f \ { 0 } ) ( x x. ( vol ` ( `' f " { x } ) ) )
33	2, 20, 32	cmpt 4729	. 2 class ( f e. { g e. MblFn | ( g : RR --> RR /\ ran g e. Fin /\ ( vol ` ( `' g " ( RR \ { 0 } ) ) ) e. RR ) } |-> sum_ x e. ( ran f \ { 0 } ) ( x x. ( vol ` ( `' f " { x } ) ) ) )
34	1, 33	wceq 1483	1 wff S.1 = ( f e. { g e. MblFn | ( g : RR --> RR /\ ran g e. Fin /\ ( vol ` ( `' g " ( RR \ { 0 } ) ) ) e. RR ) } |-> sum_ x e. ( ran f \ { 0 } ) ( x x. ( vol ` ( `' f " { x } ) ) ) )

This definition is referenced by:  isi1f  23441  itg1val  23450