Metamath Proof Explorer

Theorem itg1le

Description: If one simple function dominates another, then the integral of the larger is also larger. (Contributed by Mario Carneiro, 28-Jun-2014) (Revised by Mario Carneiro, 6-Aug-2014)

Ref Expression
Assertion itg1le 
|- ( ( F e. dom S.1 /\ G e. dom S.1 /\ F oR <_ G ) -> ( S.1 ` F ) <_ ( S.1 ` G ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 /\ F oR <_ G ) -> F e. dom S.1 )
2 0ss 
 |-  (/) C_ RR
3 2 a1i 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 /\ F oR <_ G ) -> (/) C_ RR )
4 ovol0 
 |-  ( vol* ` (/) ) = 0
5 4 a1i 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 /\ F oR <_ G ) -> ( vol* ` (/) ) = 0 )
6 simp2 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 /\ F oR <_ G ) -> G e. dom S.1 )
7 simpl 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> F e. dom S.1 )
8 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
9 ffn 
 |-  ( F : RR --> RR -> F Fn RR )
10 7 8 9 3syl 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> F Fn RR )
11 simpr 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> G e. dom S.1 )
12 i1ff 
 |-  ( G e. dom S.1 -> G : RR --> RR )
13 ffn 
 |-  ( G : RR --> RR -> G Fn RR )
14 11 12 13 3syl 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> G Fn RR )
15 reex 
 |-  RR e. _V
16 15 a1i 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> RR e. _V )
17 inidm 
 |-  ( RR i^i RR ) = RR
18 eqidd 
 |-  ( ( ( F e. dom S.1 /\ G e. dom S.1 ) /\ x e. RR ) -> ( F ` x ) = ( F ` x ) )
19 eqidd 
 |-  ( ( ( F e. dom S.1 /\ G e. dom S.1 ) /\ x e. RR ) -> ( G ` x ) = ( G ` x ) )
20 10 14 16 16 17 18 19 ofrval 
 |-  ( ( ( F e. dom S.1 /\ G e. dom S.1 ) /\ F oR <_ G /\ x e. RR ) -> ( F ` x ) <_ ( G ` x ) )
21 20 3exp 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> ( F oR <_ G -> ( x e. RR -> ( F ` x ) <_ ( G ` x ) ) ) )
22 21 3impia 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 /\ F oR <_ G ) -> ( x e. RR -> ( F ` x ) <_ ( G ` x ) ) )
23 eldifi 
 |-  ( x e. ( RR \ (/) ) -> x e. RR )
24 22 23 impel 
 |-  ( ( ( F e. dom S.1 /\ G e. dom S.1 /\ F oR <_ G ) /\ x e. ( RR \ (/) ) ) -> ( F ` x ) <_ ( G ` x ) )
25 1 3 5 6 24 itg1lea 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 /\ F oR <_ G ) -> ( S.1 ` F ) <_ ( S.1 ` G ) )