Metamath Proof Explorer

Theorem itg10

Description: The zero function has zero integral. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion itg10 
|- ( S.1 ` ( RR X. { 0 } ) ) = 0

Proof

Step Hyp Ref Expression
1 i1f0 
 |-  ( RR X. { 0 } ) e. dom S.1
2 itg1val 
 |-  ( ( RR X. { 0 } ) e. dom S.1 -> ( S.1 ` ( RR X. { 0 } ) ) = sum_ x e. ( ran ( RR X. { 0 } ) \ { 0 } ) ( x x. ( vol ` ( `' ( RR X. { 0 } ) " { x } ) ) ) )
3 1 2 ax-mp 
 |-  ( S.1 ` ( RR X. { 0 } ) ) = sum_ x e. ( ran ( RR X. { 0 } ) \ { 0 } ) ( x x. ( vol ` ( `' ( RR X. { 0 } ) " { x } ) ) )
4 rnxpss 
 |-  ran ( RR X. { 0 } ) C_ { 0 }
5 ssdif0 
 |-  ( ran ( RR X. { 0 } ) C_ { 0 } <-> ( ran ( RR X. { 0 } ) \ { 0 } ) = (/) )
6 4 5 mpbi 
 |-  ( ran ( RR X. { 0 } ) \ { 0 } ) = (/)
7 6 sumeq1i 
 |-  sum_ x e. ( ran ( RR X. { 0 } ) \ { 0 } ) ( x x. ( vol ` ( `' ( RR X. { 0 } ) " { x } ) ) ) = sum_ x e. (/) ( x x. ( vol ` ( `' ( RR X. { 0 } ) " { x } ) ) )
8 sum0 
 |-  sum_ x e. (/) ( x x. ( vol ` ( `' ( RR X. { 0 } ) " { x } ) ) ) = 0
9 3 7 8 3eqtri 
 |-  ( S.1 ` ( RR X. { 0 } ) ) = 0