Theorem itg2split 19594

Description: The S.2 integral splits under an almost disjoint union. (The proof avoids the use of itg2add 19604 which requires CC.) (Contributed by Mario Carneiro, 11-Aug-2014.)

Hypotheses

Ref	Expression
itg2split.a	|- ( ph -> A e. dom vol )
itg2split.b	|- ( ph -> B e. dom vol )
itg2split.i	|- ( ph -> ( vol * ` ( A i^i B ) ) = 0 )
itg2split.u	|- ( ph -> U = ( A u. B ) )
itg2split.c	|- ( ( ph /\ x e. U ) -> C e. ( 0 [,] +oo ) )
itg2split.f	|- F = ( x e. RR |-> if ( x e. A , C , 0 ) )
itg2split.g	|- G = ( x e. RR |-> if ( x e. B , C , 0 ) )
itg2split.h	|- H = ( x e. RR |-> if ( x e. U , C , 0 ) )
itg2split.sf	|- ( ph -> ( S.2 ` F ) e. RR )
itg2split.sg	|- ( ph -> ( S.2 ` G ) e. RR )

Assertion

Ref	Expression
itg2split	|- ( ph -> ( S.2 ` H ) = ( ( S.2 ` F ) + ( S.2 ` G ) ) )

Distinct variable groups:   ph, x   x, A   x, B   x, U

Allowed substitution hints:   C( x)   F( x)   G( x)   H( x)

Proof of Theorem itg2split

Dummy variables f g y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		itg2split.a	. . 3 |- ( ph -> A e. dom vol )
2		itg2split.b	. . 3 |- ( ph -> B e. dom vol )
3		itg2split.i	. . 3 |- ( ph -> ( vol * ` ( A i^i B ) ) = 0 )
4		itg2split.u	. . 3 |- ( ph -> U = ( A u. B ) )
5		itg2split.c	. . 3 |- ( ( ph /\ x e. U ) -> C e. ( 0 [,] +oo ) )
6		itg2split.f	. . 3 |- F = ( x e. RR |-> if ( x e. A , C , 0 ) )
7		itg2split.g	. . 3 |- G = ( x e. RR |-> if ( x e. B , C , 0 ) )
8		itg2split.h	. . 3 |- H = ( x e. RR |-> if ( x e. U , C , 0 ) )
9		itg2split.sf	. . 3 |- ( ph -> ( S.2 ` F ) e. RR )
10		itg2split.sg	. . 3 |- ( ph -> ( S.2 ` G ) e. RR )
11	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	itg2splitlem 19593	. 2 |- ( ph -> ( S.2 ` H ) <_ ( ( S.2 ` F ) + ( S.2 ` G ) ) )
12	10	adantr 452	. . . . . . 7 |- ( ( ph /\ ( f e. dom S.1 /\ f o R <_ F ) ) -> ( S.2 ` G ) e. RR )
13	5	adantlr 696	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR ) /\ x e. U ) -> C e. ( 0 [,] +oo ) )
14		0xr 9087	. . . . . . . . . . . . 13 |- 0 e. RR*
15		0le0 10037	. . . . . . . . . . . . 13 |- 0 <_ 0
16		elxrge0 10964	. . . . . . . . . . . . 13 |- ( 0 e. ( 0 [,] +oo ) <-> ( 0 e. RR* /\ 0 <_ 0 ) )
17	14, 15, 16	mpbir2an 887	. . . . . . . . . . . 12 |- 0 e. ( 0 [,] +oo )
18	17	a1i 11	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR ) /\ -. x e. U ) -> 0 e. ( 0 [,] +oo ) )
19	13, 18	ifclda 3726	. . . . . . . . . 10 |- ( ( ph /\ x e. RR ) -> if ( x e. U , C , 0 ) e. ( 0 [,] +oo ) )
20	19, 8	fmptd 5852	. . . . . . . . 9 |- ( ph -> H : RR --> ( 0 [,] +oo ) )
21	9, 10	readdcld 9071	. . . . . . . . 9 |- ( ph -> ( ( S.2 ` F ) + ( S.2 ` G ) ) e. RR )
22		itg2lecl 19583	. . . . . . . . 9 |- ( ( H : RR --> ( 0 [,] +oo ) /\ ( ( S.2 ` F ) + ( S.2 ` G ) ) e. RR /\ ( S.2 ` H ) <_ ( ( S.2 ` F ) + ( S.2 ` G ) ) ) -> ( S.2 ` H ) e. RR )
23	20, 21, 11, 22	syl3anc 1184	. . . . . . . 8 |- ( ph -> ( S.2 ` H ) e. RR )
24	23	adantr 452	. . . . . . 7 |- ( ( ph /\ ( f e. dom S.1 /\ f o R <_ F ) ) -> ( S.2 ` H ) e. RR )
25		itg1cl 19530	. . . . . . . 8 |- ( f e. dom S.1 -> ( S.1 ` f ) e. RR )
26	25	ad2antrl 709	. . . . . . 7 |- ( ( ph /\ ( f e. dom S.1 /\ f o R <_ F ) ) -> ( S.1 ` f ) e. RR )
27		simprll 739	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> f e. dom S.1 )
28		simprrl 741	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> g e. dom S.1 )
29	27, 28	itg1add 19546	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> ( S.1 ` ( f o F + g ) ) = ( ( S.1 ` f ) + ( S.1 ` g ) ) )
30	20	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> H : RR --> ( 0 [,] +oo ) )
31	27, 28	i1fadd 19540	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> ( f o F + g ) e. dom S.1 )
32		inss1 3521	. . . . . . . . . . . . . . . 16 |- ( A i^i B ) C_ A
33		mblss 19380	. . . . . . . . . . . . . . . . 17 |- ( A e. dom vol -> A C_ RR )
34	1, 33	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> A C_ RR )
35	32, 34	syl5ss 3319	. . . . . . . . . . . . . . 15 |- ( ph -> ( A i^i B ) C_ RR )
36	35	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> ( A i^i B ) C_ RR )
37	3	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> ( vol * ` ( A i^i B ) ) = 0 )
38		nfv 1626	. . . . . . . . . . . . . . . . . 18 |- F/ x ph
39		nfv 1626	. . . . . . . . . . . . . . . . . . . 20 |- F/ x f e. dom S.1
40		nfcv 2540	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ x f
41		nfcv 2540	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ x o R <_
42		nfmpt1 4258	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ x ( x e. RR |-> if ( x e. A , C , 0 ) )
43	6, 42	nfcxfr 2537	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ x F
44	40, 41, 43	nfbr 4216	. . . . . . . . . . . . . . . . . . . 20 |- F/ x f o R <_ F
45	39, 44	nfan 1842	. . . . . . . . . . . . . . . . . . 19 |- F/ x ( f e. dom S.1 /\ f o R <_ F )
46		nfv 1626	. . . . . . . . . . . . . . . . . . . 20 |- F/ x g e. dom S.1
47		nfcv 2540	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ x g
48		nfmpt1 4258	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ x ( x e. RR |-> if ( x e. B , C , 0 ) )
49	7, 48	nfcxfr 2537	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ x G
50	47, 41, 49	nfbr 4216	. . . . . . . . . . . . . . . . . . . 20 |- F/ x g o R <_ G
51	46, 50	nfan 1842	. . . . . . . . . . . . . . . . . . 19 |- F/ x ( g e. dom S.1 /\ g o R <_ G )
52	45, 51	nfan 1842	. . . . . . . . . . . . . . . . . 18 |- F/ x ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) )
53	38, 52	nfan 1842	. . . . . . . . . . . . . . . . 17 |- F/ x ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) )
54		eldifi 3429	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( RR \ ( A i^i B ) ) -> x e. RR )
55		i1ff 19521	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( f e. dom S.1 -> f : RR --> RR )
56	27, 55	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> f : RR --> RR )
57		ffn 5550	. . . . . . . . . . . . . . . . . . . . . 22 |- ( f : RR --> RR -> f Fn RR )
58	56, 57	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> f Fn RR )
59		i1ff 19521	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( g e. dom S.1 -> g : RR --> RR )
60	28, 59	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> g : RR --> RR )
61		ffn 5550	. . . . . . . . . . . . . . . . . . . . . 22 |- ( g : RR --> RR -> g Fn RR )
62	60, 61	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> g Fn RR )
63		reex 9037	. . . . . . . . . . . . . . . . . . . . . 22 |- RR e. _V
64	63	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> RR e. _V )
65		inidm 3510	. . . . . . . . . . . . . . . . . . . . 21 |- ( RR i^i RR ) = RR
66		eqidd 2405	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. RR ) -> ( f ` x ) = ( f ` x ) )
67		eqidd 2405	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. RR ) -> ( g ` x ) = ( g ` x ) )
68	58, 62, 64, 64, 65, 66, 67	ofval 6273	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. RR ) -> ( ( f o F + g ) ` x ) = ( ( f ` x ) + ( g ` x ) ) )
69	54, 68	sylan2 461	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( ( f o F + g ) ` x ) = ( ( f ` x ) + ( g ` x ) ) )
70		ffvelrn 5827	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f : RR --> RR /\ x e. RR ) -> ( f ` x ) e. RR )
71	56, 54, 70	syl2an 464	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( f ` x ) e. RR )
72		ffvelrn 5827	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g : RR --> RR /\ x e. RR ) -> ( g ` x ) e. RR )
73	60, 54, 72	syl2an 464	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( g ` x ) e. RR )
74	71, 73	readdcld 9071	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( ( f ` x ) + ( g ` x ) ) e. RR )
75	74	rexrd 9090	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( ( f ` x ) + ( g ` x ) ) e. RR* )
76	75	adantr 452	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( ( f ` x ) + ( g ` x ) ) e. RR* )
77	71	adantr 452	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( f ` x ) e. RR )
78	77	rexrd 9090	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( f ` x ) e. RR* )
79		iccssxr 10949	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 0 [,] +oo ) C_ RR*
80		ffvelrn 5827	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( H : RR --> ( 0 [,] +oo ) /\ x e. RR ) -> ( H ` x ) e. ( 0 [,] +oo ) )
81	30, 54, 80	syl2an 464	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( H ` x ) e. ( 0 [,] +oo ) )
82	79, 81	sseldi 3306	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( H ` x ) e. RR* )
83	82	adantr 452	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( H ` x ) e. RR* )
84	73	adantr 452	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( g ` x ) e. RR )
85		0re 9047	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 0 e. RR
86	85	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> 0 e. RR )
87		simprrr 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> g o R <_ G )
88	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ g Fn RR ) -> RR e. _V )
89		fvex 5701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( g ` x ) e. _V
90	89	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ g Fn RR ) /\ x e. RR ) -> ( g ` x ) e. _V )
91		ssun2 3471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- B C_ ( A u. B )
92	91, 4	syl5sseqr 3357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ph -> B C_ U )
93	92	sselda 3308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ph /\ x e. B ) -> x e. U )
94	93	adantlr 696	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ x e. RR ) /\ x e. B ) -> x e. U )
95	94, 13	syldan 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ x e. RR ) /\ x e. B ) -> C e. ( 0 [,] +oo ) )
96	17	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ x e. RR ) /\ -. x e. B ) -> 0 e. ( 0 [,] +oo ) )
97	95, 96	ifclda 3726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ x e. RR ) -> if ( x e. B , C , 0 ) e. ( 0 [,] +oo ) )
98	97	adantlr 696	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ g Fn RR ) /\ x e. RR ) -> if ( x e. B , C , 0 ) e. ( 0 [,] +oo ) )
99		simpr 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ g Fn RR ) -> g Fn RR )
100		dffn5 5731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( g Fn RR <-> g = ( x e. RR |-> ( g ` x ) ) )
101	99, 100	sylib 189	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ g Fn RR ) -> g = ( x e. RR |-> ( g ` x ) ) )
102	7	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ g Fn RR ) -> G = ( x e. RR |-> if ( x e. B , C , 0 ) ) )
103	88, 90, 98, 101, 102	ofrfval2 6282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ g Fn RR ) -> ( g o R <_ G <-> A. x e. RR ( g ` x ) <_ if ( x e. B , C , 0 ) ) )
104	62, 103	syldan 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> ( g o R <_ G <-> A. x e. RR ( g ` x ) <_ if ( x e. B , C , 0 ) ) )
105	87, 104	mpbid 202	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> A. x e. RR ( g ` x ) <_ if ( x e. B , C , 0 ) )
106	105	r19.21bi 2764	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. RR ) -> ( g ` x ) <_ if ( x e. B , C , 0 ) )
107	54, 106	sylan2 461	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( g ` x ) <_ if ( x e. B , C , 0 ) )
108	107	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( g ` x ) <_ if ( x e. B , C , 0 ) )
109		eldifn 3430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. ( RR \ ( A i^i B ) ) -> -. x e. ( A i^i B ) )
110	109	adantl 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> -. x e. ( A i^i B ) )
111		elin 3490	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
112	110, 111	sylnib 296	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> -. ( x e. A /\ x e. B ) )
113		imnan 412	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( x e. A -> -. x e. B ) <-> -. ( x e. A /\ x e. B ) )
114	112, 113	sylibr 204	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( x e. A -> -. x e. B ) )
115	114	imp 419	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> -. x e. B )
116		iffalse 3706	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( -. x e. B -> if ( x e. B , C , 0 ) = 0 )
117	115, 116	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> if ( x e. B , C , 0 ) = 0 )
118	108, 117	breqtrd 4196	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( g ` x ) <_ 0 )
119	84, 86, 77, 118	leadd2dd 9597	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( ( f ` x ) + ( g ` x ) ) <_ ( ( f ` x ) + 0 ) )
120	77	recnd 9070	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( f ` x ) e. CC )
121	120	addid1d 9222	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( ( f ` x ) + 0 ) = ( f ` x ) )
122	119, 121	breqtrd 4196	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( ( f ` x ) + ( g ` x ) ) <_ ( f ` x ) )
123		simprlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> f o R <_ F )
124	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ f Fn RR ) -> RR e. _V )
125		fvex 5701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( f ` x ) e. _V
126	125	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ f Fn RR ) /\ x e. RR ) -> ( f ` x ) e. _V )
127		ssun1 3470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- A C_ ( A u. B )
128	127, 4	syl5sseqr 3357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ph -> A C_ U )
129	128	sselda 3308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ x e. A ) -> x e. U )
130	129	adantlr 696	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ph /\ x e. RR ) /\ x e. A ) -> x e. U )
131	130, 13	syldan 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ x e. RR ) /\ x e. A ) -> C e. ( 0 [,] +oo ) )
132	17	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ x e. RR ) /\ -. x e. A ) -> 0 e. ( 0 [,] +oo ) )
133	131, 132	ifclda 3726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ x e. RR ) -> if ( x e. A , C , 0 ) e. ( 0 [,] +oo ) )
134	133	adantlr 696	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ f Fn RR ) /\ x e. RR ) -> if ( x e. A , C , 0 ) e. ( 0 [,] +oo ) )
135		simpr 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ f Fn RR ) -> f Fn RR )
136		dffn5 5731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( f Fn RR <-> f = ( x e. RR |-> ( f ` x ) ) )
137	135, 136	sylib 189	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ f Fn RR ) -> f = ( x e. RR |-> ( f ` x ) ) )
138	6	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ f Fn RR ) -> F = ( x e. RR |-> if ( x e. A , C , 0 ) ) )
139	124, 126, 134, 137, 138	ofrfval2 6282	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ f Fn RR ) -> ( f o R <_ F <-> A. x e. RR ( f ` x ) <_ if ( x e. A , C , 0 ) ) )
140	58, 139	syldan 457	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> ( f o R <_ F <-> A. x e. RR ( f ` x ) <_ if ( x e. A , C , 0 ) ) )
141	123, 140	mpbid 202	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> A. x e. RR ( f ` x ) <_ if ( x e. A , C , 0 ) )
142	141	r19.21bi 2764	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. RR ) -> ( f ` x ) <_ if ( x e. A , C , 0 ) )
143	54, 142	sylan2 461	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( f ` x ) <_ if ( x e. A , C , 0 ) )
144	143	adantr 452	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( f ` x ) <_ if ( x e. A , C , 0 ) )
145	128	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> A C_ U )
146	145	sselda 3308	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> x e. U )
147		iftrue 3705	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x e. U -> if ( x e. U , C , 0 ) = C )
148	146, 147	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> if ( x e. U , C , 0 ) = C )
149		simpr 448	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. RR ) -> x e. RR )
150	19	adantlr 696	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. RR ) -> if ( x e. U , C , 0 ) e. ( 0 [,] +oo ) )
151	8	fvmpt2 5771	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( x e. RR /\ if ( x e. U , C , 0 ) e. ( 0 [,] +oo ) ) -> ( H ` x ) = if ( x e. U , C , 0 ) )
152	149, 150, 151	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. RR ) -> ( H ` x ) = if ( x e. U , C , 0 ) )
153	54, 152	sylan2 461	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( H ` x ) = if ( x e. U , C , 0 ) )
154	153	adantr 452	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( H ` x ) = if ( x e. U , C , 0 ) )
155		iftrue 3705	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x e. A -> if ( x e. A , C , 0 ) = C )
156	155	adantl 453	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> if ( x e. A , C , 0 ) = C )
157	148, 154, 156	3eqtr4d 2446	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( H ` x ) = if ( x e. A , C , 0 ) )
158	144, 157	breqtrrd 4198	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( f ` x ) <_ ( H ` x ) )
159	76, 78, 83, 122, 158	xrletrd 10708	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ x e. A ) -> ( ( f ` x ) + ( g ` x ) ) <_ ( H ` x ) )
160	75	adantr 452	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( ( f ` x ) + ( g ` x ) ) e. RR* )
161	73	adantr 452	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( g ` x ) e. RR )
162	161	rexrd 9090	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( g ` x ) e. RR* )
163	82	adantr 452	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( H ` x ) e. RR* )
164	71	adantr 452	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( f ` x ) e. RR )
165	85	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> 0 e. RR )
166	143	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( f ` x ) <_ if ( x e. A , C , 0 ) )
167		iffalse 3706	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( -. x e. A -> if ( x e. A , C , 0 ) = 0 )
168	167	adantl 453	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> if ( x e. A , C , 0 ) = 0 )
169	166, 168	breqtrd 4196	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( f ` x ) <_ 0 )
170	164, 165, 161, 169	leadd1dd 9596	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( ( f ` x ) + ( g ` x ) ) <_ ( 0 + ( g ` x ) ) )
171	161	recnd 9070	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( g ` x ) e. CC )
172	171	addid2d 9223	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( 0 + ( g ` x ) ) = ( g ` x ) )
173	170, 172	breqtrd 4196	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( ( f ` x ) + ( g ` x ) ) <_ ( g ` x ) )
174	107	adantr 452	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( g ` x ) <_ if ( x e. B , C , 0 ) )
175	153	adantr 452	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( H ` x ) = if ( x e. U , C , 0 ) )
176	4	ad3antrrr 711	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> U = ( A u. B ) )
177	176	eleq2d 2471	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( x e. U <-> x e. ( A u. B ) ) )
178		biorf 395	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( -. x e. A -> ( x e. B <-> ( x e. A \/ x e. B ) ) )
179		elun 3448	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
180	178, 179	syl6rbbr 256	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( -. x e. A -> ( x e. ( A u. B ) <-> x e. B ) )
181	180	adantl 453	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( x e. ( A u. B ) <-> x e. B ) )
182	177, 181	bitrd 245	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( x e. U <-> x e. B ) )
183	182	ifbid 3717	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> if ( x e. U , C , 0 ) = if ( x e. B , C , 0 ) )
184	175, 183	eqtrd 2436	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( H ` x ) = if ( x e. B , C , 0 ) )
185	174, 184	breqtrrd 4198	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( g ` x ) <_ ( H ` x ) )
186	160, 162, 163, 173, 185	xrletrd 10708	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) /\ -. x e. A ) -> ( ( f ` x ) + ( g ` x ) ) <_ ( H ` x ) )
187	159, 186	pm2.61dan 767	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( ( f ` x ) + ( g ` x ) ) <_ ( H ` x ) )
188	69, 187	eqbrtrd 4192	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ x e. ( RR \ ( A i^i B ) ) ) -> ( ( f o F + g ) ` x ) <_ ( H ` x ) )
189	188	ex 424	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> ( x e. ( RR \ ( A i^i B ) ) -> ( ( f o F + g ) ` x ) <_ ( H ` x ) ) )
190	53, 189	ralrimi 2747	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> A. x e. ( RR \ ( A i^i B ) ) ( ( f o F + g ) ` x ) <_ ( H ` x ) )
191		nfv 1626	. . . . . . . . . . . . . . . . 17 |- F/ y ( ( f o F + g ) ` x ) <_ ( H ` x )
192		nfcv 2540	. . . . . . . . . . . . . . . . . 18 |- F/_ x ( ( f o F + g ) ` y )
193		nfcv 2540	. . . . . . . . . . . . . . . . . 18 |- F/_ x <_
194		nfmpt1 4258	. . . . . . . . . . . . . . . . . . . 20 |- F/_ x ( x e. RR |-> if ( x e. U , C , 0 ) )
195	8, 194	nfcxfr 2537	. . . . . . . . . . . . . . . . . . 19 |- F/_ x H
196		nfcv 2540	. . . . . . . . . . . . . . . . . . 19 |- F/_ x y
197	195, 196	nffv 5694	. . . . . . . . . . . . . . . . . 18 |- F/_ x ( H ` y )
198	192, 193, 197	nfbr 4216	. . . . . . . . . . . . . . . . 17 |- F/ x ( ( f o F + g ) ` y ) <_ ( H ` y )
199		fveq2 5687	. . . . . . . . . . . . . . . . . 18 |- ( x = y -> ( ( f o F + g ) ` x ) = ( ( f o F + g ) ` y ) )
200		fveq2 5687	. . . . . . . . . . . . . . . . . 18 |- ( x = y -> ( H ` x ) = ( H ` y ) )
201	199, 200	breq12d 4185	. . . . . . . . . . . . . . . . 17 |- ( x = y -> ( ( ( f o F + g ) ` x ) <_ ( H ` x ) <-> ( ( f o F + g ) ` y ) <_ ( H ` y ) ) )
202	191, 198, 201	cbvral 2888	. . . . . . . . . . . . . . . 16 |- ( A. x e. ( RR \ ( A i^i B ) ) ( ( f o F + g ) ` x ) <_ ( H ` x ) <-> A. y e. ( RR \ ( A i^i B ) ) ( ( f o F + g ) ` y ) <_ ( H ` y ) )
203	190, 202	sylib 189	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> A. y e. ( RR \ ( A i^i B ) ) ( ( f o F + g ) ` y ) <_ ( H ` y ) )
204	203	r19.21bi 2764	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) /\ y e. ( RR \ ( A i^i B ) ) ) -> ( ( f o F + g ) ` y ) <_ ( H ` y ) )
205	30, 31, 36, 37, 204	itg2uba 19588	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> ( S.1 ` ( f o F + g ) ) <_ ( S.2 ` H ) )
206	29, 205	eqbrtrrd 4194	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> ( ( S.1 ` f ) + ( S.1 ` g ) ) <_ ( S.2 ` H ) )
207	26	adantrr 698	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> ( S.1 ` f ) e. RR )
208		itg1cl 19530	. . . . . . . . . . . . . 14 |- ( g e. dom S.1 -> ( S.1 ` g ) e. RR )
209	28, 208	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> ( S.1 ` g ) e. RR )
210	23	adantr 452	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> ( S.2 ` H ) e. RR )
211	207, 209, 210	leaddsub2d 9584	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> ( ( ( S.1 ` f ) + ( S.1 ` g ) ) <_ ( S.2 ` H ) <-> ( S.1 ` g ) <_ ( ( S.2 ` H ) - ( S.1 ` f ) ) ) )
212	206, 211	mpbid 202	. . . . . . . . . . 11 |- ( ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) ) -> ( S.1 ` g ) <_ ( ( S.2 ` H ) - ( S.1 ` f ) ) )
213	212	anassrs 630	. . . . . . . . . 10 |- ( ( ( ph /\ ( f e. dom S.1 /\ f o R <_ F ) ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) -> ( S.1 ` g ) <_ ( ( S.2 ` H ) - ( S.1 ` f ) ) )
214	213	expr 599	. . . . . . . . 9 |- ( ( ( ph /\ ( f e. dom S.1 /\ f o R <_ F ) ) /\ g e. dom S.1 ) -> ( g o R <_ G -> ( S.1 ` g ) <_ ( ( S.2 ` H ) - ( S.1 ` f ) ) ) )
215	214	ralrimiva 2749	. . . . . . . 8 |- ( ( ph /\ ( f e. dom S.1 /\ f o R <_ F ) ) -> A. g e. dom S.1 ( g o R <_ G -> ( S.1 ` g ) <_ ( ( S.2 ` H ) - ( S.1 ` f ) ) ) )
216	97, 7	fmptd 5852	. . . . . . . . . 10 |- ( ph -> G : RR --> ( 0 [,] +oo ) )
217	216	adantr 452	. . . . . . . . 9 |- ( ( ph /\ ( f e. dom S.1 /\ f o R <_ F ) ) -> G : RR --> ( 0 [,] +oo ) )
218	24, 26	resubcld 9421	. . . . . . . . . 10 |- ( ( ph /\ ( f e. dom S.1 /\ f o R <_ F ) ) -> ( ( S.2 ` H ) - ( S.1 ` f ) ) e. RR )
219	218	rexrd 9090	. . . . . . . . 9 |- ( ( ph /\ ( f e. dom S.1 /\ f o R <_ F ) ) -> ( ( S.2 ` H ) - ( S.1 ` f ) ) e. RR* )
220		itg2leub 19579	. . . . . . . . 9 |- ( ( G : RR --> ( 0 [,] +oo ) /\ ( ( S.2 ` H ) - ( S.1 ` f ) ) e. RR* ) -> ( ( S.2 ` G ) <_ ( ( S.2 ` H ) - ( S.1 ` f ) ) <-> A. g e. dom S.1 ( g o R <_ G -> ( S.1 ` g ) <_ ( ( S.2 ` H ) - ( S.1 ` f ) ) ) ) )
221	217, 219, 220	syl2anc 643	. . . . . . . 8 |- ( ( ph /\ ( f e. dom S.1 /\ f o R <_ F ) ) -> ( ( S.2 ` G ) <_ ( ( S.2 ` H ) - ( S.1 ` f ) ) <-> A. g e. dom S.1 ( g o R <_ G -> ( S.1 ` g ) <_ ( ( S.2 ` H ) - ( S.1 ` f ) ) ) ) )
222	215, 221	mpbird 224	. . . . . . 7 |- ( ( ph /\ ( f e. dom S.1 /\ f o R <_ F ) ) -> ( S.2 ` G ) <_ ( ( S.2 ` H ) - ( S.1 ` f ) ) )
223	12, 24, 26, 222	lesubd 9586	. . . . . 6 |- ( ( ph /\ ( f e. dom S.1 /\ f o R <_ F ) ) -> ( S.1 ` f ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) )
224	223	expr 599	. . . . 5 |- ( ( ph /\ f e. dom S.1 ) -> ( f o R <_ F -> ( S.1 ` f ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) ) )
225	224	ralrimiva 2749	. . . 4 |- ( ph -> A. f e. dom S.1 ( f o R <_ F -> ( S.1 ` f ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) ) )
226	133, 6	fmptd 5852	. . . . 5 |- ( ph -> F : RR --> ( 0 [,] +oo ) )
227	23, 10	resubcld 9421	. . . . . 6 |- ( ph -> ( ( S.2 ` H ) - ( S.2 ` G ) ) e. RR )
228	227	rexrd 9090	. . . . 5 |- ( ph -> ( ( S.2 ` H ) - ( S.2 ` G ) ) e. RR* )
229		itg2leub 19579	. . . . 5 |- ( ( F : RR --> ( 0 [,] +oo ) /\ ( ( S.2 ` H ) - ( S.2 ` G ) ) e. RR* ) -> ( ( S.2 ` F ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) <-> A. f e. dom S.1 ( f o R <_ F -> ( S.1 ` f ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) ) ) )
230	226, 228, 229	syl2anc 643	. . . 4 |- ( ph -> ( ( S.2 ` F ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) <-> A. f e. dom S.1 ( f o R <_ F -> ( S.1 ` f ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) ) ) )
231	225, 230	mpbird 224	. . 3 |- ( ph -> ( S.2 ` F ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) )
232		leaddsub 9460	. . . 4 |- ( ( ( S.2 ` F ) e. RR /\ ( S.2 ` G ) e. RR /\ ( S.2 ` H ) e. RR ) -> ( ( ( S.2 ` F ) + ( S.2 ` G ) ) <_ ( S.2 ` H ) <-> ( S.2 ` F ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) ) )
233	9, 10, 23, 232	syl3anc 1184	. . 3 |- ( ph -> ( ( ( S.2 ` F ) + ( S.2 ` G ) ) <_ ( S.2 ` H ) <-> ( S.2 ` F ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) ) )
234	231, 233	mpbird 224	. 2 |- ( ph -> ( ( S.2 ` F ) + ( S.2 ` G ) ) <_ ( S.2 ` H ) )
235		itg2cl 19577	. . . 4 |- ( H : RR --> ( 0 [,] +oo ) -> ( S.2 ` H ) e. RR* )
236	20, 235	syl 16	. . 3 |- ( ph -> ( S.2 ` H ) e. RR* )
237	21	rexrd 9090	. . 3 |- ( ph -> ( ( S.2 ` F ) + ( S.2 ` G ) ) e. RR* )
238		xrletri3 10701	. . 3 |- ( ( ( S.2 ` H ) e. RR* /\ ( ( S.2 ` F ) + ( S.2 ` G ) ) e. RR* ) -> ( ( S.2 ` H ) = ( ( S.2 ` F ) + ( S.2 ` G ) ) <-> ( ( S.2 ` H ) <_ ( ( S.2 ` F ) + ( S.2 ` G ) ) /\ ( ( S.2 ` F ) + ( S.2 ` G ) ) <_ ( S.2 ` H ) ) ) )
239	236, 237, 238	syl2anc 643	. 2 |- ( ph -> ( ( S.2 ` H ) = ( ( S.2 ` F ) + ( S.2 ` G ) ) <-> ( ( S.2 ` H ) <_ ( ( S.2 ` F ) + ( S.2 ` G ) ) /\ ( ( S.2 ` F ) + ( S.2 ` G ) ) <_ ( S.2 ` H ) ) ) )
240	11, 234, 239	mpbir2and 889	1 |- ( ph -> ( S.2 ` H ) = ( ( S.2 ` F ) + ( S.2 ` G ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   \/ wo 358   /\ wa 359   = wceq 1649   e. wcel 1721   A.wral 2666   _Vcvv 2916   \ cdif 3277   u. cun 3278   i^i cin 3279   C_ wss 3280   ifcif 3699   class class class wbr 4172   e. cmpt 4226   dom cdm 4837   Fn wfn 5408   -->wf 5409   ` cfv 5413  (class class class)co 6040   o Fcof 6262   o Rcofr 6263   RRcr 8945   0cc0 8946   + caddc 8949   +oocpnf 9073   RR*cxr 9075   <_ cle 9077   - cmin 9247   [,]cicc 10875   vol *covol 19312   volcvol 19313   S.1citg1 19460   S.2citg2 19461

This theorem is referenced by:  itg2cnlem2  19607  itgsplit  19680

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024  ax-addf 9025

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-disj 4143  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-of 6264  df-ofr 6265  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-2o 6684  df-oadd 6687  df-er 6864  df-map 6979  df-pm 6980  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-fi 7374  df-sup 7404  df-oi 7435  df-card 7782  df-cda 8004  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-n0 10178  df-z 10239  df-uz 10445  df-q 10531  df-rp 10569  df-xneg 10666  df-xadd 10667  df-xmul 10668  df-ioo 10876  df-ico 10878  df-icc 10879  df-fz 11000  df-fzo 11091  df-fl 11157  df-seq 11279  df-exp 11338  df-hash 11574  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-clim 12237  df-sum 12435  df-rest 13605  df-topgen 13622  df-psmet 16649  df-xmet 16650  df-met 16651  df-bl 16652  df-mopn 16653  df-top 16918  df-bases 16920  df-topon 16921  df-cmp 17404  df-ovol 19314  df-vol 19315  df-mbf 19465  df-itg1 19466  df-itg2 19467