This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )