Metamath Proof Explorer

Theorem itg1cl

Description: Closure of the integral on simple functions. (Contributed by Mario Carneiro, 26-Jun-2014)

Ref Expression
Assertion itg1cl 
|- ( F e. dom S.1 -> ( S.1 ` F ) e. RR )

Proof

Step Hyp Ref Expression
1 itg1val 
 |-  ( F e. dom S.1 -> ( S.1 ` F ) = sum_ x e. ( ran F \ { 0 } ) ( x x. ( vol ` ( `' F " { x } ) ) ) )
2 i1frn 
 |-  ( F e. dom S.1 -> ran F e. Fin )
3 difss 
 |-  ( ran F \ { 0 } ) C_ ran F
4 ssfi 
 |-  ( ( ran F e. Fin /\ ( ran F \ { 0 } ) C_ ran F ) -> ( ran F \ { 0 } ) e. Fin )
5 2 3 4 sylancl 
 |-  ( F e. dom S.1 -> ( ran F \ { 0 } ) e. Fin )
6 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
7 6 frnd 
 |-  ( F e. dom S.1 -> ran F C_ RR )
8 7 ssdifssd 
 |-  ( F e. dom S.1 -> ( ran F \ { 0 } ) C_ RR )
9 8 sselda 
 |-  ( ( F e. dom S.1 /\ x e. ( ran F \ { 0 } ) ) -> x e. RR )
10 i1fima2sn 
 |-  ( ( F e. dom S.1 /\ x e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' F " { x } ) ) e. RR )
11 9 10 remulcld 
 |-  ( ( F e. dom S.1 /\ x e. ( ran F \ { 0 } ) ) -> ( x x. ( vol ` ( `' F " { x } ) ) ) e. RR )
12 5 11 fsumrecl 
 |-  ( F e. dom S.1 -> sum_ x e. ( ran F \ { 0 } ) ( x x. ( vol ` ( `' F " { x } ) ) ) e. RR )
13 1 12 eqeltrd 
 |-  ( F e. dom S.1 -> ( S.1 ` F ) e. RR )