Metamath Proof Explorer

Theorem itg1addlem4

Description: Lemma for itg1add . (Contributed by Mario Carneiro, 28-Jun-2014) (Proof shortened by SN, 3-Oct-2024)

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