Metamath Proof Explorer


Theorem itg1cl

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

Ref Expression
Assertion itg1cl ( ๐น โˆˆ dom โˆซ1 โ†’ ( โˆซ1 โ€˜ ๐น ) โˆˆ โ„ )

Proof

Step Hyp Ref Expression
1 itg1val โŠข ( ๐น โˆˆ dom โˆซ1 โ†’ ( โˆซ1 โ€˜ ๐น ) = ฮฃ ๐‘ฅ โˆˆ ( ran ๐น โˆ– { 0 } ) ( ๐‘ฅ ยท ( vol โ€˜ ( โ—ก ๐น โ€œ { ๐‘ฅ } ) ) ) )
2 i1frn โŠข ( ๐น โˆˆ dom โˆซ1 โ†’ ran ๐น โˆˆ Fin )
3 difss โŠข ( ran ๐น โˆ– { 0 } ) โІ ran ๐น
4 ssfi โŠข ( ( ran ๐น โˆˆ Fin โˆง ( ran ๐น โˆ– { 0 } ) โІ ran ๐น ) โ†’ ( ran ๐น โˆ– { 0 } ) โˆˆ Fin )
5 2 3 4 sylancl โŠข ( ๐น โˆˆ dom โˆซ1 โ†’ ( ran ๐น โˆ– { 0 } ) โˆˆ Fin )
6 i1ff โŠข ( ๐น โˆˆ dom โˆซ1 โ†’ ๐น : โ„ โŸถ โ„ )
7 6 frnd โŠข ( ๐น โˆˆ dom โˆซ1 โ†’ ran ๐น โІ โ„ )
8 7 ssdifssd โŠข ( ๐น โˆˆ dom โˆซ1 โ†’ ( ran ๐น โˆ– { 0 } ) โІ โ„ )
9 8 sselda โŠข ( ( ๐น โˆˆ dom โˆซ1 โˆง ๐‘ฅ โˆˆ ( ran ๐น โˆ– { 0 } ) ) โ†’ ๐‘ฅ โˆˆ โ„ )
10 i1fima2sn โŠข ( ( ๐น โˆˆ dom โˆซ1 โˆง ๐‘ฅ โˆˆ ( ran ๐น โˆ– { 0 } ) ) โ†’ ( vol โ€˜ ( โ—ก ๐น โ€œ { ๐‘ฅ } ) ) โˆˆ โ„ )
11 9 10 remulcld โŠข ( ( ๐น โˆˆ dom โˆซ1 โˆง ๐‘ฅ โˆˆ ( ran ๐น โˆ– { 0 } ) ) โ†’ ( ๐‘ฅ ยท ( vol โ€˜ ( โ—ก ๐น โ€œ { ๐‘ฅ } ) ) ) โˆˆ โ„ )
12 5 11 fsumrecl โŠข ( ๐น โˆˆ dom โˆซ1 โ†’ ฮฃ ๐‘ฅ โˆˆ ( ran ๐น โˆ– { 0 } ) ( ๐‘ฅ ยท ( vol โ€˜ ( โ—ก ๐น โ€œ { ๐‘ฅ } ) ) ) โˆˆ โ„ )
13 1 12 eqeltrd โŠข ( ๐น โˆˆ dom โˆซ1 โ†’ ( โˆซ1 โ€˜ ๐น ) โˆˆ โ„ )