Metamath Proof Explorer

Theorem itg1val

Description: The value of the integral on simple functions. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion itg1val 
|- ( F e. dom S.1 -> ( S.1 ` F ) = sum_ x e. ( ran F \ { 0 } ) ( x x. ( vol ` ( `' F " { x } ) ) ) )

Proof

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