Metamath Proof Explorer

Theorem itg20

Description: The integral of the zero function. (Contributed by Mario Carneiro, 28-Jun-2014)

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

Proof

Step Hyp Ref Expression
1 i1f0 
 |-  ( RR X. { 0 } ) e. dom S.1
2 reex 
 |-  RR e. _V
3 2 a1i 
 |-  ( T. -> RR e. _V )
4 i1ff 
 |-  ( ( RR X. { 0 } ) e. dom S.1 -> ( RR X. { 0 } ) : RR --> RR )
5 1 4 mp1i 
 |-  ( T. -> ( RR X. { 0 } ) : RR --> RR )
6 leid 
 |-  ( x e. RR -> x <_ x )
7 6 adantl 
 |-  ( ( T. /\ x e. RR ) -> x <_ x )
8 3 5 7 caofref 
 |-  ( T. -> ( RR X. { 0 } ) oR <_ ( RR X. { 0 } ) )
9 ax-resscn 
 |-  RR C_ CC
10 9 a1i 
 |-  ( T. -> RR C_ CC )
11 5 ffnd 
 |-  ( T. -> ( RR X. { 0 } ) Fn RR )
12 10 11 0pledm 
 |-  ( T. -> ( 0p oR <_ ( RR X. { 0 } ) <-> ( RR X. { 0 } ) oR <_ ( RR X. { 0 } ) ) )
13 8 12 mpbird 
 |-  ( T. -> 0p oR <_ ( RR X. { 0 } ) )
14 13 mptru 
 |-  0p oR <_ ( RR X. { 0 } )
15 itg2itg1 
 |-  ( ( ( RR X. { 0 } ) e. dom S.1 /\ 0p oR <_ ( RR X. { 0 } ) ) -> ( S.2 ` ( RR X. { 0 } ) ) = ( S.1 ` ( RR X. { 0 } ) ) )
16 1 14 15 mp2an 
 |-  ( S.2 ` ( RR X. { 0 } ) ) = ( S.1 ` ( RR X. { 0 } ) )
17 itg10 
 |-  ( S.1 ` ( RR X. { 0 } ) ) = 0
18 16 17 eqtri 
 |-  ( S.2 ` ( RR X. { 0 } ) ) = 0