Theorem itg2split 19644

Description: The S.2 integral splits under an almost disjoint union. (The proof avoids the use of itg2add 19654 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 19643	. 2 |- ( ph -> ( S.2 ` H ) <_ ( ( S.2 ` F ) + ( S.2 ` G ) ) )
12	10	adantr 453	. . . . . . 7 |- ( ( ph /\ ( f e. dom S.1 /\ f o R <_ F ) ) -> ( S.2 ` G ) e. RR )
13	5	adantlr 697	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR ) /\ x e. U ) -> C e. ( 0 [,] +oo ) )
14		0xr 9136	. . . . . . . . . . . . 13 |- 0 e. RR*
15		0le0 10086	. . . . . . . . . . . . 13 |- 0 <_ 0
16		elxrge0 11013	. . . . . . . . . . . . 13 |- ( 0 e. ( 0 [,] +oo ) <-> ( 0 e. RR* /\ 0 <_ 0 ) )
17	14, 15, 16	mpbir2an 888	. . . . . . . . . . . 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 3768	. . . . . . . . . 10 |- ( ( ph /\ x e. RR ) -> if ( x e. U , C , 0 ) e. ( 0 [,] +oo ) )
20	19, 8	fmptd 5896	. . . . . . . . 9 |- ( ph -> H : RR --> ( 0 [,] +oo ) )
21	9, 10	readdcld 9120	. . . . . . . . 9 |- ( ph -> ( ( S.2 ` F ) + ( S.2 ` G ) ) e. RR )
22		itg2lecl 19633	. . . . . . . . 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 1185	. . . . . . . 8 |- ( ph -> ( S.2 ` H ) e. RR )
24	23	adantr 453	. . . . . . 7 |- ( ( ph /\ ( f e. dom S.1 /\ f o R <_ F ) ) -> ( S.2 ` H ) e. RR )
25		itg1cl 19580	. . . . . . . 8 |- ( f e. dom S.1 -> ( S.1 ` f ) e. RR )
26	25	ad2antrl 710	. . . . . . 7 |- ( ( ph /\ ( f e. dom S.1 /\ f o R <_ F ) ) -> ( S.1 ` f ) e. RR )
27		simprll 740	. . . . . . . . . . . . . 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 742	. . . . . . . . . . . . . 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 19596	. . . . . . . . . . . . 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 453	. . . . . . . . . . . . . 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 19590	. . . . . . . . . . . . . 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 3563	. . . . . . . . . . . . . . . 16 |- ( A i^i B ) C_ A
33		mblss 19432	. . . . . . . . . . . . . . . . 17 |- ( A e. dom vol -> A C_ RR )
34	1, 33	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> A C_ RR )
35	32, 34	syl5ss 3361	. . . . . . . . . . . . . . 15 |- ( ph -> ( A i^i B ) C_ RR )
36	35	adantr 453	. . . . . . . . . . . . . 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 453	. . . . . . . . . . . . . 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 1630	. . . . . . . . . . . . . . . . . 18 |- F/ x ph
39		nfv 1630	. . . . . . . . . . . . . . . . . . . 20 |- F/ x f e. dom S.1
40		nfcv 2574	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ x f
41		nfcv 2574	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ x o R <_
42		nfmpt1 4301	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ x ( x e. RR |-> if ( x e. A , C , 0 ) )
43	6, 42	nfcxfr 2571	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ x F
44	40, 41, 43	nfbr 4259	. . . . . . . . . . . . . . . . . . . 20 |- F/ x f o R <_ F
45	39, 44	nfan 1847	. . . . . . . . . . . . . . . . . . 19 |- F/ x ( f e. dom S.1 /\ f o R <_ F )
46		nfv 1630	. . . . . . . . . . . . . . . . . . . 20 |- F/ x g e. dom S.1
47		nfcv 2574	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ x g
48		nfmpt1 4301	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ x ( x e. RR |-> if ( x e. B , C , 0 ) )
49	7, 48	nfcxfr 2571	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ x G
50	47, 41, 49	nfbr 4259	. . . . . . . . . . . . . . . . . . . 20 |- F/ x g o R <_ G
51	46, 50	nfan 1847	. . . . . . . . . . . . . . . . . . 19 |- F/ x ( g e. dom S.1 /\ g o R <_ G )
52	45, 51	nfan 1847	. . . . . . . . . . . . . . . . . 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 1847	. . . . . . . . . . . . . . . . 17 |- F/ x ( ph /\ ( ( f e. dom S.1 /\ f o R <_ F ) /\ ( g e. dom S.1 /\ g o R <_ G ) ) )
54		eldifi 3471	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( RR \ ( A i^i B ) ) -> x e. RR )
55		i1ff 19571	. . . . . . . . . . . . . . . . . . . . . . 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 5594	. . . . . . . . . . . . . . . . . . . . . 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 19571	. . . . . . . . . . . . . . . . . . . . . . 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 5594	. . . . . . . . . . . . . . . . . . . . . 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 9086	. . . . . . . . . . . . . . . . . . . . . 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 3552	. . . . . . . . . . . . . . . . . . . . 21 |- ( RR i^i RR ) = RR
66		eqidd 2439	. . . . . . . . . . . . . . . . . . . . 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 2439	. . . . . . . . . . . . . . . . . . . . 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 6317	. . . . . . . . . . . . . . . . . . . 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 462	. . . . . . . . . . . . . . . . . . 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 5871	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f : RR --> RR /\ x e. RR ) -> ( f ` x ) e. RR )
71	56, 54, 70	syl2an 465	. . . . . . . . . . . . . . . . . . . . . . . 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 5871	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g : RR --> RR /\ x e. RR ) -> ( g ` x ) e. RR )
73	60, 54, 72	syl2an 465	. . . . . . . . . . . . . . . . . . . . . . . 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 9120	. . . . . . . . . . . . . . . . . . . . . . 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 9139	. . . . . . . . . . . . . . . . . . . . . 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 453	. . . . . . . . . . . . . . . . . . . . 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 453	. . . . . . . . . . . . . . . . . . . . . 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 9139	. . . . . . . . . . . . . . . . . . . . 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 10998	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 0 [,] +oo ) C_ RR*
80		ffvelrn 5871	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( H : RR --> ( 0 [,] +oo ) /\ x e. RR ) -> ( H ` x ) e. ( 0 [,] +oo ) )
81	30, 54, 80	syl2an 465	. . . . . . . . . . . . . . . . . . . . . . 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 3348	. . . . . . . . . . . . . . . . . . . . . 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 453	. . . . . . . . . . . . . . . . . . . . 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 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 ) -> ( g ` x ) e. RR )
85		0re 9096	. . . . . . . . . . . . . . . . . . . . . . . 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 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( g ` x ) e. _V
90	89	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ g Fn RR ) /\ x e. RR ) -> ( g ` x ) e. _V )
91		ssun2 3513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- B C_ ( A u. B )
92	91, 4	syl5sseqr 3399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ph -> B C_ U )
93	92	sselda 3350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ph /\ x e. B ) -> x e. U )
94	93	adantlr 697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ x e. RR ) /\ x e. B ) -> x e. U )
95	94, 13	syldan 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ x e. RR ) -> if ( x e. B , C , 0 ) e. ( 0 [,] +oo ) )
98	97	adantlr 697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ g Fn RR ) /\ x e. RR ) -> if ( x e. B , C , 0 ) e. ( 0 [,] +oo ) )
99		simpr 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ g Fn RR ) -> g Fn RR )
100		dffn5 5775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( g Fn RR <-> g = ( x e. RR |-> ( g ` x ) ) )
101	99, 100	sylib 190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 203	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2806	. . . . . . . . . . . . . . . . . . . . . . . . . 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 462	. . . . . . . . . . . . . . . . . . . . . . . . 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 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 ) -> ( g ` x ) <_ if ( x e. B , C , 0 ) )
109		eldifn 3472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. ( RR \ ( A i^i B ) ) -> -. x e. ( A i^i B ) )
110	109	adantl 454	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3532	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
112	110, 111	sylnib 297	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 413	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( x e. A -> -. x e. B ) <-> -. ( x e. A /\ x e. B ) )
114	112, 113	sylibr 205	. . . . . . . . . . . . . . . . . . . . . . . . . 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 420	. . . . . . . . . . . . . . . . . . . . . . . . 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 3748	. . . . . . . . . . . . . . . . . . . . . . . . 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 4239	. . . . . . . . . . . . . . . . . . . . . . 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 9646	. . . . . . . . . . . . . . . . . . . . . 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 9119	. . . . . . . . . . . . . . . . . . . . . . 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 9271	. . . . . . . . . . . . . . . . . . . . . 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 4239	. . . . . . . . . . . . . . . . . . . . 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 741	. . . . . . . . . . . . . . . . . . . . . . . . . 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 5745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( f ` x ) e. _V
126	125	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ f Fn RR ) /\ x e. RR ) -> ( f ` x ) e. _V )
127		ssun1 3512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- A C_ ( A u. B )
128	127, 4	syl5sseqr 3399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ph -> A C_ U )
129	128	sselda 3350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ x e. A ) -> x e. U )
130	129	adantlr 697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ph /\ x e. RR ) /\ x e. A ) -> x e. U )
131	130, 13	syldan 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ x e. RR ) -> if ( x e. A , C , 0 ) e. ( 0 [,] +oo ) )
134	133	adantlr 697	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ f Fn RR ) /\ x e. RR ) -> if ( x e. A , C , 0 ) e. ( 0 [,] +oo ) )
135		simpr 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ f Fn RR ) -> f Fn RR )
136		dffn5 5775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( f Fn RR <-> f = ( x e. RR |-> ( f ` x ) ) )
137	135, 136	sylib 190	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6326	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 458	. . . . . . . . . . . . . . . . . . . . . . . . . 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 203	. . . . . . . . . . . . . . . . . . . . . . . . 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 2806	. . . . . . . . . . . . . . . . . . . . . . . 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 462	. . . . . . . . . . . . . . . . . . . . . . 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 453	. . . . . . . . . . . . . . . . . . . . . 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 708	. . . . . . . . . . . . . . . . . . . . . . . . 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 3350	. . . . . . . . . . . . . . . . . . . . . . . 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 3747	. . . . . . . . . . . . . . . . . . . . . . . 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 449	. . . . . . . . . . . . . . . . . . . . . . . . . 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 697	. . . . . . . . . . . . . . . . . . . . . . . . . 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 5815	. . . . . . . . . . . . . . . . . . . . . . . . . 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 644	. . . . . . . . . . . . . . . . . . . . . . . . 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 462	. . . . . . . . . . . . . . . . . . . . . . . 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 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 ) -> ( H ` x ) = if ( x e. U , C , 0 ) )
155		iftrue 3747	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x e. A -> if ( x e. A , C , 0 ) = C )
156	155	adantl 454	. . . . . . . . . . . . . . . . . . . . . . 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 2480	. . . . . . . . . . . . . . . . . . . . . 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 4241	. . . . . . . . . . . . . . . . . . . . 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 10757	. . . . . . . . . . . . . . . . . . . 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 453	. . . . . . . . . . . . . . . . . . . . 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 453	. . . . . . . . . . . . . . . . . . . . . 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 9139	. . . . . . . . . . . . . . . . . . . . 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 453	. . . . . . . . . . . . . . . . . . . . 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 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 ) -> ( 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 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 ) -> ( f ` x ) <_ if ( x e. A , C , 0 ) )
167		iffalse 3748	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( -. x e. A -> if ( x e. A , C , 0 ) = 0 )
168	167	adantl 454	. . . . . . . . . . . . . . . . . . . . . . . 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 4239	. . . . . . . . . . . . . . . . . . . . . . 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 9645	. . . . . . . . . . . . . . . . . . . . . 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 9119	. . . . . . . . . . . . . . . . . . . . . . 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 9272	. . . . . . . . . . . . . . . . . . . . . 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 4239	. . . . . . . . . . . . . . . . . . . . 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 453	. . . . . . . . . . . . . . . . . . . . . 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 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 ) -> ( H ` x ) = if ( x e. U , C , 0 ) )
176	4	ad3antrrr 712	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2505	. . . . . . . . . . . . . . . . . . . . . . . . 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 396	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( -. x e. A -> ( x e. B <-> ( x e. A \/ x e. B ) ) )
179		elun 3490	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
180	178, 179	syl6rbbr 257	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( -. x e. A -> ( x e. ( A u. B ) <-> x e. B ) )
181	180	adantl 454	. . . . . . . . . . . . . . . . . . . . . . . . 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 246	. . . . . . . . . . . . . . . . . . . . . . . 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 3759	. . . . . . . . . . . . . . . . . . . . . . 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 2470	. . . . . . . . . . . . . . . . . . . . . 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 4241	. . . . . . . . . . . . . . . . . . . . 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 10757	. . . . . . . . . . . . . . . . . . . 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 768	. . . . . . . . . . . . . . . . . . 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 4235	. . . . . . . . . . . . . . . . . 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 425	. . . . . . . . . . . . . . . . 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 2789	. . . . . . . . . . . . . . . 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 1630	. . . . . . . . . . . . . . . . 17 |- F/ y ( ( f o F + g ) ` x ) <_ ( H ` x )
192		nfcv 2574	. . . . . . . . . . . . . . . . . 18 |- F/_ x ( ( f o F + g ) ` y )
193		nfcv 2574	. . . . . . . . . . . . . . . . . 18 |- F/_ x <_
194		nfmpt1 4301	. . . . . . . . . . . . . . . . . . . 20 |- F/_ x ( x e. RR |-> if ( x e. U , C , 0 ) )
195	8, 194	nfcxfr 2571	. . . . . . . . . . . . . . . . . . 19 |- F/_ x H
196		nfcv 2574	. . . . . . . . . . . . . . . . . . 19 |- F/_ x y
197	195, 196	nffv 5738	. . . . . . . . . . . . . . . . . 18 |- F/_ x ( H ` y )
198	192, 193, 197	nfbr 4259	. . . . . . . . . . . . . . . . 17 |- F/ x ( ( f o F + g ) ` y ) <_ ( H ` y )
199		fveq2 5731	. . . . . . . . . . . . . . . . . 18 |- ( x = y -> ( ( f o F + g ) ` x ) = ( ( f o F + g ) ` y ) )
200		fveq2 5731	. . . . . . . . . . . . . . . . . 18 |- ( x = y -> ( H ` x ) = ( H ` y ) )
201	199, 200	breq12d 4228	. . . . . . . . . . . . . . . . 17 |- ( x = y -> ( ( ( f o F + g ) ` x ) <_ ( H ` x ) <-> ( ( f o F + g ) ` y ) <_ ( H ` y ) ) )
202	191, 198, 201	cbvral 2930	. . . . . . . . . . . . . . . 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 190	. . . . . . . . . . . . . . 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 2806	. . . . . . . . . . . . . 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 19638	. . . . . . . . . . . . 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 4237	. . . . . . . . . . . 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 699	. . . . . . . . . . . . 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 19580	. . . . . . . . . . . . . 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 453	. . . . . . . . . . . . 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 9633	. . . . . . . . . . . 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 203	. . . . . . . . . . 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 631	. . . . . . . . . 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 600	. . . . . . . . 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 2791	. . . . . . . 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 5896	. . . . . . . . . 10 |- ( ph -> G : RR --> ( 0 [,] +oo ) )
217	216	adantr 453	. . . . . . . . 9 |- ( ( ph /\ ( f e. dom S.1 /\ f o R <_ F ) ) -> G : RR --> ( 0 [,] +oo ) )
218	24, 26	resubcld 9470	. . . . . . . . . 10 |- ( ( ph /\ ( f e. dom S.1 /\ f o R <_ F ) ) -> ( ( S.2 ` H ) - ( S.1 ` f ) ) e. RR )
219	218	rexrd 9139	. . . . . . . . 9 |- ( ( ph /\ ( f e. dom S.1 /\ f o R <_ F ) ) -> ( ( S.2 ` H ) - ( S.1 ` f ) ) e. RR* )
220		itg2leub 19629	. . . . . . . . 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 644	. . . . . . . 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 225	. . . . . . 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 9635	. . . . . 6 |- ( ( ph /\ ( f e. dom S.1 /\ f o R <_ F ) ) -> ( S.1 ` f ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) )
224	223	expr 600	. . . . 5 |- ( ( ph /\ f e. dom S.1 ) -> ( f o R <_ F -> ( S.1 ` f ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) ) )
225	224	ralrimiva 2791	. . . 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 5896	. . . . 5 |- ( ph -> F : RR --> ( 0 [,] +oo ) )
227	23, 10	resubcld 9470	. . . . . 6 |- ( ph -> ( ( S.2 ` H ) - ( S.2 ` G ) ) e. RR )
228	227	rexrd 9139	. . . . 5 |- ( ph -> ( ( S.2 ` H ) - ( S.2 ` G ) ) e. RR* )
229		itg2leub 19629	. . . . 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 644	. . . 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 225	. . 3 |- ( ph -> ( S.2 ` F ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) )
232		leaddsub 9509	. . . 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 1185	. . 3 |- ( ph -> ( ( ( S.2 ` F ) + ( S.2 ` G ) ) <_ ( S.2 ` H ) <-> ( S.2 ` F ) <_ ( ( S.2 ` H ) - ( S.2 ` G ) ) ) )
234	231, 233	mpbird 225	. 2 |- ( ph -> ( ( S.2 ` F ) + ( S.2 ` G ) ) <_ ( S.2 ` H ) )
235		itg2cl 19627	. . . 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 9139	. . 3 |- ( ph -> ( ( S.2 ` F ) + ( S.2 ` G ) ) e. RR* )
238		xrletri3 10750	. . 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 644	. 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 890	1 |- ( ph -> ( S.2 ` H ) = ( ( S.2 ` F ) + ( S.2 ` G ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 178   \/ wo 359   /\ wa 360   = wceq 1653   e. wcel 1726   A.wral 2707   _Vcvv 2958   \ cdif 3319   u. cun 3320   i^i cin 3321   C_ wss 3322   ifcif 3741   class class class wbr 4215   e. cmpt 4269   dom cdm 4881   Fn wfn 5452   -->wf 5453   ` cfv 5457  (class class class)co 6084   o Fcof 6306   o Rcofr 6307   RRcr 8994   0cc0 8995   + caddc 8998   +oocpnf 9122   RR*cxr 9124   <_ cle 9126   - cmin 9296   [,]cicc 10924   vol *covol 19364   volcvol 19365   S.1citg1 19512   S.2citg2 19513

This theorem is referenced by:  itg2cnlem2  19657  itgsplit  19730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4323  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704  ax-inf2 7599  ax-cnex 9051  ax-resscn 9052  ax-1cn 9053  ax-icn 9054  ax-addcl 9055  ax-addrcl 9056  ax-mulcl 9057  ax-mulrcl 9058  ax-mulcom 9059  ax-addass 9060  ax-mulass 9061  ax-distr 9062  ax-i2m1 9063  ax-1ne0 9064  ax-1rid 9065  ax-rnegex 9066  ax-rrecex 9067  ax-cnre 9068  ax-pre-lttri 9069  ax-pre-lttrn 9070  ax-pre-ltadd 9071  ax-pre-mulgt0 9072  ax-pre-sup 9073  ax-addf 9074

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-disj 4186  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-se 4545  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-om 4849  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-isom 5466  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-of 6308  df-ofr 6309  df-1st 6352  df-2nd 6353  df-riota 6552  df-recs 6636  df-rdg 6671  df-1o 6727  df-2o 6728  df-oadd 6731  df-er 6908  df-map 7023  df-pm 7024  df-en 7113  df-dom 7114  df-sdom 7115  df-fin 7116  df-fi 7419  df-sup 7449  df-oi 7482  df-card 7831  df-cda 8053  df-pnf 9127  df-mnf 9128  df-xr 9129  df-ltxr 9130  df-le 9131  df-sub 9298  df-neg 9299  df-div 9683  df-nn 10006  df-2 10063  df-3 10064  df-n0 10227  df-z 10288  df-uz 10494  df-q 10580  df-rp 10618  df-xneg 10715  df-xadd 10716  df-xmul 10717  df-ioo 10925  df-ico 10927  df-icc 10928  df-fz 11049  df-fzo 11141  df-fl 11207  df-seq 11329  df-exp 11388  df-hash 11624  df-cj 11909  df-re 11910  df-im 11911  df-sqr 12045  df-abs 12046  df-clim 12287  df-sum 12485  df-rest 13655  df-topgen 13672  df-psmet 16699  df-xmet 16700  df-met 16701  df-bl 16702  df-mopn 16703  df-top 16968  df-bases 16970  df-topon 16971  df-cmp 17455  df-ovol 19366  df-vol 19367  df-mbf 19516  df-itg1 19517  df-itg2 19518