Metamath Proof Explorer

Theorem itg2itg1

Description: The integral of a nonnegative simple function using S.2 is the same as its value under S.1 . (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion itg2itg1 
|- ( ( F e. dom S.1 /\ 0p oR <_ F ) -> ( S.2 ` F ) = ( S.1 ` F ) )

Proof

Step Hyp Ref Expression
1 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
2 xrge0f 
 |-  ( ( F : RR --> RR /\ 0p oR <_ F ) -> F : RR --> ( 0 [,] +oo ) )
3 1 2 sylan 
 |-  ( ( F e. dom S.1 /\ 0p oR <_ F ) -> F : RR --> ( 0 [,] +oo ) )
4 itg2cl 
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) e. RR* )
5 3 4 syl 
 |-  ( ( F e. dom S.1 /\ 0p oR <_ F ) -> ( S.2 ` F ) e. RR* )
6 itg1cl 
 |-  ( F e. dom S.1 -> ( S.1 ` F ) e. RR )
7 6 adantr 
 |-  ( ( F e. dom S.1 /\ 0p oR <_ F ) -> ( S.1 ` F ) e. RR )
8 7 rexrd 
 |-  ( ( F e. dom S.1 /\ 0p oR <_ F ) -> ( S.1 ` F ) e. RR* )
9 itg1le 
 |-  ( ( g e. dom S.1 /\ F e. dom S.1 /\ g oR <_ F ) -> ( S.1 ` g ) <_ ( S.1 ` F ) )
10 9 3expia 
 |-  ( ( g e. dom S.1 /\ F e. dom S.1 ) -> ( g oR <_ F -> ( S.1 ` g ) <_ ( S.1 ` F ) ) )
11 10 ancoms 
 |-  ( ( F e. dom S.1 /\ g e. dom S.1 ) -> ( g oR <_ F -> ( S.1 ` g ) <_ ( S.1 ` F ) ) )
12 11 ralrimiva 
 |-  ( F e. dom S.1 -> A. g e. dom S.1 ( g oR <_ F -> ( S.1 ` g ) <_ ( S.1 ` F ) ) )
13 12 adantr 
 |-  ( ( F e. dom S.1 /\ 0p oR <_ F ) -> A. g e. dom S.1 ( g oR <_ F -> ( S.1 ` g ) <_ ( S.1 ` F ) ) )
14 itg2leub 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( S.1 ` F ) e. RR* ) -> ( ( S.2 ` F ) <_ ( S.1 ` F ) <-> A. g e. dom S.1 ( g oR <_ F -> ( S.1 ` g ) <_ ( S.1 ` F ) ) ) )
15 3 8 14 syl2anc 
 |-  ( ( F e. dom S.1 /\ 0p oR <_ F ) -> ( ( S.2 ` F ) <_ ( S.1 ` F ) <-> A. g e. dom S.1 ( g oR <_ F -> ( S.1 ` g ) <_ ( S.1 ` F ) ) ) )
16 13 15 mpbird 
 |-  ( ( F e. dom S.1 /\ 0p oR <_ F ) -> ( S.2 ` F ) <_ ( S.1 ` F ) )
17 simpl 
 |-  ( ( F e. dom S.1 /\ 0p oR <_ F ) -> F e. dom S.1 )
18 reex 
 |-  RR e. _V
19 18 a1i 
 |-  ( F e. dom S.1 -> RR e. _V )
20 leid 
 |-  ( x e. RR -> x <_ x )
21 20 adantl 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> x <_ x )
22 19 1 21 caofref 
 |-  ( F e. dom S.1 -> F oR <_ F )
23 22 adantr 
 |-  ( ( F e. dom S.1 /\ 0p oR <_ F ) -> F oR <_ F )
24 itg2ub 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ F e. dom S.1 /\ F oR <_ F ) -> ( S.1 ` F ) <_ ( S.2 ` F ) )
25 3 17 23 24 syl3anc 
 |-  ( ( F e. dom S.1 /\ 0p oR <_ F ) -> ( S.1 ` F ) <_ ( S.2 ` F ) )
26 5 8 16 25 xrletrid 
 |-  ( ( F e. dom S.1 /\ 0p oR <_ F ) -> ( S.2 ` F ) = ( S.1 ` F ) )