Metamath Proof Explorer


Theorem itg1addlem4OLD

Description: Obsolete version of itg1addlem4 . (Contributed by Mario Carneiro, 28-Jun-2014) (Proof modification is discouraged.) (New usage is discouraged.)

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