This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdm 
 |-  ( ( 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 ffvelcdmda 
 |-  ( ( 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 ) )