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