Theorem isi1f

Description: The predicate " F is a simple function". A simple function is a finite nonnegative linear combination of indicator functions for finitely measurable sets. We use the idiom F e. dom S.1 to represent this concept because S.1 is the first preparation function for our final definition S. (see df-itg ); unlike that operator, which can integrate any function, this operator can only integrate simple functions. (Contributed by Mario Carneiro, 18-Jun-2014)

	Ref	Expression
Assertion	isi1f	|- ( F e. dom S.1 <-> ( F e. MblFn /\ ( F : RR --> RR /\ ran F e. Fin /\ ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) ) )

Proof

Step	Hyp	Ref	Expression
1		feq1	|- ( g = F -> ( g : RR --> RR <-> F : RR --> RR ) )
2		rneq	|- ( g = F -> ran g = ran F )
3	2	eleq1d	|- ( g = F -> ( ran g e. Fin <-> ran F e. Fin ) )
4		cnveq	|- ( g = F -> `' g = `' F )
5	4	imaeq1d	|- ( g = F -> ( `' g " ( RR \ { 0 } ) ) = ( `' F " ( RR \ { 0 } ) ) )
6	5	fveq2d	|- ( g = F -> ( vol ` ( `' g " ( RR \ { 0 } ) ) ) = ( vol ` ( `' F " ( RR \ { 0 } ) ) ) )
7	6	eleq1d	|- ( g = F -> ( ( vol ` ( `' g " ( RR \ { 0 } ) ) ) e. RR <-> ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) )
8	1 3 7	3anbi123d	|- ( g = F -> ( ( g : RR --> RR /\ ran g e. Fin /\ ( vol ` ( `' g " ( RR \ { 0 } ) ) ) e. RR ) <-> ( F : RR --> RR /\ ran F e. Fin /\ ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) ) )
9		sumex	|- sum_ x e. ( ran f \ { 0 } ) ( x x. ( vol ` ( `' f " { x } ) ) ) e. _V
10		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 } ) ) ) )
11	9 10	dmmpti	|- dom S.1 = { g e. MblFn | ( g : RR --> RR /\ ran g e. Fin /\ ( vol ` ( `' g " ( RR \ { 0 } ) ) ) e. RR ) }
12	8 11	elrab2	|- ( F e. dom S.1 <-> ( F e. MblFn /\ ( F : RR --> RR /\ ran F e. Fin /\ ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) ) )