Metamath Proof Explorer


Theorem itg2uba

Description: Approximate version of itg2ub . If F approximately dominates G , then S.1 G <_ S.2 F . (Contributed by Mario Carneiro, 11-Aug-2014)

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

Proof

Step Hyp Ref Expression
1 itg2uba.1
 |-  ( ph -> F : RR --> ( 0 [,] +oo ) )
2 itg2uba.2
 |-  ( ph -> G e. dom S.1 )
3 itg2uba.3
 |-  ( ph -> A C_ RR )
4 itg2uba.4
 |-  ( ph -> ( vol* ` A ) = 0 )
5 itg2uba.5
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> ( G ` x ) <_ ( F ` x ) )
6 itg1cl
 |-  ( G e. dom S.1 -> ( S.1 ` G ) e. RR )
7 2 6 syl
 |-  ( ph -> ( S.1 ` G ) e. RR )
8 7 rexrd
 |-  ( ph -> ( S.1 ` G ) e. RR* )
9 nulmbl
 |-  ( ( A C_ RR /\ ( vol* ` A ) = 0 ) -> A e. dom vol )
10 3 4 9 syl2anc
 |-  ( ph -> A e. dom vol )
11 cmmbl
 |-  ( A e. dom vol -> ( RR \ A ) e. dom vol )
12 10 11 syl
 |-  ( ph -> ( RR \ A ) e. dom vol )
13 ifnot
 |-  if ( -. x e. A , ( G ` x ) , 0 ) = if ( x e. A , 0 , ( G ` x ) )
14 eldif
 |-  ( x e. ( RR \ A ) <-> ( x e. RR /\ -. x e. A ) )
15 14 baibr
 |-  ( x e. RR -> ( -. x e. A <-> x e. ( RR \ A ) ) )
16 15 ifbid
 |-  ( x e. RR -> if ( -. x e. A , ( G ` x ) , 0 ) = if ( x e. ( RR \ A ) , ( G ` x ) , 0 ) )
17 13 16 eqtr3id
 |-  ( x e. RR -> if ( x e. A , 0 , ( G ` x ) ) = if ( x e. ( RR \ A ) , ( G ` x ) , 0 ) )
18 17 mpteq2ia
 |-  ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) ) = ( x e. RR |-> if ( x e. ( RR \ A ) , ( G ` x ) , 0 ) )
19 18 i1fres
 |-  ( ( G e. dom S.1 /\ ( RR \ A ) e. dom vol ) -> ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) ) e. dom S.1 )
20 2 12 19 syl2anc
 |-  ( ph -> ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) ) e. dom S.1 )
21 itg1cl
 |-  ( ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) ) e. dom S.1 -> ( S.1 ` ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) ) ) e. RR )
22 20 21 syl
 |-  ( ph -> ( S.1 ` ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) ) ) e. RR )
23 22 rexrd
 |-  ( ph -> ( S.1 ` ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) ) ) e. RR* )
24 itg2cl
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) e. RR* )
25 1 24 syl
 |-  ( ph -> ( S.2 ` F ) e. RR* )
26 i1ff
 |-  ( G e. dom S.1 -> G : RR --> RR )
27 2 26 syl
 |-  ( ph -> G : RR --> RR )
28 eldifi
 |-  ( y e. ( RR \ A ) -> y e. RR )
29 ffvelrn
 |-  ( ( G : RR --> RR /\ y e. RR ) -> ( G ` y ) e. RR )
30 27 28 29 syl2an
 |-  ( ( ph /\ y e. ( RR \ A ) ) -> ( G ` y ) e. RR )
31 30 leidd
 |-  ( ( ph /\ y e. ( RR \ A ) ) -> ( G ` y ) <_ ( G ` y ) )
32 eldif
 |-  ( y e. ( RR \ A ) <-> ( y e. RR /\ -. y e. A ) )
33 eleq1w
 |-  ( x = y -> ( x e. A <-> y e. A ) )
34 fveq2
 |-  ( x = y -> ( G ` x ) = ( G ` y ) )
35 33 34 ifbieq2d
 |-  ( x = y -> if ( x e. A , 0 , ( G ` x ) ) = if ( y e. A , 0 , ( G ` y ) ) )
36 eqid
 |-  ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) ) = ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) )
37 c0ex
 |-  0 e. _V
38 fvex
 |-  ( G ` y ) e. _V
39 37 38 ifex
 |-  if ( y e. A , 0 , ( G ` y ) ) e. _V
40 35 36 39 fvmpt
 |-  ( y e. RR -> ( ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) ) ` y ) = if ( y e. A , 0 , ( G ` y ) ) )
41 iffalse
 |-  ( -. y e. A -> if ( y e. A , 0 , ( G ` y ) ) = ( G ` y ) )
42 40 41 sylan9eq
 |-  ( ( y e. RR /\ -. y e. A ) -> ( ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) ) ` y ) = ( G ` y ) )
43 32 42 sylbi
 |-  ( y e. ( RR \ A ) -> ( ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) ) ` y ) = ( G ` y ) )
44 43 adantl
 |-  ( ( ph /\ y e. ( RR \ A ) ) -> ( ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) ) ` y ) = ( G ` y ) )
45 31 44 breqtrrd
 |-  ( ( ph /\ y e. ( RR \ A ) ) -> ( G ` y ) <_ ( ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) ) ` y ) )
46 2 3 4 20 45 itg1lea
 |-  ( ph -> ( S.1 ` G ) <_ ( S.1 ` ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) ) ) )
47 iftrue
 |-  ( x e. A -> if ( x e. A , 0 , ( G ` x ) ) = 0 )
48 47 adantl
 |-  ( ( ( ph /\ x e. RR ) /\ x e. A ) -> if ( x e. A , 0 , ( G ` x ) ) = 0 )
49 1 ffvelrnda
 |-  ( ( ph /\ x e. RR ) -> ( F ` x ) e. ( 0 [,] +oo ) )
50 elxrge0
 |-  ( ( F ` x ) e. ( 0 [,] +oo ) <-> ( ( F ` x ) e. RR* /\ 0 <_ ( F ` x ) ) )
51 49 50 sylib
 |-  ( ( ph /\ x e. RR ) -> ( ( F ` x ) e. RR* /\ 0 <_ ( F ` x ) ) )
52 51 simprd
 |-  ( ( ph /\ x e. RR ) -> 0 <_ ( F ` x ) )
53 52 adantr
 |-  ( ( ( ph /\ x e. RR ) /\ x e. A ) -> 0 <_ ( F ` x ) )
54 48 53 eqbrtrd
 |-  ( ( ( ph /\ x e. RR ) /\ x e. A ) -> if ( x e. A , 0 , ( G ` x ) ) <_ ( F ` x ) )
55 iffalse
 |-  ( -. x e. A -> if ( x e. A , 0 , ( G ` x ) ) = ( G ` x ) )
56 55 adantl
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. A ) -> if ( x e. A , 0 , ( G ` x ) ) = ( G ` x ) )
57 14 5 sylan2br
 |-  ( ( ph /\ ( x e. RR /\ -. x e. A ) ) -> ( G ` x ) <_ ( F ` x ) )
58 57 anassrs
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. A ) -> ( G ` x ) <_ ( F ` x ) )
59 56 58 eqbrtrd
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. A ) -> if ( x e. A , 0 , ( G ` x ) ) <_ ( F ` x ) )
60 54 59 pm2.61dan
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , 0 , ( G ` x ) ) <_ ( F ` x ) )
61 60 ralrimiva
 |-  ( ph -> A. x e. RR if ( x e. A , 0 , ( G ` x ) ) <_ ( F ` x ) )
62 reex
 |-  RR e. _V
63 62 a1i
 |-  ( ph -> RR e. _V )
64 fvex
 |-  ( G ` x ) e. _V
65 37 64 ifex
 |-  if ( x e. A , 0 , ( G ` x ) ) e. _V
66 65 a1i
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , 0 , ( G ` x ) ) e. _V )
67 fvexd
 |-  ( ( ph /\ x e. RR ) -> ( F ` x ) e. _V )
68 eqidd
 |-  ( ph -> ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) ) = ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) ) )
69 1 feqmptd
 |-  ( ph -> F = ( x e. RR |-> ( F ` x ) ) )
70 63 66 67 68 69 ofrfval2
 |-  ( ph -> ( ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) ) oR <_ F <-> A. x e. RR if ( x e. A , 0 , ( G ` x ) ) <_ ( F ` x ) ) )
71 61 70 mpbird
 |-  ( ph -> ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) ) oR <_ F )
72 itg2ub
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) ) e. dom S.1 /\ ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) ) oR <_ F ) -> ( S.1 ` ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) ) ) <_ ( S.2 ` F ) )
73 1 20 71 72 syl3anc
 |-  ( ph -> ( S.1 ` ( x e. RR |-> if ( x e. A , 0 , ( G ` x ) ) ) ) <_ ( S.2 ` F ) )
74 8 23 25 46 73 xrletrd
 |-  ( ph -> ( S.1 ` G ) <_ ( S.2 ` F ) )