Theorem i1fadd 22639

Description: The sum of two simple functions is a simple function. (Contributed by Mario Carneiro, 18-Jun-2014.)

Hypotheses

Ref	Expression
i1fadd.1	|- ( ph -> F e. dom S.1 )
i1fadd.2	|- ( ph -> G e. dom S.1 )

Assertion

Ref	Expression
i1fadd	|- ( ph -> ( F oF + G ) e. dom S.1 )

Proof of Theorem i1fadd

Dummy variables y z w v x u are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		readdcl 9622	. . . 4 |- ( ( x e. RR /\ y e. RR ) -> ( x + y ) e. RR )
2	1	adantl 467	. . 3 |- ( ( ph /\ ( x e. RR /\ y e. RR ) ) -> ( x + y ) e. RR )
3		i1fadd.1	. . . 4 |- ( ph -> F e. dom S.1 )
4		i1ff 22620	. . . 4 |- ( F e. dom S.1 -> F : RR --> RR )
5	3, 4	syl 17	. . 3 |- ( ph -> F : RR --> RR )
6		i1fadd.2	. . . 4 |- ( ph -> G e. dom S.1 )
7		i1ff 22620	. . . 4 |- ( G e. dom S.1 -> G : RR --> RR )
8	6, 7	syl 17	. . 3 |- ( ph -> G : RR --> RR )
9		reex 9630	. . . 4 |- RR e. _V
10	9	a1i 11	. . 3 |- ( ph -> RR e. _V )
11		inidm 3671	. . 3 |- ( RR i^i RR ) = RR
12	2, 5, 8, 10, 10, 11	off 6556	. 2 |- ( ph -> ( F oF + G ) : RR --> RR )
13		i1frn 22621	. . . . . 6 |- ( F e. dom S.1 -> ran F e. Fin )
14	3, 13	syl 17	. . . . 5 |- ( ph -> ran F e. Fin )
15		i1frn 22621	. . . . . 6 |- ( G e. dom S.1 -> ran G e. Fin )
16	6, 15	syl 17	. . . . 5 |- ( ph -> ran G e. Fin )
17		xpfi 7844	. . . . 5 |- ( ( ran F e. Fin /\ ran G e. Fin ) -> ( ran F X. ran G ) e. Fin )
18	14, 16, 17	syl2anc 665	. . . 4 |- ( ph -> ( ran F X. ran G ) e. Fin )
19		eqid 2422	. . . . . 6 |- ( u e. ran F , v e. ran G |-> ( u + v ) ) = ( u e. ran F , v e. ran G |-> ( u + v ) )
20		ovex 6329	. . . . . 6 |- ( u + v ) e. _V
21	19, 20	fnmpt2i 6872	. . . . 5 |- ( u e. ran F , v e. ran G |-> ( u + v ) ) Fn ( ran F X. ran G )
22		dffn4 5812	. . . . 5 |- ( ( u e. ran F , v e. ran G |-> ( u + v ) ) Fn ( ran F X. ran G ) <-> ( u e. ran F , v e. ran G |-> ( u + v ) ) : ( ran F X. ran G ) -onto-> ran ( u e. ran F , v e. ran G |-> ( u + v ) ) )
23	21, 22	mpbi 211	. . . 4 |- ( u e. ran F , v e. ran G |-> ( u + v ) ) : ( ran F X. ran G ) -onto-> ran ( u e. ran F , v e. ran G |-> ( u + v ) )
24		fofi 7862	. . . 4 |- ( ( ( ran F X. ran G ) e. Fin /\ ( u e. ran F , v e. ran G |-> ( u + v ) ) : ( ran F X. ran G ) -onto-> ran ( u e. ran F , v e. ran G |-> ( u + v ) ) ) -> ran ( u e. ran F , v e. ran G |-> ( u + v ) ) e. Fin )
25	18, 23, 24	sylancl 666	. . 3 |- ( ph -> ran ( u e. ran F , v e. ran G |-> ( u + v ) ) e. Fin )
26		eqid 2422	. . . . . . . . 9 |- ( x + y ) = ( x + y )
27		rspceov 6340	. . . . . . . . 9 |- ( ( x e. ran F /\ y e. ran G /\ ( x + y ) = ( x + y ) ) -> E. u e. ran F E. v e. ran G ( x + y ) = ( u + v ) )
28	26, 27	mp3an3 1349	. . . . . . . 8 |- ( ( x e. ran F /\ y e. ran G ) -> E. u e. ran F E. v e. ran G ( x + y ) = ( u + v ) )
29		ovex 6329	. . . . . . . . 9 |- ( x + y ) e. _V
30		eqeq1 2426	. . . . . . . . . 10 |- ( w = ( x + y ) -> ( w = ( u + v ) <-> ( x + y ) = ( u + v ) ) )
31	30	2rexbidv 2946	. . . . . . . . 9 |- ( w = ( x + y ) -> ( E. u e. ran F E. v e. ran G w = ( u + v ) <-> E. u e. ran F E. v e. ran G ( x + y ) = ( u + v ) ) )
32	29, 31	elab 3218	. . . . . . . 8 |- ( ( x + y ) e. { w | E. u e. ran F E. v e. ran G w = ( u + v ) } <-> E. u e. ran F E. v e. ran G ( x + y ) = ( u + v ) )
33	28, 32	sylibr 215	. . . . . . 7 |- ( ( x e. ran F /\ y e. ran G ) -> ( x + y ) e. { w | E. u e. ran F E. v e. ran G w = ( u + v ) } )
34	33	adantl 467	. . . . . 6 |- ( ( ph /\ ( x e. ran F /\ y e. ran G ) ) -> ( x + y ) e. { w | E. u e. ran F E. v e. ran G w = ( u + v ) } )
35		ffn 5742	. . . . . . . 8 |- ( F : RR --> RR -> F Fn RR )
36	5, 35	syl 17	. . . . . . 7 |- ( ph -> F Fn RR )
37		dffn3 5749	. . . . . . 7 |- ( F Fn RR <-> F : RR --> ran F )
38	36, 37	sylib 199	. . . . . 6 |- ( ph -> F : RR --> ran F )
39		ffn 5742	. . . . . . . 8 |- ( G : RR --> RR -> G Fn RR )
40	8, 39	syl 17	. . . . . . 7 |- ( ph -> G Fn RR )
41		dffn3 5749	. . . . . . 7 |- ( G Fn RR <-> G : RR --> ran G )
42	40, 41	sylib 199	. . . . . 6 |- ( ph -> G : RR --> ran G )
43	34, 38, 42, 10, 10, 11	off 6556	. . . . 5 |- ( ph -> ( F oF + G ) : RR --> { w | E. u e. ran F E. v e. ran G w = ( u + v ) } )
44		frn 5748	. . . . 5 |- ( ( F oF + G ) : RR --> { w | E. u e. ran F E. v e. ran G w = ( u + v ) } -> ran ( F oF + G ) C_ { w | E. u e. ran F E. v e. ran G w = ( u + v ) } )
45	43, 44	syl 17	. . . 4 |- ( ph -> ran ( F oF + G ) C_ { w | E. u e. ran F E. v e. ran G w = ( u + v ) } )
46	19	rnmpt2 6416	. . . 4 |- ran ( u e. ran F , v e. ran G |-> ( u + v ) ) = { w | E. u e. ran F E. v e. ran G w = ( u + v ) }
47	45, 46	syl6sseqr 3511	. . 3 |- ( ph -> ran ( F oF + G ) C_ ran ( u e. ran F , v e. ran G |-> ( u + v ) ) )
48		ssfi 7794	. . 3 |- ( ( ran ( u e. ran F , v e. ran G |-> ( u + v ) ) e. Fin /\ ran ( F oF + G ) C_ ran ( u e. ran F , v e. ran G |-> ( u + v ) ) ) -> ran ( F oF + G ) e. Fin )
49	25, 47, 48	syl2anc 665	. 2 |- ( ph -> ran ( F oF + G ) e. Fin )
50		frn 5748	. . . . . . . 8 |- ( ( F oF + G ) : RR --> RR -> ran ( F oF + G ) C_ RR )
51	12, 50	syl 17	. . . . . . 7 |- ( ph -> ran ( F oF + G ) C_ RR )
52	51	ssdifssd 3603	. . . . . 6 |- ( ph -> ( ran ( F oF + G ) \ { 0 } ) C_ RR )
53	52	sselda 3464	. . . . 5 |- ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> y e. RR )
54	53	recnd 9669	. . . 4 |- ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> y e. CC )
55	3, 6	i1faddlem 22637	. . . 4 |- ( ( ph /\ y e. CC ) -> ( `' ( F oF + G ) " { y } ) = U_ z e. ran G ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) )
56	54, 55	syldan 472	. . 3 |- ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ( `' ( F oF + G ) " { y } ) = U_ z e. ran G ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) )
57	16	adantr 466	. . . 4 |- ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ran G e. Fin )
58	3	ad2antrr 730	. . . . . . . 8 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> F e. dom S.1 )
59		i1fmbf 22619	. . . . . . . 8 |- ( F e. dom S.1 -> F e. MblFn )
60	58, 59	syl 17	. . . . . . 7 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> F e. MblFn )
61	5	ad2antrr 730	. . . . . . 7 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> F : RR --> RR )
62	12	ad2antrr 730	. . . . . . . . . 10 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ( F oF + G ) : RR --> RR )
63	62, 50	syl 17	. . . . . . . . 9 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ran ( F oF + G ) C_ RR )
64		eldifi 3587	. . . . . . . . . 10 |- ( y e. ( ran ( F oF + G ) \ { 0 } ) -> y e. ran ( F oF + G ) )
65	64	ad2antlr 731	. . . . . . . . 9 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> y e. ran ( F oF + G ) )
66	63, 65	sseldd 3465	. . . . . . . 8 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> y e. RR )
67	8	adantr 466	. . . . . . . . . 10 |- ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> G : RR --> RR )
68		frn 5748	. . . . . . . . . 10 |- ( G : RR --> RR -> ran G C_ RR )
69	67, 68	syl 17	. . . . . . . . 9 |- ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ran G C_ RR )
70	69	sselda 3464	. . . . . . . 8 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> z e. RR )
71	66, 70	resubcld 10047	. . . . . . 7 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ( y - z ) e. RR )
72		mbfimasn 22576	. . . . . . 7 |- ( ( F e. MblFn /\ F : RR --> RR /\ ( y - z ) e. RR ) -> ( `' F " { ( y - z ) } ) e. dom vol )
73	60, 61, 71, 72	syl3anc 1264	. . . . . 6 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ( `' F " { ( y - z ) } ) e. dom vol )
74	6	ad2antrr 730	. . . . . . . 8 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> G e. dom S.1 )
75		i1fmbf 22619	. . . . . . . 8 |- ( G e. dom S.1 -> G e. MblFn )
76	74, 75	syl 17	. . . . . . 7 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> G e. MblFn )
77	8	ad2antrr 730	. . . . . . 7 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> G : RR --> RR )
78		mbfimasn 22576	. . . . . . 7 |- ( ( G e. MblFn /\ G : RR --> RR /\ z e. RR ) -> ( `' G " { z } ) e. dom vol )
79	76, 77, 70, 78	syl3anc 1264	. . . . . 6 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ( `' G " { z } ) e. dom vol )
80		inmbl 22481	. . . . . 6 |- ( ( ( `' F " { ( y - z ) } ) e. dom vol /\ ( `' G " { z } ) e. dom vol ) -> ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) e. dom vol )
81	73, 79, 80	syl2anc 665	. . . . 5 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) e. dom vol )
82	81	ralrimiva 2839	. . . 4 |- ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> A. z e. ran G ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) e. dom vol )
83		finiunmbl 22483	. . . 4 |- ( ( ran G e. Fin /\ A. z e. ran G ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) e. dom vol ) -> U_ z e. ran G ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) e. dom vol )
84	57, 82, 83	syl2anc 665	. . 3 |- ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> U_ z e. ran G ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) e. dom vol )
85	56, 84	eqeltrd 2510	. 2 |- ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ( `' ( F oF + G ) " { y } ) e. dom vol )
86		mblvol 22470	. . . 4 |- ( ( `' ( F oF + G ) " { y } ) e. dom vol -> ( vol ` ( `' ( F oF + G ) " { y } ) ) = ( vol* ` ( `' ( F oF + G ) " { y } ) ) )
87	85, 86	syl 17	. . 3 |- ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ( vol ` ( `' ( F oF + G ) " { y } ) ) = ( vol* ` ( `' ( F oF + G ) " { y } ) ) )
88		mblss 22471	. . . . 5 |- ( ( `' ( F oF + G ) " { y } ) e. dom vol -> ( `' ( F oF + G ) " { y } ) C_ RR )
89	85, 88	syl 17	. . . 4 |- ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ( `' ( F oF + G ) " { y } ) C_ RR )
90		inss1 3682	. . . . . . . . 9 |- ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) C_ ( `' F " { ( y - z ) } )
91	90	a1i 11	. . . . . . . 8 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) C_ ( `' F " { ( y - z ) } ) )
92	73	adantrr 721	. . . . . . . . 9 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( `' F " { ( y - z ) } ) e. dom vol )
93		mblss 22471	. . . . . . . . 9 |- ( ( `' F " { ( y - z ) } ) e. dom vol -> ( `' F " { ( y - z ) } ) C_ RR )
94	92, 93	syl 17	. . . . . . . 8 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( `' F " { ( y - z ) } ) C_ RR )
95		mblvol 22470	. . . . . . . . . 10 |- ( ( `' F " { ( y - z ) } ) e. dom vol -> ( vol ` ( `' F " { ( y - z ) } ) ) = ( vol* ` ( `' F " { ( y - z ) } ) ) )
96	92, 95	syl 17	. . . . . . . . 9 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( vol ` ( `' F " { ( y - z ) } ) ) = ( vol* ` ( `' F " { ( y - z ) } ) ) )
97		simprr 764	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> z = 0 )
98	97	oveq2d 6317	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( y - z ) = ( y - 0 ) )
99	54	adantr 466	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> y e. CC )
100	99	subid1d 9975	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( y - 0 ) = y )
101	98, 100	eqtrd 2463	. . . . . . . . . . . . 13 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( y - z ) = y )
102	101	sneqd 4008	. . . . . . . . . . . 12 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> { ( y - z ) } = { y } )
103	102	imaeq2d 5183	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( `' F " { ( y - z ) } ) = ( `' F " { y } ) )
104	103	fveq2d 5881	. . . . . . . . . 10 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( vol ` ( `' F " { ( y - z ) } ) ) = ( vol ` ( `' F " { y } ) ) )
105		i1fima2sn 22624	. . . . . . . . . . . 12 |- ( ( F e. dom S.1 /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ( vol ` ( `' F " { y } ) ) e. RR )
106	3, 105	sylan 473	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ( vol ` ( `' F " { y } ) ) e. RR )
107	106	adantr 466	. . . . . . . . . 10 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( vol ` ( `' F " { y } ) ) e. RR )
108	104, 107	eqeltrd 2510	. . . . . . . . 9 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( vol ` ( `' F " { ( y - z ) } ) ) e. RR )
109	96, 108	eqeltrrd 2511	. . . . . . . 8 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( vol* ` ( `' F " { ( y - z ) } ) ) e. RR )
110		ovolsscl 22425	. . . . . . . 8 |- ( ( ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) C_ ( `' F " { ( y - z ) } ) /\ ( `' F " { ( y - z ) } ) C_ RR /\ ( vol* ` ( `' F " { ( y - z ) } ) ) e. RR ) -> ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) e. RR )
111	91, 94, 109, 110	syl3anc 1264	. . . . . . 7 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) e. RR )
112	111	expr 618	. . . . . 6 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ( z = 0 -> ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) e. RR ) )
113		eldifsn 4122	. . . . . . . 8 |- ( z e. ( ran G \ { 0 } ) <-> ( z e. ran G /\ z =/= 0 ) )
114		inss2 3683	. . . . . . . . . 10 |- ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) C_ ( `' G " { z } )
115	114	a1i 11	. . . . . . . . 9 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ( ran G \ { 0 } ) ) -> ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) C_ ( `' G " { z } ) )
116		eldifi 3587	. . . . . . . . . 10 |- ( z e. ( ran G \ { 0 } ) -> z e. ran G )
117		mblss 22471	. . . . . . . . . . 11 |- ( ( `' G " { z } ) e. dom vol -> ( `' G " { z } ) C_ RR )
118	79, 117	syl 17	. . . . . . . . . 10 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ( `' G " { z } ) C_ RR )
119	116, 118	sylan2 476	. . . . . . . . 9 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ( ran G \ { 0 } ) ) -> ( `' G " { z } ) C_ RR )
120		i1fima 22622	. . . . . . . . . . . . 13 |- ( G e. dom S.1 -> ( `' G " { z } ) e. dom vol )
121	6, 120	syl 17	. . . . . . . . . . . 12 |- ( ph -> ( `' G " { z } ) e. dom vol )
122	121	ad2antrr 730	. . . . . . . . . . 11 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ( ran G \ { 0 } ) ) -> ( `' G " { z } ) e. dom vol )
123		mblvol 22470	. . . . . . . . . . 11 |- ( ( `' G " { z } ) e. dom vol -> ( vol ` ( `' G " { z } ) ) = ( vol* ` ( `' G " { z } ) ) )
124	122, 123	syl 17	. . . . . . . . . 10 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ( ran G \ { 0 } ) ) -> ( vol ` ( `' G " { z } ) ) = ( vol* ` ( `' G " { z } ) ) )
125	6	adantr 466	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> G e. dom S.1 )
126		i1fima2sn 22624	. . . . . . . . . . 11 |- ( ( G e. dom S.1 /\ z e. ( ran G \ { 0 } ) ) -> ( vol ` ( `' G " { z } ) ) e. RR )
127	125, 126	sylan 473	. . . . . . . . . 10 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ( ran G \ { 0 } ) ) -> ( vol ` ( `' G " { z } ) ) e. RR )
128	124, 127	eqeltrrd 2511	. . . . . . . . 9 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ( ran G \ { 0 } ) ) -> ( vol* ` ( `' G " { z } ) ) e. RR )
129		ovolsscl 22425	. . . . . . . . 9 |- ( ( ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) C_ ( `' G " { z } ) /\ ( `' G " { z } ) C_ RR /\ ( vol* ` ( `' G " { z } ) ) e. RR ) -> ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) e. RR )
130	115, 119, 128, 129	syl3anc 1264	. . . . . . . 8 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ( ran G \ { 0 } ) ) -> ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) e. RR )
131	113, 130	sylan2br 478	. . . . . . 7 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z =/= 0 ) ) -> ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) e. RR )
132	131	expr 618	. . . . . 6 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ( z =/= 0 -> ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) e. RR ) )
133	112, 132	pm2.61dne 2741	. . . . 5 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) e. RR )
134	57, 133	fsumrecl 13787	. . . 4 |- ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> sum_ z e. ran G ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) e. RR )
135	56	fveq2d 5881	. . . . 5 |- ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ( vol* ` ( `' ( F oF + G ) " { y } ) ) = ( vol* ` U_ z e. ran G ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) )
136	114, 118	syl5ss 3475	. . . . . . . 8 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) C_ RR )
137	136, 133	jca 534	. . . . . . 7 |- ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ( ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) C_ RR /\ ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) e. RR ) )
138	137	ralrimiva 2839	. . . . . 6 |- ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> A. z e. ran G ( ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) C_ RR /\ ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) e. RR ) )
139		ovolfiniun 22440	. . . . . 6 |- ( ( ran G e. Fin /\ A. z e. ran G ( ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) C_ RR /\ ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) e. RR ) ) -> ( vol* ` U_ z e. ran G ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) <_ sum_ z e. ran G ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) )
140	57, 138, 139	syl2anc 665	. . . . 5 |- ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ( vol* ` U_ z e. ran G ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) <_ sum_ z e. ran G ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) )
141	135, 140	eqbrtrd 4441	. . . 4 |- ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ( vol* ` ( `' ( F oF + G ) " { y } ) ) <_ sum_ z e. ran G ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) )
142		ovollecl 22422	. . . 4 |- ( ( ( `' ( F oF + G ) " { y } ) C_ RR /\ sum_ z e. ran G ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) e. RR /\ ( vol* ` ( `' ( F oF + G ) " { y } ) ) <_ sum_ z e. ran G ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) ) -> ( vol* ` ( `' ( F oF + G ) " { y } ) ) e. RR )
143	89, 134, 141, 142	syl3anc 1264	. . 3 |- ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ( vol* ` ( `' ( F oF + G ) " { y } ) ) e. RR )
144	87, 143	eqeltrd 2510	. 2 |- ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ( vol ` ( `' ( F oF + G ) " { y } ) ) e. RR )
145	12, 49, 85, 144	i1fd 22625	1 |- ( ph -> ( F oF + G ) e. dom S.1 )

Syntax hints:   -> wi 4   /\ wa 370   = wceq 1437   e. wcel 1868   {cab 2407   =/= wne 2618   A.wral 2775   E.wrex 2776   _Vcvv 3081   \ cdif 3433   i^i cin 3435   C_ wss 3436   {csn 3996   U_ciun 4296   class class class wbr 4420   X. cxp 4847   `'ccnv 4848   dom cdm 4849   ran crn 4850   "cima 4852   Fn wfn 5592   -->wf 5593   -onto->wfo 5595   ` cfv 5597  (class class class)co 6301   |-> cmpt2 6303   oFcof 6539   Fincfn 7573   CCcc 9537   RRcr 9538   0cc0 9539   + caddc 9542   <_ cle 9676   - cmin 9860   sum_csu 13739   vol*covol 22399   volcvol 22401  MblFncmbf 22558   S.1citg1 22559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-inf2 8148  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616  ax-pre-sup 9617

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-int 4253  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-se 4809  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-isom 5606  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-of 6541  df-om 6703  df-1st 6803  df-2nd 6804  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-1o 7186  df-2o 7187  df-oadd 7190  df-er 7367  df-map 7478  df-pm 7479  df-en 7574  df-dom 7575  df-sdom 7576  df-fin 7577  df-sup 7958  df-inf 7959  df-oi 8027  df-card 8374  df-cda 8598  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-div 10270  df-nn 10610  df-2 10668  df-3 10669  df-n0 10870  df-z 10938  df-uz 11160  df-q 11265  df-rp 11303  df-xadd 11410  df-ioo 11639  df-ico 11641  df-icc 11642  df-fz 11785  df-fzo 11916  df-fl 12027  df-seq 12213  df-exp 12272  df-hash 12515  df-cj 13150  df-re 13151  df-im 13152  df-sqrt 13286  df-abs 13287  df-clim 13539  df-sum 13740  df-xmet 18950  df-met 18951  df-ovol 22402  df-vol 22404  df-mbf 22563  df-itg1 22564

This theorem is referenced by:  itg1addlem4  22643  i1fsub  22652  itg2splitlem  22692  itg2split  22693  itg2addlem  22702  itg2addnc  31909  ftc1anclem3  31932  ftc1anclem5  31934  ftc1anclem8  31937