Metamath Proof Explorer

Theorem itg1addlem5

Description: Lemma for itg1add . (Contributed by Mario Carneiro, 27-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 itg1addlem5 
|- ( ph -> ( S.1 ` ( F oF + G ) ) = ( ( S.1 ` F ) + ( S.1 ` G ) ) )

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 i1frn 
 |-  ( F e. dom S.1 -> ran F e. Fin )
6 1 5 syl 
 |-  ( ph -> ran F e. Fin )
7 i1frn 
 |-  ( G e. dom S.1 -> ran G e. Fin )
8 2 7 syl 
 |-  ( ph -> ran G e. Fin )
9 8 adantr 
 |-  ( ( ph /\ y e. ran F ) -> ran G e. Fin )
10 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
11 1 10 syl 
 |-  ( ph -> F : RR --> RR )
12 11 frnd 
 |-  ( ph -> ran F C_ RR )
13 12 sselda 
 |-  ( ( ph /\ y e. ran F ) -> y e. RR )
14 13 adantr 
 |-  ( ( ( ph /\ y e. ran F ) /\ z e. ran G ) -> y e. RR )
15 14 recnd 
 |-  ( ( ( ph /\ y e. ran F ) /\ z e. ran G ) -> y e. CC )
16 1 2 3 itg1addlem2 
 |-  ( ph -> I : ( RR X. RR ) --> RR )
17 16 ad2antrr 
 |-  ( ( ( ph /\ y e. ran F ) /\ z e. ran G ) -> I : ( RR X. RR ) --> RR )
18 i1ff 
 |-  ( G e. dom S.1 -> G : RR --> RR )
19 2 18 syl 
 |-  ( ph -> G : RR --> RR )
20 19 frnd 
 |-  ( ph -> ran G C_ RR )
21 20 sselda 
 |-  ( ( ph /\ z e. ran G ) -> z e. RR )
22 21 adantlr 
 |-  ( ( ( ph /\ y e. ran F ) /\ z e. ran G ) -> z e. RR )
23 17 14 22 fovrnd 
 |-  ( ( ( ph /\ y e. ran F ) /\ z e. ran G ) -> ( y I z ) e. RR )
24 23 recnd 
 |-  ( ( ( ph /\ y e. ran F ) /\ z e. ran G ) -> ( y I z ) e. CC )
25 15 24 mulcld 
 |-  ( ( ( ph /\ y e. ran F ) /\ z e. ran G ) -> ( y x. ( y I z ) ) e. CC )
26 9 25 fsumcl 
 |-  ( ( ph /\ y e. ran F ) -> sum_ z e. ran G ( y x. ( y I z ) ) e. CC )
27 22 recnd 
 |-  ( ( ( ph /\ y e. ran F ) /\ z e. ran G ) -> z e. CC )
28 27 24 mulcld 
 |-  ( ( ( ph /\ y e. ran F ) /\ z e. ran G ) -> ( z x. ( y I z ) ) e. CC )
29 9 28 fsumcl 
 |-  ( ( ph /\ y e. ran F ) -> sum_ z e. ran G ( z x. ( y I z ) ) e. CC )
30 6 26 29 fsumadd 
 |-  ( ph -> sum_ y e. ran F ( sum_ z e. ran G ( y x. ( y I z ) ) + sum_ z e. ran G ( z x. ( y I z ) ) ) = ( sum_ y e. ran F sum_ z e. ran G ( y x. ( y I z ) ) + sum_ y e. ran F sum_ z e. ran G ( z x. ( y I z ) ) ) )
31 1 2 3 4 itg1addlem4 
 |-  ( ph -> ( S.1 ` ( F oF + G ) ) = sum_ y e. ran F sum_ z e. ran G ( ( y + z ) x. ( y I z ) ) )
32 15 27 24 adddird 
 |-  ( ( ( ph /\ y e. ran F ) /\ z e. ran G ) -> ( ( y + z ) x. ( y I z ) ) = ( ( y x. ( y I z ) ) + ( z x. ( y I z ) ) ) )
33 32 sumeq2dv 
 |-  ( ( ph /\ y e. ran F ) -> sum_ z e. ran G ( ( y + z ) x. ( y I z ) ) = sum_ z e. ran G ( ( y x. ( y I z ) ) + ( z x. ( y I z ) ) ) )
34 9 25 28 fsumadd 
 |-  ( ( ph /\ y e. ran F ) -> sum_ z e. ran G ( ( y x. ( y I z ) ) + ( z x. ( y I z ) ) ) = ( sum_ z e. ran G ( y x. ( y I z ) ) + sum_ z e. ran G ( z x. ( y I z ) ) ) )
35 33 34 eqtrd 
 |-  ( ( ph /\ y e. ran F ) -> sum_ z e. ran G ( ( y + z ) x. ( y I z ) ) = ( sum_ z e. ran G ( y x. ( y I z ) ) + sum_ z e. ran G ( z x. ( y I z ) ) ) )
36 35 sumeq2dv 
 |-  ( ph -> sum_ y e. ran F sum_ z e. ran G ( ( y + z ) x. ( y I z ) ) = sum_ y e. ran F ( sum_ z e. ran G ( y x. ( y I z ) ) + sum_ z e. ran G ( z x. ( y I z ) ) ) )
37 31 36 eqtrd 
 |-  ( ph -> ( S.1 ` ( F oF + G ) ) = sum_ y e. ran F ( sum_ z e. ran G ( y x. ( y I z ) ) + sum_ z e. ran G ( z x. ( y I z ) ) ) )
38 itg1val 
 |-  ( F e. dom S.1 -> ( S.1 ` F ) = sum_ y e. ( ran F \ { 0 } ) ( y x. ( vol ` ( `' F " { y } ) ) ) )
39 1 38 syl 
 |-  ( ph -> ( S.1 ` F ) = sum_ y e. ( ran F \ { 0 } ) ( y x. ( vol ` ( `' F " { y } ) ) ) )
40 19 adantr 
 |-  ( ( ph /\ y e. ( ran F \ { 0 } ) ) -> G : RR --> RR )
41 8 adantr 
 |-  ( ( ph /\ y e. ( ran F \ { 0 } ) ) -> ran G e. Fin )
42 inss2 
 |-  ( ( `' F " { y } ) i^i ( `' G " { z } ) ) C_ ( `' G " { z } )
43 42 a1i 
 |-  ( ( ( ph /\ y e. ( ran F \ { 0 } ) ) /\ z e. ran G ) -> ( ( `' F " { y } ) i^i ( `' G " { z } ) ) C_ ( `' G " { z } ) )
44 i1fima 
 |-  ( F e. dom S.1 -> ( `' F " { y } ) e. dom vol )
45 1 44 syl 
 |-  ( ph -> ( `' F " { y } ) e. dom vol )
46 45 ad2antrr 
 |-  ( ( ( ph /\ y e. ( ran F \ { 0 } ) ) /\ z e. ran G ) -> ( `' F " { y } ) e. dom vol )
47 i1fima 
 |-  ( G e. dom S.1 -> ( `' G " { z } ) e. dom vol )
48 2 47 syl 
 |-  ( ph -> ( `' G " { z } ) e. dom vol )
49 48 ad2antrr 
 |-  ( ( ( ph /\ y e. ( ran F \ { 0 } ) ) /\ z e. ran G ) -> ( `' G " { z } ) e. dom vol )
50 inmbl 
 |-  ( ( ( `' F " { y } ) e. dom vol /\ ( `' G " { z } ) e. dom vol ) -> ( ( `' F " { y } ) i^i ( `' G " { z } ) ) e. dom vol )
51 46 49 50 syl2anc 
 |-  ( ( ( ph /\ y e. ( ran F \ { 0 } ) ) /\ z e. ran G ) -> ( ( `' F " { y } ) i^i ( `' G " { z } ) ) e. dom vol )
52 12 ssdifssd 
 |-  ( ph -> ( ran F \ { 0 } ) C_ RR )
53 52 sselda 
 |-  ( ( ph /\ y e. ( ran F \ { 0 } ) ) -> y e. RR )
54 53 adantr 
 |-  ( ( ( ph /\ y e. ( ran F \ { 0 } ) ) /\ z e. ran G ) -> y e. RR )
55 20 adantr 
 |-  ( ( ph /\ y e. ( ran F \ { 0 } ) ) -> ran G C_ RR )
56 55 sselda 
 |-  ( ( ( ph /\ y e. ( ran F \ { 0 } ) ) /\ z e. ran G ) -> z e. RR )
57 eldifsni 
 |-  ( y e. ( ran F \ { 0 } ) -> y =/= 0 )
58 57 ad2antlr 
 |-  ( ( ( ph /\ y e. ( ran F \ { 0 } ) ) /\ z e. ran G ) -> y =/= 0 )
59 simpl 
 |-  ( ( y = 0 /\ z = 0 ) -> y = 0 )
60 59 necon3ai 
 |-  ( y =/= 0 -> -. ( y = 0 /\ z = 0 ) )
61 58 60 syl 
 |-  ( ( ( ph /\ y e. ( ran F \ { 0 } ) ) /\ z e. ran G ) -> -. ( y = 0 /\ z = 0 ) )
62 1 2 3 itg1addlem3 
 |-  ( ( ( y e. RR /\ z e. RR ) /\ -. ( y = 0 /\ z = 0 ) ) -> ( y I z ) = ( vol ` ( ( `' F " { y } ) i^i ( `' G " { z } ) ) ) )
63 54 56 61 62 syl21anc 
 |-  ( ( ( ph /\ y e. ( ran F \ { 0 } ) ) /\ z e. ran G ) -> ( y I z ) = ( vol ` ( ( `' F " { y } ) i^i ( `' G " { z } ) ) ) )
64 16 ad2antrr 
 |-  ( ( ( ph /\ y e. ( ran F \ { 0 } ) ) /\ z e. ran G ) -> I : ( RR X. RR ) --> RR )
65 64 54 56 fovrnd 
 |-  ( ( ( ph /\ y e. ( ran F \ { 0 } ) ) /\ z e. ran G ) -> ( y I z ) e. RR )
66 63 65 eqeltrrd 
 |-  ( ( ( ph /\ y e. ( ran F \ { 0 } ) ) /\ z e. ran G ) -> ( vol ` ( ( `' F " { y } ) i^i ( `' G " { z } ) ) ) e. RR )
67 40 41 43 51 66 itg1addlem1 
 |-  ( ( ph /\ y e. ( ran F \ { 0 } ) ) -> ( vol ` U_ z e. ran G ( ( `' F " { y } ) i^i ( `' G " { z } ) ) ) = sum_ z e. ran G ( vol ` ( ( `' F " { y } ) i^i ( `' G " { z } ) ) ) )
68 iunin2 
 |-  U_ z e. ran G ( ( `' F " { y } ) i^i ( `' G " { z } ) ) = ( ( `' F " { y } ) i^i U_ z e. ran G ( `' G " { z } ) )
69 1 adantr 
 |-  ( ( ph /\ y e. ( ran F \ { 0 } ) ) -> F e. dom S.1 )
70 69 44 syl 
 |-  ( ( ph /\ y e. ( ran F \ { 0 } ) ) -> ( `' F " { y } ) e. dom vol )
71 mblss 
 |-  ( ( `' F " { y } ) e. dom vol -> ( `' F " { y } ) C_ RR )
72 70 71 syl 
 |-  ( ( ph /\ y e. ( ran F \ { 0 } ) ) -> ( `' F " { y } ) C_ RR )
73 iunid 
 |-  U_ z e. ran G { z } = ran G
74 73 imaeq2i 
 |-  ( `' G " U_ z e. ran G { z } ) = ( `' G " ran G )
75 imaiun 
 |-  ( `' G " U_ z e. ran G { z } ) = U_ z e. ran G ( `' G " { z } )
76 cnvimarndm 
 |-  ( `' G " ran G ) = dom G
77 74 75 76 3eqtr3i 
 |-  U_ z e. ran G ( `' G " { z } ) = dom G
78 40 fdmd 
 |-  ( ( ph /\ y e. ( ran F \ { 0 } ) ) -> dom G = RR )
79 77 78 syl5eq 
 |-  ( ( ph /\ y e. ( ran F \ { 0 } ) ) -> U_ z e. ran G ( `' G " { z } ) = RR )
80 72 79 sseqtrrd 
 |-  ( ( ph /\ y e. ( ran F \ { 0 } ) ) -> ( `' F " { y } ) C_ U_ z e. ran G ( `' G " { z } ) )
81 df-ss 
 |-  ( ( `' F " { y } ) C_ U_ z e. ran G ( `' G " { z } ) <-> ( ( `' F " { y } ) i^i U_ z e. ran G ( `' G " { z } ) ) = ( `' F " { y } ) )
82 80 81 sylib 
 |-  ( ( ph /\ y e. ( ran F \ { 0 } ) ) -> ( ( `' F " { y } ) i^i U_ z e. ran G ( `' G " { z } ) ) = ( `' F " { y } ) )
83 68 82 eqtr2id 
 |-  ( ( ph /\ y e. ( ran F \ { 0 } ) ) -> ( `' F " { y } ) = U_ z e. ran G ( ( `' F " { y } ) i^i ( `' G " { z } ) ) )
84 83 fveq2d 
 |-  ( ( ph /\ y e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' F " { y } ) ) = ( vol ` U_ z e. ran G ( ( `' F " { y } ) i^i ( `' G " { z } ) ) ) )
85 63 sumeq2dv 
 |-  ( ( ph /\ y e. ( ran F \ { 0 } ) ) -> sum_ z e. ran G ( y I z ) = sum_ z e. ran G ( vol ` ( ( `' F " { y } ) i^i ( `' G " { z } ) ) ) )
86 67 84 85 3eqtr4d 
 |-  ( ( ph /\ y e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' F " { y } ) ) = sum_ z e. ran G ( y I z ) )
87 86 oveq2d 
 |-  ( ( ph /\ y e. ( ran F \ { 0 } ) ) -> ( y x. ( vol ` ( `' F " { y } ) ) ) = ( y x. sum_ z e. ran G ( y I z ) ) )
88 53 recnd 
 |-  ( ( ph /\ y e. ( ran F \ { 0 } ) ) -> y e. CC )
89 65 recnd 
 |-  ( ( ( ph /\ y e. ( ran F \ { 0 } ) ) /\ z e. ran G ) -> ( y I z ) e. CC )
90 41 88 89 fsummulc2 
 |-  ( ( ph /\ y e. ( ran F \ { 0 } ) ) -> ( y x. sum_ z e. ran G ( y I z ) ) = sum_ z e. ran G ( y x. ( y I z ) ) )
91 87 90 eqtrd 
 |-  ( ( ph /\ y e. ( ran F \ { 0 } ) ) -> ( y x. ( vol ` ( `' F " { y } ) ) ) = sum_ z e. ran G ( y x. ( y I z ) ) )
92 91 sumeq2dv 
 |-  ( ph -> sum_ y e. ( ran F \ { 0 } ) ( y x. ( vol ` ( `' F " { y } ) ) ) = sum_ y e. ( ran F \ { 0 } ) sum_ z e. ran G ( y x. ( y I z ) ) )
93 difssd 
 |-  ( ph -> ( ran F \ { 0 } ) C_ ran F )
94 54 recnd 
 |-  ( ( ( ph /\ y e. ( ran F \ { 0 } ) ) /\ z e. ran G ) -> y e. CC )
95 94 89 mulcld 
 |-  ( ( ( ph /\ y e. ( ran F \ { 0 } ) ) /\ z e. ran G ) -> ( y x. ( y I z ) ) e. CC )
96 41 95 fsumcl 
 |-  ( ( ph /\ y e. ( ran F \ { 0 } ) ) -> sum_ z e. ran G ( y x. ( y I z ) ) e. CC )
97 dfin4 
 |-  ( ran F i^i { 0 } ) = ( ran F \ ( ran F \ { 0 } ) )
98 inss2 
 |-  ( ran F i^i { 0 } ) C_ { 0 }
99 97 98 eqsstrri 
 |-  ( ran F \ ( ran F \ { 0 } ) ) C_ { 0 }
100 99 sseli 
 |-  ( y e. ( ran F \ ( ran F \ { 0 } ) ) -> y e. { 0 } )
101 elsni 
 |-  ( y e. { 0 } -> y = 0 )
102 101 ad2antlr 
 |-  ( ( ( ph /\ y e. { 0 } ) /\ z e. ran G ) -> y = 0 )
103 102 oveq1d 
 |-  ( ( ( ph /\ y e. { 0 } ) /\ z e. ran G ) -> ( y x. ( y I z ) ) = ( 0 x. ( y I z ) ) )
104 16 ad2antrr 
 |-  ( ( ( ph /\ y e. { 0 } ) /\ z e. ran G ) -> I : ( RR X. RR ) --> RR )
105 0re 
 |-  0 e. RR
106 102 105 eqeltrdi 
 |-  ( ( ( ph /\ y e. { 0 } ) /\ z e. ran G ) -> y e. RR )
107 21 adantlr 
 |-  ( ( ( ph /\ y e. { 0 } ) /\ z e. ran G ) -> z e. RR )
108 104 106 107 fovrnd 
 |-  ( ( ( ph /\ y e. { 0 } ) /\ z e. ran G ) -> ( y I z ) e. RR )
109 108 recnd 
 |-  ( ( ( ph /\ y e. { 0 } ) /\ z e. ran G ) -> ( y I z ) e. CC )
110 109 mul02d 
 |-  ( ( ( ph /\ y e. { 0 } ) /\ z e. ran G ) -> ( 0 x. ( y I z ) ) = 0 )
111 103 110 eqtrd 
 |-  ( ( ( ph /\ y e. { 0 } ) /\ z e. ran G ) -> ( y x. ( y I z ) ) = 0 )
112 111 sumeq2dv 
 |-  ( ( ph /\ y e. { 0 } ) -> sum_ z e. ran G ( y x. ( y I z ) ) = sum_ z e. ran G 0 )
113 8 adantr 
 |-  ( ( ph /\ y e. { 0 } ) -> ran G e. Fin )
114 113 olcd 
 |-  ( ( ph /\ y e. { 0 } ) -> ( ran G C_ ( ZZ>= ` 0 ) \/ ran G e. Fin ) )
115 sumz 
 |-  ( ( ran G C_ ( ZZ>= ` 0 ) \/ ran G e. Fin ) -> sum_ z e. ran G 0 = 0 )
116 114 115 syl 
 |-  ( ( ph /\ y e. { 0 } ) -> sum_ z e. ran G 0 = 0 )
117 112 116 eqtrd 
 |-  ( ( ph /\ y e. { 0 } ) -> sum_ z e. ran G ( y x. ( y I z ) ) = 0 )
118 100 117 sylan2 
 |-  ( ( ph /\ y e. ( ran F \ ( ran F \ { 0 } ) ) ) -> sum_ z e. ran G ( y x. ( y I z ) ) = 0 )
119 93 96 118 6 fsumss 
 |-  ( ph -> sum_ y e. ( ran F \ { 0 } ) sum_ z e. ran G ( y x. ( y I z ) ) = sum_ y e. ran F sum_ z e. ran G ( y x. ( y I z ) ) )
120 39 92 119 3eqtrd 
 |-  ( ph -> ( S.1 ` F ) = sum_ y e. ran F sum_ z e. ran G ( y x. ( y I z ) ) )
121 itg1val 
 |-  ( G e. dom S.1 -> ( S.1 ` G ) = sum_ z e. ( ran G \ { 0 } ) ( z x. ( vol ` ( `' G " { z } ) ) ) )
122 2 121 syl 
 |-  ( ph -> ( S.1 ` G ) = sum_ z e. ( ran G \ { 0 } ) ( z x. ( vol ` ( `' G " { z } ) ) ) )
123 11 adantr 
 |-  ( ( ph /\ z e. ( ran G \ { 0 } ) ) -> F : RR --> RR )
124 6 adantr 
 |-  ( ( ph /\ z e. ( ran G \ { 0 } ) ) -> ran F e. Fin )
125 inss1 
 |-  ( ( `' F " { y } ) i^i ( `' G " { z } ) ) C_ ( `' F " { y } )
126 125 a1i 
 |-  ( ( ( ph /\ z e. ( ran G \ { 0 } ) ) /\ y e. ran F ) -> ( ( `' F " { y } ) i^i ( `' G " { z } ) ) C_ ( `' F " { y } ) )
127 45 ad2antrr 
 |-  ( ( ( ph /\ z e. ( ran G \ { 0 } ) ) /\ y e. ran F ) -> ( `' F " { y } ) e. dom vol )
128 48 ad2antrr 
 |-  ( ( ( ph /\ z e. ( ran G \ { 0 } ) ) /\ y e. ran F ) -> ( `' G " { z } ) e. dom vol )
129 127 128 50 syl2anc 
 |-  ( ( ( ph /\ z e. ( ran G \ { 0 } ) ) /\ y e. ran F ) -> ( ( `' F " { y } ) i^i ( `' G " { z } ) ) e. dom vol )
130 12 adantr 
 |-  ( ( ph /\ z e. ( ran G \ { 0 } ) ) -> ran F C_ RR )
131 130 sselda 
 |-  ( ( ( ph /\ z e. ( ran G \ { 0 } ) ) /\ y e. ran F ) -> y e. RR )
132 20 ssdifssd 
 |-  ( ph -> ( ran G \ { 0 } ) C_ RR )
133 132 sselda 
 |-  ( ( ph /\ z e. ( ran G \ { 0 } ) ) -> z e. RR )
134 133 adantr 
 |-  ( ( ( ph /\ z e. ( ran G \ { 0 } ) ) /\ y e. ran F ) -> z e. RR )
135 eldifsni 
 |-  ( z e. ( ran G \ { 0 } ) -> z =/= 0 )
136 135 ad2antlr 
 |-  ( ( ( ph /\ z e. ( ran G \ { 0 } ) ) /\ y e. ran F ) -> z =/= 0 )
137 simpr 
 |-  ( ( y = 0 /\ z = 0 ) -> z = 0 )
138 137 necon3ai 
 |-  ( z =/= 0 -> -. ( y = 0 /\ z = 0 ) )
139 136 138 syl 
 |-  ( ( ( ph /\ z e. ( ran G \ { 0 } ) ) /\ y e. ran F ) -> -. ( y = 0 /\ z = 0 ) )
140 131 134 139 62 syl21anc 
 |-  ( ( ( ph /\ z e. ( ran G \ { 0 } ) ) /\ y e. ran F ) -> ( y I z ) = ( vol ` ( ( `' F " { y } ) i^i ( `' G " { z } ) ) ) )
141 16 ad2antrr 
 |-  ( ( ( ph /\ z e. ( ran G \ { 0 } ) ) /\ y e. ran F ) -> I : ( RR X. RR ) --> RR )
142 141 131 134 fovrnd 
 |-  ( ( ( ph /\ z e. ( ran G \ { 0 } ) ) /\ y e. ran F ) -> ( y I z ) e. RR )
143 140 142 eqeltrrd 
 |-  ( ( ( ph /\ z e. ( ran G \ { 0 } ) ) /\ y e. ran F ) -> ( vol ` ( ( `' F " { y } ) i^i ( `' G " { z } ) ) ) e. RR )
144 123 124 126 129 143 itg1addlem1 
 |-  ( ( ph /\ z e. ( ran G \ { 0 } ) ) -> ( vol ` U_ y e. ran F ( ( `' F " { y } ) i^i ( `' G " { z } ) ) ) = sum_ y e. ran F ( vol ` ( ( `' F " { y } ) i^i ( `' G " { z } ) ) ) )
145 incom 
 |-  ( ( `' F " { y } ) i^i ( `' G " { z } ) ) = ( ( `' G " { z } ) i^i ( `' F " { y } ) )
146 145 a1i 
 |-  ( y e. ran F -> ( ( `' F " { y } ) i^i ( `' G " { z } ) ) = ( ( `' G " { z } ) i^i ( `' F " { y } ) ) )
147 146 iuneq2i 
 |-  U_ y e. ran F ( ( `' F " { y } ) i^i ( `' G " { z } ) ) = U_ y e. ran F ( ( `' G " { z } ) i^i ( `' F " { y } ) )
148 iunin2 
 |-  U_ y e. ran F ( ( `' G " { z } ) i^i ( `' F " { y } ) ) = ( ( `' G " { z } ) i^i U_ y e. ran F ( `' F " { y } ) )
149 147 148 eqtri 
 |-  U_ y e. ran F ( ( `' F " { y } ) i^i ( `' G " { z } ) ) = ( ( `' G " { z } ) i^i U_ y e. ran F ( `' F " { y } ) )
150 cnvimass 
 |-  ( `' G " { z } ) C_ dom G
151 19 fdmd 
 |-  ( ph -> dom G = RR )
152 151 adantr 
 |-  ( ( ph /\ z e. ( ran G \ { 0 } ) ) -> dom G = RR )
153 150 152 sseqtrid 
 |-  ( ( ph /\ z e. ( ran G \ { 0 } ) ) -> ( `' G " { z } ) C_ RR )
154 iunid 
 |-  U_ y e. ran F { y } = ran F
155 154 imaeq2i 
 |-  ( `' F " U_ y e. ran F { y } ) = ( `' F " ran F )
156 imaiun 
 |-  ( `' F " U_ y e. ran F { y } ) = U_ y e. ran F ( `' F " { y } )
157 cnvimarndm 
 |-  ( `' F " ran F ) = dom F
158 155 156 157 3eqtr3i 
 |-  U_ y e. ran F ( `' F " { y } ) = dom F
159 11 fdmd 
 |-  ( ph -> dom F = RR )
160 159 adantr 
 |-  ( ( ph /\ z e. ( ran G \ { 0 } ) ) -> dom F = RR )
161 158 160 syl5eq 
 |-  ( ( ph /\ z e. ( ran G \ { 0 } ) ) -> U_ y e. ran F ( `' F " { y } ) = RR )
162 153 161 sseqtrrd 
 |-  ( ( ph /\ z e. ( ran G \ { 0 } ) ) -> ( `' G " { z } ) C_ U_ y e. ran F ( `' F " { y } ) )
163 df-ss 
 |-  ( ( `' G " { z } ) C_ U_ y e. ran F ( `' F " { y } ) <-> ( ( `' G " { z } ) i^i U_ y e. ran F ( `' F " { y } ) ) = ( `' G " { z } ) )
164 162 163 sylib 
 |-  ( ( ph /\ z e. ( ran G \ { 0 } ) ) -> ( ( `' G " { z } ) i^i U_ y e. ran F ( `' F " { y } ) ) = ( `' G " { z } ) )
165 149 164 eqtr2id 
 |-  ( ( ph /\ z e. ( ran G \ { 0 } ) ) -> ( `' G " { z } ) = U_ y e. ran F ( ( `' F " { y } ) i^i ( `' G " { z } ) ) )
166 165 fveq2d 
 |-  ( ( ph /\ z e. ( ran G \ { 0 } ) ) -> ( vol ` ( `' G " { z } ) ) = ( vol ` U_ y e. ran F ( ( `' F " { y } ) i^i ( `' G " { z } ) ) ) )
167 140 sumeq2dv 
 |-  ( ( ph /\ z e. ( ran G \ { 0 } ) ) -> sum_ y e. ran F ( y I z ) = sum_ y e. ran F ( vol ` ( ( `' F " { y } ) i^i ( `' G " { z } ) ) ) )
168 144 166 167 3eqtr4d 
 |-  ( ( ph /\ z e. ( ran G \ { 0 } ) ) -> ( vol ` ( `' G " { z } ) ) = sum_ y e. ran F ( y I z ) )
169 168 oveq2d 
 |-  ( ( ph /\ z e. ( ran G \ { 0 } ) ) -> ( z x. ( vol ` ( `' G " { z } ) ) ) = ( z x. sum_ y e. ran F ( y I z ) ) )
170 133 recnd 
 |-  ( ( ph /\ z e. ( ran G \ { 0 } ) ) -> z e. CC )
171 142 recnd 
 |-  ( ( ( ph /\ z e. ( ran G \ { 0 } ) ) /\ y e. ran F ) -> ( y I z ) e. CC )
172 124 170 171 fsummulc2 
 |-  ( ( ph /\ z e. ( ran G \ { 0 } ) ) -> ( z x. sum_ y e. ran F ( y I z ) ) = sum_ y e. ran F ( z x. ( y I z ) ) )
173 169 172 eqtrd 
 |-  ( ( ph /\ z e. ( ran G \ { 0 } ) ) -> ( z x. ( vol ` ( `' G " { z } ) ) ) = sum_ y e. ran F ( z x. ( y I z ) ) )
174 173 sumeq2dv 
 |-  ( ph -> sum_ z e. ( ran G \ { 0 } ) ( z x. ( vol ` ( `' G " { z } ) ) ) = sum_ z e. ( ran G \ { 0 } ) sum_ y e. ran F ( z x. ( y I z ) ) )
175 difssd 
 |-  ( ph -> ( ran G \ { 0 } ) C_ ran G )
176 170 adantr 
 |-  ( ( ( ph /\ z e. ( ran G \ { 0 } ) ) /\ y e. ran F ) -> z e. CC )
177 176 171 mulcld 
 |-  ( ( ( ph /\ z e. ( ran G \ { 0 } ) ) /\ y e. ran F ) -> ( z x. ( y I z ) ) e. CC )
178 124 177 fsumcl 
 |-  ( ( ph /\ z e. ( ran G \ { 0 } ) ) -> sum_ y e. ran F ( z x. ( y I z ) ) e. CC )
179 dfin4 
 |-  ( ran G i^i { 0 } ) = ( ran G \ ( ran G \ { 0 } ) )
180 inss2 
 |-  ( ran G i^i { 0 } ) C_ { 0 }
181 179 180 eqsstrri 
 |-  ( ran G \ ( ran G \ { 0 } ) ) C_ { 0 }
182 181 sseli 
 |-  ( z e. ( ran G \ ( ran G \ { 0 } ) ) -> z e. { 0 } )
183 elsni 
 |-  ( z e. { 0 } -> z = 0 )
184 183 ad2antlr 
 |-  ( ( ( ph /\ z e. { 0 } ) /\ y e. ran F ) -> z = 0 )
185 184 oveq1d 
 |-  ( ( ( ph /\ z e. { 0 } ) /\ y e. ran F ) -> ( z x. ( y I z ) ) = ( 0 x. ( y I z ) ) )
186 16 ad2antrr 
 |-  ( ( ( ph /\ z e. { 0 } ) /\ y e. ran F ) -> I : ( RR X. RR ) --> RR )
187 13 adantlr 
 |-  ( ( ( ph /\ z e. { 0 } ) /\ y e. ran F ) -> y e. RR )
188 184 105 eqeltrdi 
 |-  ( ( ( ph /\ z e. { 0 } ) /\ y e. ran F ) -> z e. RR )
189 186 187 188 fovrnd 
 |-  ( ( ( ph /\ z e. { 0 } ) /\ y e. ran F ) -> ( y I z ) e. RR )
190 189 recnd 
 |-  ( ( ( ph /\ z e. { 0 } ) /\ y e. ran F ) -> ( y I z ) e. CC )
191 190 mul02d 
 |-  ( ( ( ph /\ z e. { 0 } ) /\ y e. ran F ) -> ( 0 x. ( y I z ) ) = 0 )
192 185 191 eqtrd 
 |-  ( ( ( ph /\ z e. { 0 } ) /\ y e. ran F ) -> ( z x. ( y I z ) ) = 0 )
193 192 sumeq2dv 
 |-  ( ( ph /\ z e. { 0 } ) -> sum_ y e. ran F ( z x. ( y I z ) ) = sum_ y e. ran F 0 )
194 6 adantr 
 |-  ( ( ph /\ z e. { 0 } ) -> ran F e. Fin )
195 194 olcd 
 |-  ( ( ph /\ z e. { 0 } ) -> ( ran F C_ ( ZZ>= ` 0 ) \/ ran F e. Fin ) )
196 sumz 
 |-  ( ( ran F C_ ( ZZ>= ` 0 ) \/ ran F e. Fin ) -> sum_ y e. ran F 0 = 0 )
197 195 196 syl 
 |-  ( ( ph /\ z e. { 0 } ) -> sum_ y e. ran F 0 = 0 )
198 193 197 eqtrd 
 |-  ( ( ph /\ z e. { 0 } ) -> sum_ y e. ran F ( z x. ( y I z ) ) = 0 )
199 182 198 sylan2 
 |-  ( ( ph /\ z e. ( ran G \ ( ran G \ { 0 } ) ) ) -> sum_ y e. ran F ( z x. ( y I z ) ) = 0 )
200 175 178 199 8 fsumss 
 |-  ( ph -> sum_ z e. ( ran G \ { 0 } ) sum_ y e. ran F ( z x. ( y I z ) ) = sum_ z e. ran G sum_ y e. ran F ( z x. ( y I z ) ) )
201 21 adantr 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> z e. RR )
202 201 recnd 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> z e. CC )
203 16 ad2antrr 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> I : ( RR X. RR ) --> RR )
204 12 adantr 
 |-  ( ( ph /\ z e. ran G ) -> ran F C_ RR )
205 204 sselda 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> y e. RR )
206 203 205 201 fovrnd 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> ( y I z ) e. RR )
207 206 recnd 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> ( y I z ) e. CC )
208 202 207 mulcld 
 |-  ( ( ( ph /\ z e. ran G ) /\ y e. ran F ) -> ( z x. ( y I z ) ) e. CC )
209 208 anasss 
 |-  ( ( ph /\ ( z e. ran G /\ y e. ran F ) ) -> ( z x. ( y I z ) ) e. CC )
210 8 6 209 fsumcom 
 |-  ( ph -> sum_ z e. ran G sum_ y e. ran F ( z x. ( y I z ) ) = sum_ y e. ran F sum_ z e. ran G ( z x. ( y I z ) ) )
211 200 210 eqtrd 
 |-  ( ph -> sum_ z e. ( ran G \ { 0 } ) sum_ y e. ran F ( z x. ( y I z ) ) = sum_ y e. ran F sum_ z e. ran G ( z x. ( y I z ) ) )
212 122 174 211 3eqtrd 
 |-  ( ph -> ( S.1 ` G ) = sum_ y e. ran F sum_ z e. ran G ( z x. ( y I z ) ) )
213 120 212 oveq12d 
 |-  ( ph -> ( ( S.1 ` F ) + ( S.1 ` G ) ) = ( sum_ y e. ran F sum_ z e. ran G ( y x. ( y I z ) ) + sum_ y e. ran F sum_ z e. ran G ( z x. ( y I z ) ) ) )
214 30 37 213 3eqtr4d 
 |-  ( ph -> ( S.1 ` ( F oF + G ) ) = ( ( S.1 ` F ) + ( S.1 ` G ) ) )