Metamath Proof Explorer

Theorem itg1lea

Description: Approximate version of itg1le . If F <_ G for almost all x , then S.1 F <_ S.1 G . (Contributed by Mario Carneiro, 28-Jun-2014) (Revised by Mario Carneiro, 6-Aug-2014)

Ref Expression
Hypotheses itg10a.1 
|- ( ph -> F e. dom S.1 )
itg10a.2 
|- ( ph -> A C_ RR )
itg10a.3 
|- ( ph -> ( vol* ` A ) = 0 )
itg1lea.4 
|- ( ph -> G e. dom S.1 )
itg1lea.5 
|- ( ( ph /\ x e. ( RR \ A ) ) -> ( F ` x ) <_ ( G ` x ) )
Assertion itg1lea 
|- ( ph -> ( S.1 ` F ) <_ ( S.1 ` G ) )

Proof

Step Hyp Ref Expression
1 itg10a.1 
 |-  ( ph -> F e. dom S.1 )
2 itg10a.2 
 |-  ( ph -> A C_ RR )
3 itg10a.3 
 |-  ( ph -> ( vol* ` A ) = 0 )
4 itg1lea.4 
 |-  ( ph -> G e. dom S.1 )
5 itg1lea.5 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> ( F ` x ) <_ ( G ` x ) )
6 i1fsub 
 |-  ( ( G e. dom S.1 /\ F e. dom S.1 ) -> ( G oF - F ) e. dom S.1 )
7 4 1 6 syl2anc 
 |-  ( ph -> ( G oF - F ) e. dom S.1 )
8 eldifi 
 |-  ( x e. ( RR \ A ) -> x e. RR )
9 i1ff 
 |-  ( G e. dom S.1 -> G : RR --> RR )
10 4 9 syl 
 |-  ( ph -> G : RR --> RR )
11 10 ffvelcdmda 
 |-  ( ( ph /\ x e. RR ) -> ( G ` x ) e. RR )
12 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
13 1 12 syl 
 |-  ( ph -> F : RR --> RR )
14 13 ffvelcdmda 
 |-  ( ( ph /\ x e. RR ) -> ( F ` x ) e. RR )
15 11 14 subge0d 
 |-  ( ( ph /\ x e. RR ) -> ( 0 <_ ( ( G ` x ) - ( F ` x ) ) <-> ( F ` x ) <_ ( G ` x ) ) )
16 8 15 sylan2 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> ( 0 <_ ( ( G ` x ) - ( F ` x ) ) <-> ( F ` x ) <_ ( G ` x ) ) )
17 5 16 mpbird 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> 0 <_ ( ( G ` x ) - ( F ` x ) ) )
18 10 ffnd 
 |-  ( ph -> G Fn RR )
19 13 ffnd 
 |-  ( ph -> F Fn RR )
20 reex 
 |-  RR e. _V
21 20 a1i 
 |-  ( ph -> RR e. _V )
22 inidm 
 |-  ( RR i^i RR ) = RR
23 eqidd 
 |-  ( ( ph /\ x e. RR ) -> ( G ` x ) = ( G ` x ) )
24 eqidd 
 |-  ( ( ph /\ x e. RR ) -> ( F ` x ) = ( F ` x ) )
25 18 19 21 21 22 23 24 ofval 
 |-  ( ( ph /\ x e. RR ) -> ( ( G oF - F ) ` x ) = ( ( G ` x ) - ( F ` x ) ) )
26 8 25 sylan2 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> ( ( G oF - F ) ` x ) = ( ( G ` x ) - ( F ` x ) ) )
27 17 26 breqtrrd 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> 0 <_ ( ( G oF - F ) ` x ) )
28 7 2 3 27 itg1ge0a 
 |-  ( ph -> 0 <_ ( S.1 ` ( G oF - F ) ) )
29 itg1sub 
 |-  ( ( G e. dom S.1 /\ F e. dom S.1 ) -> ( S.1 ` ( G oF - F ) ) = ( ( S.1 ` G ) - ( S.1 ` F ) ) )
30 4 1 29 syl2anc 
 |-  ( ph -> ( S.1 ` ( G oF - F ) ) = ( ( S.1 ` G ) - ( S.1 ` F ) ) )
31 28 30 breqtrd 
 |-  ( ph -> 0 <_ ( ( S.1 ` G ) - ( S.1 ` F ) ) )
32 itg1cl 
 |-  ( G e. dom S.1 -> ( S.1 ` G ) e. RR )
33 4 32 syl 
 |-  ( ph -> ( S.1 ` G ) e. RR )
34 itg1cl 
 |-  ( F e. dom S.1 -> ( S.1 ` F ) e. RR )
35 1 34 syl 
 |-  ( ph -> ( S.1 ` F ) e. RR )
36 33 35 subge0d 
 |-  ( ph -> ( 0 <_ ( ( S.1 ` G ) - ( S.1 ` F ) ) <-> ( S.1 ` F ) <_ ( S.1 ` G ) ) )
37 31 36 mpbid 
 |-  ( ph -> ( S.1 ` F ) <_ ( S.1 ` G ) )