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 ) |