Metamath Proof Explorer

Theorem itg1addlem4

Description: Lemma for itg1add . (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Hypotheses i1fadd.1 
|- ( ph -> F e. dom S.1 )
i1fadd.2 
|- ( ph -> G e. dom S.1 )
itg1add.3 
|- I = ( i e. RR , j e. RR |-> if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) )
itg1add.4 
|- P = ( + |` ( ran F X. ran G ) )
Assertion itg1addlem4 
|- ( ph -> ( S.1 ` ( F oF + G ) ) = sum_ y e. ran F sum_ z e. ran G ( ( y + z ) x. ( y I z ) ) )

Proof

Step Hyp Ref Expression
1 i1fadd.1 
 |-  ( ph -> F e. dom S.1 )
2 i1fadd.2 
 |-  ( ph -> G e. dom S.1 )
3 itg1add.3 
 |-  I = ( i e. RR , j e. RR |-> if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) )
4 itg1add.4 
 |-  P = ( + |` ( ran F X. ran G ) )
5 1 2 i1fadd 
 |-  ( ph -> ( F oF + G ) e. dom S.1 )
6 i1frn 
 |-  ( F e. dom S.1 -> ran F e. Fin )
7 1 6 syl 
 |-  ( ph -> ran F e. Fin )
8 i1frn 
 |-  ( G e. dom S.1 -> ran G e. Fin )
9 2 8 syl 
 |-  ( ph -> ran G e. Fin )
10 xpfi 
 |-  ( ( ran F e. Fin /\ ran G e. Fin ) -> ( ran F X. ran G ) e. Fin )
11 7 9 10 syl2anc 
 |-  ( ph -> ( ran F X. ran G ) e. Fin )
12 ax-addf 
 |-  + : ( CC X. CC ) --> CC
13 ffn 
 |-  ( + : ( CC X. CC ) --> CC -> + Fn ( CC X. CC ) )
14 12 13 ax-mp 
 |-  + Fn ( CC X. CC )
15 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
16 1 15 syl 
 |-  ( ph -> F : RR --> RR )
17 16 frnd 
 |-  ( ph -> ran F C_ RR )
18 ax-resscn 
 |-  RR C_ CC
19 17 18 sstrdi 
 |-  ( ph -> ran F C_ CC )
20 i1ff 
 |-  ( G e. dom S.1 -> G : RR --> RR )
21 2 20 syl 
 |-  ( ph -> G : RR --> RR )
22 21 frnd 
 |-  ( ph -> ran G C_ RR )
23 22 18 sstrdi 
 |-  ( ph -> ran G C_ CC )
24 xpss12 
 |-  ( ( ran F C_ CC /\ ran G C_ CC ) -> ( ran F X. ran G ) C_ ( CC X. CC ) )
25 19 23 24 syl2anc 
 |-  ( ph -> ( ran F X. ran G ) C_ ( CC X. CC ) )
26 fnssres 
 |-  ( ( + Fn ( CC X. CC ) /\ ( ran F X. ran G ) C_ ( CC X. CC ) ) -> ( + |` ( ran F X. ran G ) ) Fn ( ran F X. ran G ) )
27 14 25 26 sylancr 
 |-  ( ph -> ( + |` ( ran F X. ran G ) ) Fn ( ran F X. ran G ) )
28 4 fneq1i 
 |-  ( P Fn ( ran F X. ran G ) <-> ( + |` ( ran F X. ran G ) ) Fn ( ran F X. ran G ) )
29 27 28 sylibr 
 |-  ( ph -> P Fn ( ran F X. ran G ) )
30 dffn4 
 |-  ( P Fn ( ran F X. ran G ) <-> P : ( ran F X. ran G ) -onto-> ran P )
31 29 30 sylib 
 |-  ( ph -> P : ( ran F X. ran G ) -onto-> ran P )
32 fofi 
 |-  ( ( ( ran F X. ran G ) e. Fin /\ P : ( ran F X. ran G ) -onto-> ran P ) -> ran P e. Fin )
33 11 31 32 syl2anc 
 |-  ( ph -> ran P e. Fin )
34 difss 
 |-  ( ran P \ { 0 } ) C_ ran P
35 ssfi 
 |-  ( ( ran P e. Fin /\ ( ran P \ { 0 } ) C_ ran P ) -> ( ran P \ { 0 } ) e. Fin )
36 33 34 35 sylancl 
 |-  ( ph -> ( ran P \ { 0 } ) e. Fin )
37 ffun 
 |-  ( + : ( CC X. CC ) --> CC -> Fun + )
38 12 37 ax-mp 
 |-  Fun +
39 12 fdmi 
 |-  dom + = ( CC X. CC )
40 25 39 sseqtrrdi 
 |-  ( ph -> ( ran F X. ran G ) C_ dom + )
41 funfvima2 
 |-  ( ( Fun + /\ ( ran F X. ran G ) C_ dom + ) -> ( <. x , y >. e. ( ran F X. ran G ) -> ( + ` <. x , y >. ) e. ( + " ( ran F X. ran G ) ) ) )
42 38 40 41 sylancr 
 |-  ( ph -> ( <. x , y >. e. ( ran F X. ran G ) -> ( + ` <. x , y >. ) e. ( + " ( ran F X. ran G ) ) ) )
43 opelxpi 
 |-  ( ( x e. ran F /\ y e. ran G ) -> <. x , y >. e. ( ran F X. ran G ) )
44 42 43 impel 
 |-  ( ( ph /\ ( x e. ran F /\ y e. ran G ) ) -> ( + ` <. x , y >. ) e. ( + " ( ran F X. ran G ) ) )
45 df-ov 
 |-  ( x + y ) = ( + ` <. x , y >. )
46 4 rneqi 
 |-  ran P = ran ( + |` ( ran F X. ran G ) )
47 df-ima 
 |-  ( + " ( ran F X. ran G ) ) = ran ( + |` ( ran F X. ran G ) )
48 46 47 eqtr4i 
 |-  ran P = ( + " ( ran F X. ran G ) )
49 44 45 48 3eltr4g 
 |-  ( ( ph /\ ( x e. ran F /\ y e. ran G ) ) -> ( x + y ) e. ran P )
50 16 ffnd 
 |-  ( ph -> F Fn RR )
51 dffn3 
 |-  ( F Fn RR <-> F : RR --> ran F )
52 50 51 sylib 
 |-  ( ph -> F : RR --> ran F )
53 21 ffnd 
 |-  ( ph -> G Fn RR )
54 dffn3 
 |-  ( G Fn RR <-> G : RR --> ran G )
55 53 54 sylib 
 |-  ( ph -> G : RR --> ran G )
56 reex 
 |-  RR e. _V
57 56 a1i 
 |-  ( ph -> RR e. _V )
58 inidm 
 |-  ( RR i^i RR ) = RR
59 49 52 55 57 57 58 off 
 |-  ( ph -> ( F oF + G ) : RR --> ran P )
60 59 frnd 
 |-  ( ph -> ran ( F oF + G ) C_ ran P )
61 60 ssdifd 
 |-  ( ph -> ( ran ( F oF + G ) \ { 0 } ) C_ ( ran P \ { 0 } ) )
62 17 sselda 
 |-  ( ( ph /\ y e. ran F ) -> y e. RR )
63 22 sselda 
 |-  ( ( ph /\ z e. ran G ) -> z e. RR )
64 62 63 anim12dan 
 |-  ( ( ph /\ ( y e. ran F /\ z e. ran G ) ) -> ( y e. RR /\ z e. RR ) )
65 readdcl 
 |-  ( ( y e. RR /\ z e. RR ) -> ( y + z ) e. RR )
66 64 65 syl 
 |-  ( ( ph /\ ( y e. ran F /\ z e. ran G ) ) -> ( y + z ) e. RR )
67 66 ralrimivva 
 |-  ( ph -> A. y e. ran F A. z e. ran G ( y + z ) e. RR )
68 funimassov 
 |-  ( ( Fun + /\ ( ran F X. ran G ) C_ dom + ) -> ( ( + " ( ran F X. ran G ) ) C_ RR <-> A. y e. ran F A. z e. ran G ( y + z ) e. RR ) )
69 38 40 68 sylancr 
 |-  ( ph -> ( ( + " ( ran F X. ran G ) ) C_ RR <-> A. y e. ran F A. z e. ran G ( y + z ) e. RR ) )
70 67 69 mpbird 
 |-  ( ph -> ( + " ( ran F X. ran G ) ) C_ RR )
71 48 70 eqsstrid 
 |-  ( ph -> ran P C_ RR )
72 71 ssdifd 
 |-  ( ph -> ( ran P \ { 0 } ) C_ ( RR \ { 0 } ) )
73 itg1val2 
 |-  ( ( ( F oF + G ) e. dom S.1 /\ ( ( ran P \ { 0 } ) e. Fin /\ ( ran ( F oF + G ) \ { 0 } ) C_ ( ran P \ { 0 } ) /\ ( ran P \ { 0 } ) C_ ( RR \ { 0 } ) ) ) -> ( S.1 ` ( F oF + G ) ) = sum_ w e. ( ran P \ { 0 } ) ( w x. ( vol ` ( `' ( F oF + G ) " { w } ) ) ) )
74 5 36 61 72 73 syl13anc 
 |-  ( ph -> ( S.1 ` ( F oF + G ) ) = sum_ w e. ( ran P \ { 0 } ) ( w x. ( vol ` ( `' ( F oF + G ) " { w } ) ) ) )
75 21 adantr 
 |-  ( ( ph /\ w e. ( ran P \ { 0 } ) ) -> G : RR --> RR )
76 9 adantr 
 |-  ( ( ph /\ w e. ( ran P \ { 0 } ) ) -> ran G e. Fin )
77 inss2 
 |-  ( ( `' F " { ( w - z ) } ) i^i ( `' G " { z } ) ) C_ ( `' G " { z } )
78 77 a1i 
 |-  ( ( ( ph /\ w e. ( ran P \ { 0 } ) ) /\ z e. ran G ) -> ( ( `' F " { ( w - z ) } ) i^i ( `' G " { z } ) ) C_ ( `' G " { z } ) )
79 i1fima 
 |-  ( F e. dom S.1 -> ( `' F " { ( w - z ) } ) e. dom vol )
80 1 79 syl 
 |-  ( ph -> ( `' F " { ( w - z ) } ) e. dom vol )
81 i1fima 
 |-  ( G e. dom S.1 -> ( `' G " { z } ) e. dom vol )
82 2 81 syl 
 |-  ( ph -> ( `' G " { z } ) e. dom vol )
83 inmbl 
 |-  ( ( ( `' F " { ( w - z ) } ) e. dom vol /\ ( `' G " { z } ) e. dom vol ) -> ( ( `' F " { ( w - z ) } ) i^i ( `' G " { z } ) ) e. dom vol )
84 80 82 83 syl2anc 
 |-  ( ph -> ( ( `' F " { ( w - z ) } ) i^i ( `' G " { z } ) ) e. dom vol )
85 84 ad2antrr 
 |-  ( ( ( ph /\ w e. ( ran P \ { 0 } ) ) /\ z e. ran G ) -> ( ( `' F " { ( w - z ) } ) i^i ( `' G " { z } ) ) e. dom vol )
86 34 71 sstrid 
 |-  ( ph -> ( ran P \ { 0 } ) C_ RR )
87 86 sselda 
 |-  ( ( ph /\ w e. ( ran P \ { 0 } ) ) -> w e. RR )
88 87 adantr 
 |-  ( ( ( ph /\ w e. ( ran P \ { 0 } ) ) /\ z e. ran G ) -> w e. RR )
89 63 adantlr 
 |-  ( ( ( ph /\ w e. ( ran P \ { 0 } ) ) /\ z e. ran G ) -> z e. RR )
90 88 89 resubcld 
 |-  ( ( ( ph /\ w e. ( ran P \ { 0 } ) ) /\ z e. ran G ) -> ( w - z ) e. RR )
91 88 recnd 
 |-  ( ( ( ph /\ w e. ( ran P \ { 0 } ) ) /\ z e. ran G ) -> w e. CC )
92 89 recnd 
 |-  ( ( ( ph /\ w e. ( ran P \ { 0 } ) ) /\ z e. ran G ) -> z e. CC )
93 91 92 npcand 
 |-  ( ( ( ph /\ w e. ( ran P \ { 0 } ) ) /\ z e. ran G ) -> ( ( w - z ) + z ) = w )
94 eldifsni 
 |-  ( w e. ( ran P \ { 0 } ) -> w =/= 0 )
95 94 ad2antlr 
 |-  ( ( ( ph /\ w e. ( ran P \ { 0 } ) ) /\ z e. ran G ) -> w =/= 0 )
96 93 95 eqnetrd 
 |-  ( ( ( ph /\ w e. ( ran P \ { 0 } ) ) /\ z e. ran G ) -> ( ( w - z ) + z ) =/= 0 )
97 oveq12 
 |-  ( ( ( w - z ) = 0 /\ z = 0 ) -> ( ( w - z ) + z ) = ( 0 + 0 ) )
98 00id 
 |-  ( 0 + 0 ) = 0
99 97 98 eqtrdi 
 |-  ( ( ( w - z ) = 0 /\ z = 0 ) -> ( ( w - z ) + z ) = 0 )
100 99 necon3ai 
 |-  ( ( ( w - z ) + z ) =/= 0 -> -. ( ( w - z ) = 0 /\ z = 0 ) )
101 96 100 syl 
 |-  ( ( ( ph /\ w e. ( ran P \ { 0 } ) ) /\ z e. ran G ) -> -. ( ( w - z ) = 0 /\ z = 0 ) )
102 1 2 3 itg1addlem3 
 |-  ( ( ( ( w - z ) e. RR /\ z e. RR ) /\ -. ( ( w - z ) = 0 /\ z = 0 ) ) -> ( ( w - z ) I z ) = ( vol ` ( ( `' F " { ( w - z ) } ) i^i ( `' G " { z } ) ) ) )
103 90 89 101 102 syl21anc 
 |-  ( ( ( ph /\ w e. ( ran P \ { 0 } ) ) /\ z e. ran G ) -> ( ( w - z ) I z ) = ( vol ` ( ( `' F " { ( w - z ) } ) i^i ( `' G " { z } ) ) ) )
104 1 2 3 itg1addlem2 
 |-  ( ph -> I : ( RR X. RR ) --> RR )
105 104 ad2antrr 
 |-  ( ( ( ph /\ w e. ( ran P \ { 0 } ) ) /\ z e. ran G ) -> I : ( RR X. RR ) --> RR )
106 105 90 89 fovrnd 
 |-  ( ( ( ph /\ w e. ( ran P \ { 0 } ) ) /\ z e. ran G ) -> ( ( w - z ) I z ) e. RR )
107 103 106 eqeltrrd 
 |-  ( ( ( ph /\ w e. ( ran P \ { 0 } ) ) /\ z e. ran G ) -> ( vol ` ( ( `' F " { ( w - z ) } ) i^i ( `' G " { z } ) ) ) e. RR )
108 75 76 78 85 107 itg1addlem1 
 |-  ( ( ph /\ w e. ( ran P \ { 0 } ) ) -> ( vol ` U_ z e. ran G ( ( `' F " { ( w - z ) } ) i^i ( `' G " { z } ) ) ) = sum_ z e. ran G ( vol ` ( ( `' F " { ( w - z ) } ) i^i ( `' G " { z } ) ) ) )
109 87 recnd 
 |-  ( ( ph /\ w e. ( ran P \ { 0 } ) ) -> w e. CC )
110 1 2 i1faddlem 
 |-  ( ( ph /\ w e. CC ) -> ( `' ( F oF + G ) " { w } ) = U_ z e. ran G ( ( `' F " { ( w - z ) } ) i^i ( `' G " { z } ) ) )
111 109 110 syldan 
 |-  ( ( ph /\ w e. ( ran P \ { 0 } ) ) -> ( `' ( F oF + G ) " { w } ) = U_ z e. ran G ( ( `' F " { ( w - z ) } ) i^i ( `' G " { z } ) ) )
112 111 fveq2d 
 |-  ( ( ph /\ w e. ( ran P \ { 0 } ) ) -> ( vol ` ( `' ( F oF + G ) " { w } ) ) = ( vol ` U_ z e. ran G ( ( `' F " { ( w - z ) } ) i^i ( `' G " { z } ) ) ) )
113 103 sumeq2dv 
 |-  ( ( ph /\ w e. ( ran P \ { 0 } ) ) -> sum_ z e. ran G ( ( w - z ) I z ) = sum_ z e. ran G ( vol ` ( ( `' F " { ( w - z ) } ) i^i ( `' G " { z } ) ) ) )
114 108 112 113 3eqtr4d 
 |-  ( ( ph /\ w e. ( ran P \ { 0 } ) ) -> ( vol ` ( `' ( F oF + G ) " { w } ) ) = sum_ z e. ran G ( ( w - z ) I z ) )
115 114 oveq2d 
 |-  ( ( ph /\ w e. ( ran P \ { 0 } ) ) -> ( w x. ( vol ` ( `' ( F oF + G ) " { w } ) ) ) = ( w x. sum_ z e. ran G ( ( w - z ) I z ) ) )
116 106 recnd 
 |-  ( ( ( ph /\ w e. ( ran P \ { 0 } ) ) /\ z e. ran G ) -> ( ( w - z ) I z ) e. CC )
117 76 109 116 fsummulc2 
 |-  ( ( ph /\ w e. ( ran P \ { 0 } ) ) -> ( w x. sum_ z e. ran G ( ( w - z ) I z ) ) = sum_ z e. ran G ( w x. ( ( w - z ) I z ) ) )
118 115 117 eqtrd 
 |-  ( ( ph /\ w e. ( ran P \ { 0 } ) ) -> ( w x. ( vol ` ( `' ( F oF + G ) " { w } ) ) ) = sum_ z e. ran G ( w x. ( ( w - z ) I z ) ) )
119 118 sumeq2dv 
 |-  ( ph -> sum_ w e. ( ran P \ { 0 } ) ( w x. ( vol ` ( `' ( F oF + G ) " { w } ) ) ) = sum_ w e. ( ran P \ { 0 } ) sum_ z e. ran G ( w x. ( ( w - z ) I z ) ) )
120 91 116 mulcld 
 |-  ( ( ( ph /\ w e. ( ran P \ { 0 } ) ) /\ z e. ran G ) -> ( w x. ( ( w - z ) I z ) ) e. CC )
121 120 anasss 
 |-  ( ( ph /\ ( w e. ( ran P \ { 0 } ) /\ z e. ran G ) ) -> ( w x. ( ( w - z ) I z ) ) e. CC )
122 36 9 121 fsumcom 
 |-  ( ph -> sum_ w e. ( ran P \ { 0 } ) sum_ z e. ran G ( w x. ( ( w - z ) I z ) ) = sum_ z e. ran G sum_ w e. ( ran P \ { 0 } ) ( w x. ( ( w - z ) I z ) ) )
123 74 119 122 3eqtrd 
 |-  ( ph -> ( S.1 ` ( F oF + G ) ) = sum_ z e. ran G sum_ w e. ( ran P \ { 0 } ) ( w x. ( ( w - z ) I z ) ) )
124 oveq1 
 |-  ( y = ( w - z ) -> ( y + z ) = ( ( w - z ) + z ) )
125 oveq1 
 |-  ( y = ( w - z ) -> ( y I z ) = ( ( w - z ) I z ) )
126 124 125 oveq12d 
 |-  ( y = ( w - z ) -> ( ( y + z ) x. ( y I z ) ) = ( ( ( w - z ) + z ) x. ( ( w - z ) I z ) ) )
127 33 adantr 
 |-  ( ( ph /\ z e. ran G ) -> ran P e. Fin )
128 71 adantr 
 |-  ( ( ph /\ z e. ran G ) -> ran P C_ RR )
129 128 sselda 
 |-  ( ( ( ph /\ z e. ran G ) /\ v e. ran P ) -> v e. RR )
130 63 adantr 
 |-  ( ( ( ph /\ z e. ran G ) /\ v e. ran P ) -> z e. RR )
131 129 130 resubcld 
 |-  ( ( ( ph /\ z e. ran G ) /\ v e. ran P ) -> ( v - z ) e. RR )
132 131 ex 
 |-  ( ( ph /\ z e. ran G ) -> ( v e. ran P -> ( v - z ) e. RR ) )
133 129 recnd 
 |-  ( ( ( ph /\ z e. ran G ) /\ v e. ran P ) -> v e. CC )
134 133 adantrr 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( v e. ran P /\ y e. ran P ) ) -> v e. CC )
135 71 sselda 
 |-  ( ( ph /\ y e. ran P ) -> y e. RR )
136 135 ad2ant2rl 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( v e. ran P /\ y e. ran P ) ) -> y e. RR )
137 136 recnd 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( v e. ran P /\ y e. ran P ) ) -> y e. CC )
138 63 recnd 
 |-  ( ( ph /\ z e. ran G ) -> z e. CC )
139 138 adantr 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( v e. ran P /\ y e. ran P ) ) -> z e. CC )
140 134 137 139 subcan2ad 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( v e. ran P /\ y e. ran P ) ) -> ( ( v - z ) = ( y - z ) <-> v = y ) )
141 140 ex 
 |-  ( ( ph /\ z e. ran G ) -> ( ( v e. ran P /\ y e. ran P ) -> ( ( v - z ) = ( y - z ) <-> v = y ) ) )
142 132 141 dom2lem 
 |-  ( ( ph /\ z e. ran G ) -> ( v e. ran P |-> ( v - z ) ) : ran P -1-1-> RR )
143 f1f1orn 
 |-  ( ( v e. ran P |-> ( v - z ) ) : ran P -1-1-> RR -> ( v e. ran P |-> ( v - z ) ) : ran P -1-1-onto-> ran ( v e. ran P |-> ( v - z ) ) )
144 142 143 syl 
 |-  ( ( ph /\ z e. ran G ) -> ( v e. ran P |-> ( v - z ) ) : ran P -1-1-onto-> ran ( v e. ran P |-> ( v - z ) ) )
145 oveq1 
 |-  ( v = w -> ( v - z ) = ( w - z ) )
146 eqid 
 |-  ( v e. ran P |-> ( v - z ) ) = ( v e. ran P |-> ( v - z ) )
147 ovex 
 |-  ( w - z ) e. _V
148 145 146 147 fvmpt 
 |-  ( w e. ran P -> ( ( v e. ran P |-> ( v - z ) ) ` w ) = ( w - z ) )
149 148 adantl 
 |-  ( ( ( ph /\ z e. ran G ) /\ w e. ran P ) -> ( ( v e. ran P |-> ( v - z ) ) ` w ) = ( w - z ) )
150 f1f 
 |-  ( ( v e. ran P |-> ( v - z ) ) : ran P -1-1-> RR -> ( v e. ran P |-> ( v - z ) ) : ran P --> RR )
151 frn 
 |-  ( ( v e. ran P |-> ( v - z ) ) : ran P --> RR -> ran ( v e. ran P |-> ( v - z ) ) C_ RR )
152 142 150 151 3syl 
 |-  ( ( ph /\ z e. ran G ) -> ran ( v e. ran P |-> ( v - z ) ) C_ RR )
153 152 sselda 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran ( v e. ran P |-> ( v - z ) ) ) -> y e. RR )
154 63 adantr 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran ( v e. ran P |-> ( v - z ) ) ) -> z e. RR )
155 153 154 readdcld 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran ( v e. ran P |-> ( v - z ) ) ) -> ( y + z ) e. RR )
156 104 ad2antrr 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran ( v e. ran P |-> ( v - z ) ) ) -> I : ( RR X. RR ) --> RR )
157 156 153 154 fovrnd 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran ( v e. ran P |-> ( v - z ) ) ) -> ( y I z ) e. RR )
158 155 157 remulcld 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran ( v e. ran P |-> ( v - z ) ) ) -> ( ( y + z ) x. ( y I z ) ) e. RR )
159 158 recnd 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran ( v e. ran P |-> ( v - z ) ) ) -> ( ( y + z ) x. ( y I z ) ) e. CC )
160 126 127 144 149 159 fsumf1o 
 |-  ( ( ph /\ z e. ran G ) -> sum_ y e. ran ( v e. ran P |-> ( v - z ) ) ( ( y + z ) x. ( y I z ) ) = sum_ w e. ran P ( ( ( w - z ) + z ) x. ( ( w - z ) I z ) ) )
161 128 sselda 
 |-  ( ( ( ph /\ z e. ran G ) /\ w e. ran P ) -> w e. RR )
162 161 recnd 
 |-  ( ( ( ph /\ z e. ran G ) /\ w e. ran P ) -> w e. CC )
163 138 adantr 
 |-  ( ( ( ph /\ z e. ran G ) /\ w e. ran P ) -> z e. CC )
164 162 163 npcand 
 |-  ( ( ( ph /\ z e. ran G ) /\ w e. ran P ) -> ( ( w - z ) + z ) = w )
165 164 oveq1d 
 |-  ( ( ( ph /\ z e. ran G ) /\ w e. ran P ) -> ( ( ( w - z ) + z ) x. ( ( w - z ) I z ) ) = ( w x. ( ( w - z ) I z ) ) )
166 165 sumeq2dv 
 |-  ( ( ph /\ z e. ran G ) -> sum_ w e. ran P ( ( ( w - z ) + z ) x. ( ( w - z ) I z ) ) = sum_ w e. ran P ( w x. ( ( w - z ) I z ) ) )
167 160 166 eqtrd 
 |-  ( ( ph /\ z e. ran G ) -> sum_ y e. ran ( v e. ran P |-> ( v - z ) ) ( ( y + z ) x. ( y I z ) ) = sum_ w e. ran P ( w x. ( ( w - z ) I z ) ) )
168 40 ad2antrr 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> ( ran F X. ran G ) C_ dom + )
169 simpr 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> y e. ran F )
170 simplr 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> z e. ran G )
171 169 170 opelxpd 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> <. y , z >. e. ( ran F X. ran G ) )
172 funfvima2 
 |-  ( ( Fun + /\ ( ran F X. ran G ) C_ dom + ) -> ( <. y , z >. e. ( ran F X. ran G ) -> ( + ` <. y , z >. ) e. ( + " ( ran F X. ran G ) ) ) )
173 38 172 mpan 
 |-  ( ( ran F X. ran G ) C_ dom + -> ( <. y , z >. e. ( ran F X. ran G ) -> ( + ` <. y , z >. ) e. ( + " ( ran F X. ran G ) ) ) )
174 168 171 173 sylc 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> ( + ` <. y , z >. ) e. ( + " ( ran F X. ran G ) ) )
175 df-ov 
 |-  ( y + z ) = ( + ` <. y , z >. )
176 174 175 48 3eltr4g 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> ( y + z ) e. ran P )
177 62 adantlr 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> y e. RR )
178 177 recnd 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> y e. CC )
179 138 adantr 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> z e. CC )
180 178 179 pncand 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> ( ( y + z ) - z ) = y )
181 180 eqcomd 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> y = ( ( y + z ) - z ) )
182 oveq1 
 |-  ( v = ( y + z ) -> ( v - z ) = ( ( y + z ) - z ) )
183 182 rspceeqv 
 |-  ( ( ( y + z ) e. ran P /\ y = ( ( y + z ) - z ) ) -> E. v e. ran P y = ( v - z ) )
184 176 181 183 syl2anc 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> E. v e. ran P y = ( v - z ) )
185 184 ralrimiva 
 |-  ( ( ph /\ z e. ran G ) -> A. y e. ran F E. v e. ran P y = ( v - z ) )
186 ssabral 
 |-  ( ran F C_ { y | E. v e. ran P y = ( v - z ) } <-> A. y e. ran F E. v e. ran P y = ( v - z ) )
187 185 186 sylibr 
 |-  ( ( ph /\ z e. ran G ) -> ran F C_ { y | E. v e. ran P y = ( v - z ) } )
188 146 rnmpt 
 |-  ran ( v e. ran P |-> ( v - z ) ) = { y | E. v e. ran P y = ( v - z ) }
189 187 188 sseqtrrdi 
 |-  ( ( ph /\ z e. ran G ) -> ran F C_ ran ( v e. ran P |-> ( v - z ) ) )
190 63 adantr 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> z e. RR )
191 177 190 readdcld 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> ( y + z ) e. RR )
192 104 ad2antrr 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> I : ( RR X. RR ) --> RR )
193 192 177 190 fovrnd 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> ( y I z ) e. RR )
194 191 193 remulcld 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> ( ( y + z ) x. ( y I z ) ) e. RR )
195 194 recnd 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> ( ( y + z ) x. ( y I z ) ) e. CC )
196 152 ssdifd 
 |-  ( ( ph /\ z e. ran G ) -> ( ran ( v e. ran P |-> ( v - z ) ) \ ran F ) C_ ( RR \ ran F ) )
197 196 sselda 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ( ran ( v e. ran P |-> ( v - z ) ) \ ran F ) ) -> y e. ( RR \ ran F ) )
198 eldifi 
 |-  ( y e. ( RR \ ran F ) -> y e. RR )
199 198 ad2antrl 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( y e. ( RR \ ran F ) /\ -. ( y = 0 /\ z = 0 ) ) ) -> y e. RR )
200 63 adantr 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( y e. ( RR \ ran F ) /\ -. ( y = 0 /\ z = 0 ) ) ) -> z e. RR )
201 simprr 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( y e. ( RR \ ran F ) /\ -. ( y = 0 /\ z = 0 ) ) ) -> -. ( y = 0 /\ z = 0 ) )
202 1 2 3 itg1addlem3 
 |-  ( ( ( y e. RR /\ z e. RR ) /\ -. ( y = 0 /\ z = 0 ) ) -> ( y I z ) = ( vol ` ( ( `' F " { y } ) i^i ( `' G " { z } ) ) ) )
203 199 200 201 202 syl21anc 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( y e. ( RR \ ran F ) /\ -. ( y = 0 /\ z = 0 ) ) ) -> ( y I z ) = ( vol ` ( ( `' F " { y } ) i^i ( `' G " { z } ) ) ) )
204 inss1 
 |-  ( ( `' F " { y } ) i^i ( `' G " { z } ) ) C_ ( `' F " { y } )
205 eldifn 
 |-  ( y e. ( RR \ ran F ) -> -. y e. ran F )
206 205 ad2antrl 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( y e. ( RR \ ran F ) /\ -. ( y = 0 /\ z = 0 ) ) ) -> -. y e. ran F )
207 vex 
 |-  v e. _V
208 207 eliniseg 
 |-  ( y e. _V -> ( v e. ( `' F " { y } ) <-> v F y ) )
209 208 elv 
 |-  ( v e. ( `' F " { y } ) <-> v F y )
210 vex 
 |-  y e. _V
211 207 210 brelrn 
 |-  ( v F y -> y e. ran F )
212 209 211 sylbi 
 |-  ( v e. ( `' F " { y } ) -> y e. ran F )
213 206 212 nsyl 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( y e. ( RR \ ran F ) /\ -. ( y = 0 /\ z = 0 ) ) ) -> -. v e. ( `' F " { y } ) )
214 213 pm2.21d 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( y e. ( RR \ ran F ) /\ -. ( y = 0 /\ z = 0 ) ) ) -> ( v e. ( `' F " { y } ) -> v e. (/) ) )
215 214 ssrdv 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( y e. ( RR \ ran F ) /\ -. ( y = 0 /\ z = 0 ) ) ) -> ( `' F " { y } ) C_ (/) )
216 204 215 sstrid 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( y e. ( RR \ ran F ) /\ -. ( y = 0 /\ z = 0 ) ) ) -> ( ( `' F " { y } ) i^i ( `' G " { z } ) ) C_ (/) )
217 ss0 
 |-  ( ( ( `' F " { y } ) i^i ( `' G " { z } ) ) C_ (/) -> ( ( `' F " { y } ) i^i ( `' G " { z } ) ) = (/) )
218 216 217 syl 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( y e. ( RR \ ran F ) /\ -. ( y = 0 /\ z = 0 ) ) ) -> ( ( `' F " { y } ) i^i ( `' G " { z } ) ) = (/) )
219 218 fveq2d 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( y e. ( RR \ ran F ) /\ -. ( y = 0 /\ z = 0 ) ) ) -> ( vol ` ( ( `' F " { y } ) i^i ( `' G " { z } ) ) ) = ( vol ` (/) ) )
220 0mbl 
 |-  (/) e. dom vol
221 mblvol 
 |-  ( (/) e. dom vol -> ( vol ` (/) ) = ( vol* ` (/) ) )
222 220 221 ax-mp 
 |-  ( vol ` (/) ) = ( vol* ` (/) )
223 ovol0 
 |-  ( vol* ` (/) ) = 0
224 222 223 eqtri 
 |-  ( vol ` (/) ) = 0
225 219 224 eqtrdi 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( y e. ( RR \ ran F ) /\ -. ( y = 0 /\ z = 0 ) ) ) -> ( vol ` ( ( `' F " { y } ) i^i ( `' G " { z } ) ) ) = 0 )
226 203 225 eqtrd 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( y e. ( RR \ ran F ) /\ -. ( y = 0 /\ z = 0 ) ) ) -> ( y I z ) = 0 )
227 226 oveq2d 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( y e. ( RR \ ran F ) /\ -. ( y = 0 /\ z = 0 ) ) ) -> ( ( y + z ) x. ( y I z ) ) = ( ( y + z ) x. 0 ) )
228 199 200 readdcld 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( y e. ( RR \ ran F ) /\ -. ( y = 0 /\ z = 0 ) ) ) -> ( y + z ) e. RR )
229 228 recnd 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( y e. ( RR \ ran F ) /\ -. ( y = 0 /\ z = 0 ) ) ) -> ( y + z ) e. CC )
230 229 mul01d 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( y e. ( RR \ ran F ) /\ -. ( y = 0 /\ z = 0 ) ) ) -> ( ( y + z ) x. 0 ) = 0 )
231 227 230 eqtrd 
 |-  ( ( ( ph /\ z e. ran G ) /\ ( y e. ( RR \ ran F ) /\ -. ( y = 0 /\ z = 0 ) ) ) -> ( ( y + z ) x. ( y I z ) ) = 0 )
232 231 expr 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ( RR \ ran F ) ) -> ( -. ( y = 0 /\ z = 0 ) -> ( ( y + z ) x. ( y I z ) ) = 0 ) )
233 oveq12 
 |-  ( ( y = 0 /\ z = 0 ) -> ( y + z ) = ( 0 + 0 ) )
234 233 98 eqtrdi 
 |-  ( ( y = 0 /\ z = 0 ) -> ( y + z ) = 0 )
235 oveq12 
 |-  ( ( y = 0 /\ z = 0 ) -> ( y I z ) = ( 0 I 0 ) )
236 0re 
 |-  0 e. RR
237 iftrue 
 |-  ( ( i = 0 /\ j = 0 ) -> if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) = 0 )
238 c0ex 
 |-  0 e. _V
239 237 3 238 ovmpoa 
 |-  ( ( 0 e. RR /\ 0 e. RR ) -> ( 0 I 0 ) = 0 )
240 236 236 239 mp2an 
 |-  ( 0 I 0 ) = 0
241 235 240 eqtrdi 
 |-  ( ( y = 0 /\ z = 0 ) -> ( y I z ) = 0 )
242 234 241 oveq12d 
 |-  ( ( y = 0 /\ z = 0 ) -> ( ( y + z ) x. ( y I z ) ) = ( 0 x. 0 ) )
243 0cn 
 |-  0 e. CC
244 243 mul01i 
 |-  ( 0 x. 0 ) = 0
245 242 244 eqtrdi 
 |-  ( ( y = 0 /\ z = 0 ) -> ( ( y + z ) x. ( y I z ) ) = 0 )
246 232 245 pm2.61d2 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ( RR \ ran F ) ) -> ( ( y + z ) x. ( y I z ) ) = 0 )
247 197 246 syldan 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ( ran ( v e. ran P |-> ( v - z ) ) \ ran F ) ) -> ( ( y + z ) x. ( y I z ) ) = 0 )
248 f1ofo 
 |-  ( ( v e. ran P |-> ( v - z ) ) : ran P -1-1-onto-> ran ( v e. ran P |-> ( v - z ) ) -> ( v e. ran P |-> ( v - z ) ) : ran P -onto-> ran ( v e. ran P |-> ( v - z ) ) )
249 144 248 syl 
 |-  ( ( ph /\ z e. ran G ) -> ( v e. ran P |-> ( v - z ) ) : ran P -onto-> ran ( v e. ran P |-> ( v - z ) ) )
250 fofi 
 |-  ( ( ran P e. Fin /\ ( v e. ran P |-> ( v - z ) ) : ran P -onto-> ran ( v e. ran P |-> ( v - z ) ) ) -> ran ( v e. ran P |-> ( v - z ) ) e. Fin )
251 127 249 250 syl2anc 
 |-  ( ( ph /\ z e. ran G ) -> ran ( v e. ran P |-> ( v - z ) ) e. Fin )
252 189 195 247 251 fsumss 
 |-  ( ( ph /\ z e. ran G ) -> sum_ y e. ran F ( ( y + z ) x. ( y I z ) ) = sum_ y e. ran ( v e. ran P |-> ( v - z ) ) ( ( y + z ) x. ( y I z ) ) )
253 34 a1i 
 |-  ( ( ph /\ z e. ran G ) -> ( ran P \ { 0 } ) C_ ran P )
254 120 an32s 
 |-  ( ( ( ph /\ z e. ran G ) /\ w e. ( ran P \ { 0 } ) ) -> ( w x. ( ( w - z ) I z ) ) e. CC )
255 dfin4 
 |-  ( ran P i^i { 0 } ) = ( ran P \ ( ran P \ { 0 } ) )
256 inss2 
 |-  ( ran P i^i { 0 } ) C_ { 0 }
257 255 256 eqsstrri 
 |-  ( ran P \ ( ran P \ { 0 } ) ) C_ { 0 }
258 257 sseli 
 |-  ( w e. ( ran P \ ( ran P \ { 0 } ) ) -> w e. { 0 } )
259 elsni 
 |-  ( w e. { 0 } -> w = 0 )
260 259 adantl 
 |-  ( ( ( ph /\ z e. ran G ) /\ w e. { 0 } ) -> w = 0 )
261 260 oveq1d 
 |-  ( ( ( ph /\ z e. ran G ) /\ w e. { 0 } ) -> ( w x. ( ( w - z ) I z ) ) = ( 0 x. ( ( w - z ) I z ) ) )
262 104 ad2antrr 
 |-  ( ( ( ph /\ z e. ran G ) /\ w e. { 0 } ) -> I : ( RR X. RR ) --> RR )
263 260 236 eqeltrdi 
 |-  ( ( ( ph /\ z e. ran G ) /\ w e. { 0 } ) -> w e. RR )
264 63 adantr 
 |-  ( ( ( ph /\ z e. ran G ) /\ w e. { 0 } ) -> z e. RR )
265 263 264 resubcld 
 |-  ( ( ( ph /\ z e. ran G ) /\ w e. { 0 } ) -> ( w - z ) e. RR )
266 262 265 264 fovrnd 
 |-  ( ( ( ph /\ z e. ran G ) /\ w e. { 0 } ) -> ( ( w - z ) I z ) e. RR )
267 266 recnd 
 |-  ( ( ( ph /\ z e. ran G ) /\ w e. { 0 } ) -> ( ( w - z ) I z ) e. CC )
268 267 mul02d 
 |-  ( ( ( ph /\ z e. ran G ) /\ w e. { 0 } ) -> ( 0 x. ( ( w - z ) I z ) ) = 0 )
269 261 268 eqtrd 
 |-  ( ( ( ph /\ z e. ran G ) /\ w e. { 0 } ) -> ( w x. ( ( w - z ) I z ) ) = 0 )
270 258 269 sylan2 
 |-  ( ( ( ph /\ z e. ran G ) /\ w e. ( ran P \ ( ran P \ { 0 } ) ) ) -> ( w x. ( ( w - z ) I z ) ) = 0 )
271 253 254 270 127 fsumss 
 |-  ( ( ph /\ z e. ran G ) -> sum_ w e. ( ran P \ { 0 } ) ( w x. ( ( w - z ) I z ) ) = sum_ w e. ran P ( w x. ( ( w - z ) I z ) ) )
272 167 252 271 3eqtr4d 
 |-  ( ( ph /\ z e. ran G ) -> sum_ y e. ran F ( ( y + z ) x. ( y I z ) ) = sum_ w e. ( ran P \ { 0 } ) ( w x. ( ( w - z ) I z ) ) )
273 272 sumeq2dv 
 |-  ( ph -> sum_ z e. ran G sum_ y e. ran F ( ( y + z ) x. ( y I z ) ) = sum_ z e. ran G sum_ w e. ( ran P \ { 0 } ) ( w x. ( ( w - z ) I z ) ) )
274 195 anasss 
 |-  ( ( ph /\ ( z e. ran G /\ y e. ran F ) ) -> ( ( y + z ) x. ( y I z ) ) e. CC )
275 9 7 274 fsumcom 
 |-  ( ph -> sum_ z e. ran G sum_ y e. ran F ( ( y + z ) x. ( y I z ) ) = sum_ y e. ran F sum_ z e. ran G ( ( y + z ) x. ( y I z ) ) )
276 123 273 275 3eqtr2d 
 |-  ( ph -> ( S.1 ` ( F oF + G ) ) = sum_ y e. ran F sum_ z e. ran G ( ( y + z ) x. ( y I z ) ) )