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 ) )