Metamath Proof Explorer

Theorem itg2lea

Description: Approximate version of itg2le . If F <_ G for almost all x , then S.2 F <_ S.2 G . (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypotheses itg2lea.1 
|- ( ph -> F : RR --> ( 0 [,] +oo ) )
itg2lea.2 
|- ( ph -> G : RR --> ( 0 [,] +oo ) )
itg2lea.3 
|- ( ph -> A C_ RR )
itg2lea.4 
|- ( ph -> ( vol* ` A ) = 0 )
itg2lea.5 
|- ( ( ph /\ x e. ( RR \ A ) ) -> ( F ` x ) <_ ( G ` x ) )
Assertion itg2lea 
|- ( ph -> ( S.2 ` F ) <_ ( S.2 ` G ) )

Proof

Step Hyp Ref Expression
1 itg2lea.1 
 |-  ( ph -> F : RR --> ( 0 [,] +oo ) )
2 itg2lea.2 
 |-  ( ph -> G : RR --> ( 0 [,] +oo ) )
3 itg2lea.3 
 |-  ( ph -> A C_ RR )
4 itg2lea.4 
 |-  ( ph -> ( vol* ` A ) = 0 )
5 itg2lea.5 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> ( F ` x ) <_ ( G ` x ) )
6 2 adantr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> G : RR --> ( 0 [,] +oo ) )
7 simprl 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> f e. dom S.1 )
8 3 adantr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> A C_ RR )
9 4 adantr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> ( vol* ` A ) = 0 )
10 i1ff 
 |-  ( f e. dom S.1 -> f : RR --> RR )
11 10 ad2antrl 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> f : RR --> RR )
12 eldifi 
 |-  ( x e. ( RR \ A ) -> x e. RR )
13 ffvelrn 
 |-  ( ( f : RR --> RR /\ x e. RR ) -> ( f ` x ) e. RR )
14 11 12 13 syl2an 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) /\ x e. ( RR \ A ) ) -> ( f ` x ) e. RR )
15 14 rexrd 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) /\ x e. ( RR \ A ) ) -> ( f ` x ) e. RR* )
16 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
17 1 adantr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> F : RR --> ( 0 [,] +oo ) )
18 ffvelrn 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ x e. RR ) -> ( F ` x ) e. ( 0 [,] +oo ) )
19 17 12 18 syl2an 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) /\ x e. ( RR \ A ) ) -> ( F ` x ) e. ( 0 [,] +oo ) )
20 16 19 sselid 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) /\ x e. ( RR \ A ) ) -> ( F ` x ) e. RR* )
21 ffvelrn 
 |-  ( ( G : RR --> ( 0 [,] +oo ) /\ x e. RR ) -> ( G ` x ) e. ( 0 [,] +oo ) )
22 6 12 21 syl2an 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) /\ x e. ( RR \ A ) ) -> ( G ` x ) e. ( 0 [,] +oo ) )
23 16 22 sselid 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) /\ x e. ( RR \ A ) ) -> ( G ` x ) e. RR* )
24 simprr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> f oR <_ F )
25 11 ffnd 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> f Fn RR )
26 17 ffnd 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> F Fn RR )
27 reex 
 |-  RR e. _V
28 27 a1i 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> RR e. _V )
29 inidm 
 |-  ( RR i^i RR ) = RR
30 eqidd 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) /\ x e. RR ) -> ( f ` x ) = ( f ` x ) )
31 eqidd 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) /\ x e. RR ) -> ( F ` x ) = ( F ` x ) )
32 25 26 28 28 29 30 31 ofrfval 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> ( f oR <_ F <-> A. x e. RR ( f ` x ) <_ ( F ` x ) ) )
33 24 32 mpbid 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> A. x e. RR ( f ` x ) <_ ( F ` x ) )
34 33 r19.21bi 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) /\ x e. RR ) -> ( f ` x ) <_ ( F ` x ) )
35 12 34 sylan2 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) /\ x e. ( RR \ A ) ) -> ( f ` x ) <_ ( F ` x ) )
36 5 adantlr 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) /\ x e. ( RR \ A ) ) -> ( F ` x ) <_ ( G ` x ) )
37 15 20 23 35 36 xrletrd 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) /\ x e. ( RR \ A ) ) -> ( f ` x ) <_ ( G ` x ) )
38 6 7 8 9 37 itg2uba 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ F ) ) -> ( S.1 ` f ) <_ ( S.2 ` G ) )
39 38 expr 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( f oR <_ F -> ( S.1 ` f ) <_ ( S.2 ` G ) ) )
40 39 ralrimiva 
 |-  ( ph -> A. f e. dom S.1 ( f oR <_ F -> ( S.1 ` f ) <_ ( S.2 ` G ) ) )
41 itg2cl 
 |-  ( G : RR --> ( 0 [,] +oo ) -> ( S.2 ` G ) e. RR* )
42 2 41 syl 
 |-  ( ph -> ( S.2 ` G ) e. RR* )
43 itg2leub 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( S.2 ` G ) e. RR* ) -> ( ( S.2 ` F ) <_ ( S.2 ` G ) <-> A. f e. dom S.1 ( f oR <_ F -> ( S.1 ` f ) <_ ( S.2 ` G ) ) ) )
44 1 42 43 syl2anc 
 |-  ( ph -> ( ( S.2 ` F ) <_ ( S.2 ` G ) <-> A. f e. dom S.1 ( f oR <_ F -> ( S.1 ` f ) <_ ( S.2 ` G ) ) ) )
45 40 44 mpbird 
 |-  ( ph -> ( S.2 ` F ) <_ ( S.2 ` G ) )