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