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 )