Metamath Proof Explorer

Theorem i1fadd

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

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

Proof

Step Hyp Ref Expression
1 i1fadd.1 
 |-  ( ph -> F e. dom S.1 )
2 i1fadd.2 
 |-  ( ph -> G e. dom S.1 )
3 readdcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + y ) e. RR )
4 3 adantl 
 |-  ( ( ph /\ ( x e. RR /\ y e. RR ) ) -> ( x + y ) e. RR )
5 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
6 1 5 syl 
 |-  ( ph -> F : RR --> RR )
7 i1ff 
 |-  ( G e. dom S.1 -> G : RR --> RR )
8 2 7 syl 
 |-  ( ph -> G : RR --> RR )
9 reex 
 |-  RR e. _V
10 9 a1i 
 |-  ( ph -> RR e. _V )
11 inidm 
 |-  ( RR i^i RR ) = RR
12 4 6 8 10 10 11 off 
 |-  ( ph -> ( F oF + G ) : RR --> RR )
13 i1frn 
 |-  ( F e. dom S.1 -> ran F e. Fin )
14 1 13 syl 
 |-  ( ph -> ran F e. Fin )
15 i1frn 
 |-  ( G e. dom S.1 -> ran G e. Fin )
16 2 15 syl 
 |-  ( ph -> ran G e. Fin )
17 xpfi 
 |-  ( ( ran F e. Fin /\ ran G e. Fin ) -> ( ran F X. ran G ) e. Fin )
18 14 16 17 syl2anc 
 |-  ( ph -> ( ran F X. ran G ) e. Fin )
19 eqid 
 |-  ( u e. ran F , v e. ran G |-> ( u + v ) ) = ( u e. ran F , v e. ran G |-> ( u + v ) )
20 ovex 
 |-  ( u + v ) e. _V
21 19 20 fnmpoi 
 |-  ( u e. ran F , v e. ran G |-> ( u + v ) ) Fn ( ran F X. ran G )
22 dffn4 
 |-  ( ( 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 
 |-  ( 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 
 |-  ( ( ( 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 
 |-  ( ph -> ran ( u e. ran F , v e. ran G |-> ( u + v ) ) e. Fin )
26 eqid 
 |-  ( x + y ) = ( x + y )
27 rspceov 
 |-  ( ( 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 
 |-  ( ( x e. ran F /\ y e. ran G ) -> E. u e. ran F E. v e. ran G ( x + y ) = ( u + v ) )
29 ovex 
 |-  ( x + y ) e. _V
30 eqeq1 
 |-  ( w = ( x + y ) -> ( w = ( u + v ) <-> ( x + y ) = ( u + v ) ) )
31 30 2rexbidv 
 |-  ( 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 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( ( 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 6 ffnd 
 |-  ( ph -> F Fn RR )
36 dffn3 
 |-  ( F Fn RR <-> F : RR --> ran F )
37 35 36 sylib 
 |-  ( ph -> F : RR --> ran F )
38 8 ffnd 
 |-  ( ph -> G Fn RR )
39 dffn3 
 |-  ( G Fn RR <-> G : RR --> ran G )
40 38 39 sylib 
 |-  ( ph -> G : RR --> ran G )
41 34 37 40 10 10 11 off 
 |-  ( ph -> ( F oF + G ) : RR --> { w | E. u e. ran F E. v e. ran G w = ( u + v ) } )
42 41 frnd 
 |-  ( ph -> ran ( F oF + G ) C_ { w | E. u e. ran F E. v e. ran G w = ( u + v ) } )
43 19 rnmpo 
 |-  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 ) }
44 42 43 sseqtrrdi 
 |-  ( ph -> ran ( F oF + G ) C_ ran ( u e. ran F , v e. ran G |-> ( u + v ) ) )
45 25 44 ssfid 
 |-  ( ph -> ran ( F oF + G ) e. Fin )
46 12 frnd 
 |-  ( ph -> ran ( F oF + G ) C_ RR )
47 46 ssdifssd 
 |-  ( ph -> ( ran ( F oF + G ) \ { 0 } ) C_ RR )
48 47 sselda 
 |-  ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> y e. RR )
49 48 recnd 
 |-  ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> y e. CC )
50 1 2 i1faddlem 
 |-  ( ( ph /\ y e. CC ) -> ( `' ( F oF + G ) " { y } ) = U_ z e. ran G ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) )
51 49 50 syldan 
 |-  ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ( `' ( F oF + G ) " { y } ) = U_ z e. ran G ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) )
52 16 adantr 
 |-  ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ran G e. Fin )
53 1 ad2antrr 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> F e. dom S.1 )
54 i1fmbf 
 |-  ( F e. dom S.1 -> F e. MblFn )
55 53 54 syl 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> F e. MblFn )
56 6 ad2antrr 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> F : RR --> RR )
57 12 ad2antrr 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ( F oF + G ) : RR --> RR )
58 57 frnd 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ran ( F oF + G ) C_ RR )
59 eldifi 
 |-  ( y e. ( ran ( F oF + G ) \ { 0 } ) -> y e. ran ( F oF + G ) )
60 59 ad2antlr 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> y e. ran ( F oF + G ) )
61 58 60 sseldd 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> y e. RR )
62 8 adantr 
 |-  ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> G : RR --> RR )
63 62 frnd 
 |-  ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ran G C_ RR )
64 63 sselda 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> z e. RR )
65 61 64 resubcld 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ( y - z ) e. RR )
66 mbfimasn 
 |-  ( ( F e. MblFn /\ F : RR --> RR /\ ( y - z ) e. RR ) -> ( `' F " { ( y - z ) } ) e. dom vol )
67 55 56 65 66 syl3anc 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ( `' F " { ( y - z ) } ) e. dom vol )
68 2 ad2antrr 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> G e. dom S.1 )
69 i1fmbf 
 |-  ( G e. dom S.1 -> G e. MblFn )
70 68 69 syl 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> G e. MblFn )
71 8 ad2antrr 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> G : RR --> RR )
72 mbfimasn 
 |-  ( ( G e. MblFn /\ G : RR --> RR /\ z e. RR ) -> ( `' G " { z } ) e. dom vol )
73 70 71 64 72 syl3anc 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ( `' G " { z } ) e. dom vol )
74 inmbl 
 |-  ( ( ( `' F " { ( y - z ) } ) e. dom vol /\ ( `' G " { z } ) e. dom vol ) -> ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) e. dom vol )
75 67 73 74 syl2anc 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) e. dom vol )
76 75 ralrimiva 
 |-  ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> A. z e. ran G ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) e. dom vol )
77 finiunmbl 
 |-  ( ( 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 )
78 52 76 77 syl2anc 
 |-  ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> U_ z e. ran G ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) e. dom vol )
79 51 78 eqeltrd 
 |-  ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ( `' ( F oF + G ) " { y } ) e. dom vol )
80 mblvol 
 |-  ( ( `' ( F oF + G ) " { y } ) e. dom vol -> ( vol ` ( `' ( F oF + G ) " { y } ) ) = ( vol* ` ( `' ( F oF + G ) " { y } ) ) )
81 79 80 syl 
 |-  ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ( vol ` ( `' ( F oF + G ) " { y } ) ) = ( vol* ` ( `' ( F oF + G ) " { y } ) ) )
82 mblss 
 |-  ( ( `' ( F oF + G ) " { y } ) e. dom vol -> ( `' ( F oF + G ) " { y } ) C_ RR )
83 79 82 syl 
 |-  ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ( `' ( F oF + G ) " { y } ) C_ RR )
84 inss1 
 |-  ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) C_ ( `' F " { ( y - z ) } )
85 67 adantrr 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( `' F " { ( y - z ) } ) e. dom vol )
86 mblss 
 |-  ( ( `' F " { ( y - z ) } ) e. dom vol -> ( `' F " { ( y - z ) } ) C_ RR )
87 85 86 syl 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( `' F " { ( y - z ) } ) C_ RR )
88 mblvol 
 |-  ( ( `' F " { ( y - z ) } ) e. dom vol -> ( vol ` ( `' F " { ( y - z ) } ) ) = ( vol* ` ( `' F " { ( y - z ) } ) ) )
89 85 88 syl 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( vol ` ( `' F " { ( y - z ) } ) ) = ( vol* ` ( `' F " { ( y - z ) } ) ) )
90 simprr 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> z = 0 )
91 90 oveq2d 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( y - z ) = ( y - 0 ) )
92 49 adantr 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> y e. CC )
93 92 subid1d 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( y - 0 ) = y )
94 91 93 eqtrd 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( y - z ) = y )
95 94 sneqd 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> { ( y - z ) } = { y } )
96 95 imaeq2d 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( `' F " { ( y - z ) } ) = ( `' F " { y } ) )
97 96 fveq2d 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( vol ` ( `' F " { ( y - z ) } ) ) = ( vol ` ( `' F " { y } ) ) )
98 i1fima2sn 
 |-  ( ( F e. dom S.1 /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ( vol ` ( `' F " { y } ) ) e. RR )
99 1 98 sylan 
 |-  ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ( vol ` ( `' F " { y } ) ) e. RR )
100 99 adantr 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( vol ` ( `' F " { y } ) ) e. RR )
101 97 100 eqeltrd 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( vol ` ( `' F " { ( y - z ) } ) ) e. RR )
102 89 101 eqeltrrd 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( vol* ` ( `' F " { ( y - z ) } ) ) e. RR )
103 ovolsscl 
 |-  ( ( ( ( `' 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 )
104 84 87 102 103 mp3an2i 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z = 0 ) ) -> ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) e. RR )
105 104 expr 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ( z = 0 -> ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) e. RR ) )
106 eldifsn 
 |-  ( z e. ( ran G \ { 0 } ) <-> ( z e. ran G /\ z =/= 0 ) )
107 inss2 
 |-  ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) C_ ( `' G " { z } )
108 eldifi 
 |-  ( z e. ( ran G \ { 0 } ) -> z e. ran G )
109 mblss 
 |-  ( ( `' G " { z } ) e. dom vol -> ( `' G " { z } ) C_ RR )
110 73 109 syl 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ( `' G " { z } ) C_ RR )
111 108 110 sylan2 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ( ran G \ { 0 } ) ) -> ( `' G " { z } ) C_ RR )
112 i1fima 
 |-  ( G e. dom S.1 -> ( `' G " { z } ) e. dom vol )
113 2 112 syl 
 |-  ( ph -> ( `' G " { z } ) e. dom vol )
114 113 ad2antrr 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ( ran G \ { 0 } ) ) -> ( `' G " { z } ) e. dom vol )
115 mblvol 
 |-  ( ( `' G " { z } ) e. dom vol -> ( vol ` ( `' G " { z } ) ) = ( vol* ` ( `' G " { z } ) ) )
116 114 115 syl 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ( ran G \ { 0 } ) ) -> ( vol ` ( `' G " { z } ) ) = ( vol* ` ( `' G " { z } ) ) )
117 2 adantr 
 |-  ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> G e. dom S.1 )
118 i1fima2sn 
 |-  ( ( G e. dom S.1 /\ z e. ( ran G \ { 0 } ) ) -> ( vol ` ( `' G " { z } ) ) e. RR )
119 117 118 sylan 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ( ran G \ { 0 } ) ) -> ( vol ` ( `' G " { z } ) ) e. RR )
120 116 119 eqeltrrd 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ( ran G \ { 0 } ) ) -> ( vol* ` ( `' G " { z } ) ) e. RR )
121 ovolsscl 
 |-  ( ( ( ( `' 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 )
122 107 111 120 121 mp3an2i 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ( ran G \ { 0 } ) ) -> ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) e. RR )
123 106 122 sylan2br 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ ( z e. ran G /\ z =/= 0 ) ) -> ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) e. RR )
124 123 expr 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ( z =/= 0 -> ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) e. RR ) )
125 105 124 pm2.61dne 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) e. RR )
126 52 125 fsumrecl 
 |-  ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> sum_ z e. ran G ( vol* ` ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) ) e. RR )
127 51 fveq2d 
 |-  ( ( 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 } ) ) ) )
128 107 110 sstrid 
 |-  ( ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) /\ z e. ran G ) -> ( ( `' F " { ( y - z ) } ) i^i ( `' G " { z } ) ) C_ RR )
129 128 125 jca 
 |-  ( ( ( 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 ) )
130 129 ralrimiva 
 |-  ( ( 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 ) )
131 ovolfiniun 
 |-  ( ( 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 } ) ) ) )
132 52 130 131 syl2anc 
 |-  ( ( 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 } ) ) ) )
133 127 132 eqbrtrd 
 |-  ( ( 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 } ) ) ) )
134 ovollecl 
 |-  ( ( ( `' ( 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 )
135 83 126 133 134 syl3anc 
 |-  ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ( vol* ` ( `' ( F oF + G ) " { y } ) ) e. RR )
136 81 135 eqeltrd 
 |-  ( ( ph /\ y e. ( ran ( F oF + G ) \ { 0 } ) ) -> ( vol ` ( `' ( F oF + G ) " { y } ) ) e. RR )
137 12 45 79 136 i1fd 
 |-  ( ph -> ( F oF + G ) e. dom S.1 )