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 )