Metamath Proof Explorer


Theorem dvmptfprodlem

Description: Induction step for dvmptfprod . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses dvmptfprodlem.xph
|- F/ x ph
dvmptfprodlem.iph
|- F/ i ph
dvmptfprodlem.jph
|- F/ j ph
dvmptfprodlem.if
|- F/_ i F
dvmptfprodlem.jg
|- F/_ j G
dvmptfprodlem.a
|- ( ( ph /\ i e. I /\ x e. X ) -> A e. CC )
dvmptfprodlem.d
|- ( ph -> D e. Fin )
dvmptfprodlem.e
|- ( ph -> E e. _V )
dvmptfprodlem.db
|- ( ph -> -. E e. D )
dvmptfprodlem.ss
|- ( ph -> ( D u. { E } ) C_ I )
dvmptfprodlem.s
|- ( ph -> S e. { RR , CC } )
dvmptfprodlem.c
|- ( ( ( ph /\ x e. X ) /\ j e. D ) -> C e. CC )
dvmptfprodlem.dvp
|- ( ph -> ( S _D ( x e. X |-> prod_ i e. D A ) ) = ( x e. X |-> sum_ j e. D ( C x. prod_ i e. ( D \ { j } ) A ) ) )
dvmptfprodlem.14
|- ( ( ph /\ x e. X ) -> G e. CC )
dvmptfprodlem.dvf
|- ( ph -> ( S _D ( x e. X |-> F ) ) = ( x e. X |-> G ) )
dvmptfprodlem.f
|- ( i = E -> A = F )
dvmptfprodlem.cg
|- ( j = E -> C = G )
Assertion dvmptfprodlem
|- ( ph -> ( S _D ( x e. X |-> prod_ i e. ( D u. { E } ) A ) ) = ( x e. X |-> sum_ j e. ( D u. { E } ) ( C x. prod_ i e. ( ( D u. { E } ) \ { j } ) A ) ) )

Proof

Step Hyp Ref Expression
1 dvmptfprodlem.xph
 |-  F/ x ph
2 dvmptfprodlem.iph
 |-  F/ i ph
3 dvmptfprodlem.jph
 |-  F/ j ph
4 dvmptfprodlem.if
 |-  F/_ i F
5 dvmptfprodlem.jg
 |-  F/_ j G
6 dvmptfprodlem.a
 |-  ( ( ph /\ i e. I /\ x e. X ) -> A e. CC )
7 dvmptfprodlem.d
 |-  ( ph -> D e. Fin )
8 dvmptfprodlem.e
 |-  ( ph -> E e. _V )
9 dvmptfprodlem.db
 |-  ( ph -> -. E e. D )
10 dvmptfprodlem.ss
 |-  ( ph -> ( D u. { E } ) C_ I )
11 dvmptfprodlem.s
 |-  ( ph -> S e. { RR , CC } )
12 dvmptfprodlem.c
 |-  ( ( ( ph /\ x e. X ) /\ j e. D ) -> C e. CC )
13 dvmptfprodlem.dvp
 |-  ( ph -> ( S _D ( x e. X |-> prod_ i e. D A ) ) = ( x e. X |-> sum_ j e. D ( C x. prod_ i e. ( D \ { j } ) A ) ) )
14 dvmptfprodlem.14
 |-  ( ( ph /\ x e. X ) -> G e. CC )
15 dvmptfprodlem.dvf
 |-  ( ph -> ( S _D ( x e. X |-> F ) ) = ( x e. X |-> G ) )
16 dvmptfprodlem.f
 |-  ( i = E -> A = F )
17 dvmptfprodlem.cg
 |-  ( j = E -> C = G )
18 nfcv
 |-  F/_ i x
19 nfcv
 |-  F/_ i X
20 18 19 nfel
 |-  F/ i x e. X
21 2 20 nfan
 |-  F/ i ( ph /\ x e. X )
22 4 a1i
 |-  ( ( ph /\ x e. X ) -> F/_ i F )
23 snfi
 |-  { E } e. Fin
24 23 a1i
 |-  ( ph -> { E } e. Fin )
25 unfi
 |-  ( ( D e. Fin /\ { E } e. Fin ) -> ( D u. { E } ) e. Fin )
26 7 24 25 syl2anc
 |-  ( ph -> ( D u. { E } ) e. Fin )
27 26 adantr
 |-  ( ( ph /\ x e. X ) -> ( D u. { E } ) e. Fin )
28 simpll
 |-  ( ( ( ph /\ x e. X ) /\ i e. ( D u. { E } ) ) -> ph )
29 10 sselda
 |-  ( ( ph /\ i e. ( D u. { E } ) ) -> i e. I )
30 29 adantlr
 |-  ( ( ( ph /\ x e. X ) /\ i e. ( D u. { E } ) ) -> i e. I )
31 simplr
 |-  ( ( ( ph /\ x e. X ) /\ i e. ( D u. { E } ) ) -> x e. X )
32 28 30 31 6 syl3anc
 |-  ( ( ( ph /\ x e. X ) /\ i e. ( D u. { E } ) ) -> A e. CC )
33 snidg
 |-  ( E e. _V -> E e. { E } )
34 8 33 syl
 |-  ( ph -> E e. { E } )
35 elun2
 |-  ( E e. { E } -> E e. ( D u. { E } ) )
36 34 35 syl
 |-  ( ph -> E e. ( D u. { E } ) )
37 36 adantr
 |-  ( ( ph /\ x e. X ) -> E e. ( D u. { E } ) )
38 16 adantl
 |-  ( ( ( ph /\ x e. X ) /\ i = E ) -> A = F )
39 21 22 27 32 37 38 fprodsplit1f
 |-  ( ( ph /\ x e. X ) -> prod_ i e. ( D u. { E } ) A = ( F x. prod_ i e. ( ( D u. { E } ) \ { E } ) A ) )
40 difundir
 |-  ( ( D u. { E } ) \ { E } ) = ( ( D \ { E } ) u. ( { E } \ { E } ) )
41 40 a1i
 |-  ( ph -> ( ( D u. { E } ) \ { E } ) = ( ( D \ { E } ) u. ( { E } \ { E } ) ) )
42 difsn
 |-  ( -. E e. D -> ( D \ { E } ) = D )
43 9 42 syl
 |-  ( ph -> ( D \ { E } ) = D )
44 difid
 |-  ( { E } \ { E } ) = (/)
45 44 a1i
 |-  ( ph -> ( { E } \ { E } ) = (/) )
46 43 45 uneq12d
 |-  ( ph -> ( ( D \ { E } ) u. ( { E } \ { E } ) ) = ( D u. (/) ) )
47 un0
 |-  ( D u. (/) ) = D
48 47 a1i
 |-  ( ph -> ( D u. (/) ) = D )
49 41 46 48 3eqtrd
 |-  ( ph -> ( ( D u. { E } ) \ { E } ) = D )
50 49 prodeq1d
 |-  ( ph -> prod_ i e. ( ( D u. { E } ) \ { E } ) A = prod_ i e. D A )
51 50 oveq2d
 |-  ( ph -> ( F x. prod_ i e. ( ( D u. { E } ) \ { E } ) A ) = ( F x. prod_ i e. D A ) )
52 51 adantr
 |-  ( ( ph /\ x e. X ) -> ( F x. prod_ i e. ( ( D u. { E } ) \ { E } ) A ) = ( F x. prod_ i e. D A ) )
53 39 52 eqtrd
 |-  ( ( ph /\ x e. X ) -> prod_ i e. ( D u. { E } ) A = ( F x. prod_ i e. D A ) )
54 1 53 mpteq2da
 |-  ( ph -> ( x e. X |-> prod_ i e. ( D u. { E } ) A ) = ( x e. X |-> ( F x. prod_ i e. D A ) ) )
55 54 oveq2d
 |-  ( ph -> ( S _D ( x e. X |-> prod_ i e. ( D u. { E } ) A ) ) = ( S _D ( x e. X |-> ( F x. prod_ i e. D A ) ) ) )
56 10 36 sseldd
 |-  ( ph -> E e. I )
57 56 adantr
 |-  ( ( ph /\ x e. X ) -> E e. I )
58 simpl
 |-  ( ( ph /\ x e. X ) -> ph )
59 simpr
 |-  ( ( ph /\ x e. X ) -> x e. X )
60 58 57 59 3jca
 |-  ( ( ph /\ x e. X ) -> ( ph /\ E e. I /\ x e. X ) )
61 nfcv
 |-  F/_ i E
62 nfv
 |-  F/ i E e. I
63 2 62 20 nf3an
 |-  F/ i ( ph /\ E e. I /\ x e. X )
64 nfcv
 |-  F/_ i CC
65 4 64 nfel
 |-  F/ i F e. CC
66 63 65 nfim
 |-  F/ i ( ( ph /\ E e. I /\ x e. X ) -> F e. CC )
67 ancom
 |-  ( ( ( ph /\ x e. X ) /\ i = E ) <-> ( i = E /\ ( ph /\ x e. X ) ) )
68 67 imbi1i
 |-  ( ( ( ( ph /\ x e. X ) /\ i = E ) -> A = F ) <-> ( ( i = E /\ ( ph /\ x e. X ) ) -> A = F ) )
69 eqcom
 |-  ( A = F <-> F = A )
70 69 imbi2i
 |-  ( ( ( i = E /\ ( ph /\ x e. X ) ) -> A = F ) <-> ( ( i = E /\ ( ph /\ x e. X ) ) -> F = A ) )
71 68 70 bitri
 |-  ( ( ( ( ph /\ x e. X ) /\ i = E ) -> A = F ) <-> ( ( i = E /\ ( ph /\ x e. X ) ) -> F = A ) )
72 38 71 mpbi
 |-  ( ( i = E /\ ( ph /\ x e. X ) ) -> F = A )
73 72 3adantr2
 |-  ( ( i = E /\ ( ph /\ E e. I /\ x e. X ) ) -> F = A )
74 73 3adant2
 |-  ( ( i = E /\ ( ( ph /\ i e. I /\ x e. X ) -> A e. CC ) /\ ( ph /\ E e. I /\ x e. X ) ) -> F = A )
75 simp3
 |-  ( ( i = E /\ ( ( ph /\ i e. I /\ x e. X ) -> A e. CC ) /\ ( ph /\ E e. I /\ x e. X ) ) -> ( ph /\ E e. I /\ x e. X ) )
76 eleq1
 |-  ( i = E -> ( i e. I <-> E e. I ) )
77 76 3anbi2d
 |-  ( i = E -> ( ( ph /\ i e. I /\ x e. X ) <-> ( ph /\ E e. I /\ x e. X ) ) )
78 77 imbi1d
 |-  ( i = E -> ( ( ( ph /\ i e. I /\ x e. X ) -> A e. CC ) <-> ( ( ph /\ E e. I /\ x e. X ) -> A e. CC ) ) )
79 78 biimpa
 |-  ( ( i = E /\ ( ( ph /\ i e. I /\ x e. X ) -> A e. CC ) ) -> ( ( ph /\ E e. I /\ x e. X ) -> A e. CC ) )
80 79 3adant3
 |-  ( ( i = E /\ ( ( ph /\ i e. I /\ x e. X ) -> A e. CC ) /\ ( ph /\ E e. I /\ x e. X ) ) -> ( ( ph /\ E e. I /\ x e. X ) -> A e. CC ) )
81 75 80 mpd
 |-  ( ( i = E /\ ( ( ph /\ i e. I /\ x e. X ) -> A e. CC ) /\ ( ph /\ E e. I /\ x e. X ) ) -> A e. CC )
82 74 81 eqeltrd
 |-  ( ( i = E /\ ( ( ph /\ i e. I /\ x e. X ) -> A e. CC ) /\ ( ph /\ E e. I /\ x e. X ) ) -> F e. CC )
83 82 3exp
 |-  ( i = E -> ( ( ( ph /\ i e. I /\ x e. X ) -> A e. CC ) -> ( ( ph /\ E e. I /\ x e. X ) -> F e. CC ) ) )
84 6 2a1i
 |-  ( i = E -> ( ( ( ph /\ E e. I /\ x e. X ) -> F e. CC ) -> ( ( ph /\ i e. I /\ x e. X ) -> A e. CC ) ) )
85 83 84 impbid
 |-  ( i = E -> ( ( ( ph /\ i e. I /\ x e. X ) -> A e. CC ) <-> ( ( ph /\ E e. I /\ x e. X ) -> F e. CC ) ) )
86 61 66 85 6 vtoclgf
 |-  ( E e. I -> ( ( ph /\ E e. I /\ x e. X ) -> F e. CC ) )
87 57 60 86 sylc
 |-  ( ( ph /\ x e. X ) -> F e. CC )
88 58 7 syl
 |-  ( ( ph /\ x e. X ) -> D e. Fin )
89 58 adantr
 |-  ( ( ( ph /\ x e. X ) /\ i e. D ) -> ph )
90 10 adantr
 |-  ( ( ph /\ i e. D ) -> ( D u. { E } ) C_ I )
91 elun1
 |-  ( i e. D -> i e. ( D u. { E } ) )
92 91 adantl
 |-  ( ( ph /\ i e. D ) -> i e. ( D u. { E } ) )
93 90 92 sseldd
 |-  ( ( ph /\ i e. D ) -> i e. I )
94 93 adantlr
 |-  ( ( ( ph /\ x e. X ) /\ i e. D ) -> i e. I )
95 59 adantr
 |-  ( ( ( ph /\ x e. X ) /\ i e. D ) -> x e. X )
96 89 94 95 6 syl3anc
 |-  ( ( ( ph /\ x e. X ) /\ i e. D ) -> A e. CC )
97 21 88 96 fprodclf
 |-  ( ( ph /\ x e. X ) -> prod_ i e. D A e. CC )
98 nfv
 |-  F/ j x e. X
99 3 98 nfan
 |-  F/ j ( ph /\ x e. X )
100 diffi
 |-  ( D e. Fin -> ( D \ { j } ) e. Fin )
101 7 100 syl
 |-  ( ph -> ( D \ { j } ) e. Fin )
102 101 adantr
 |-  ( ( ph /\ x e. X ) -> ( D \ { j } ) e. Fin )
103 eldifi
 |-  ( i e. ( D \ { j } ) -> i e. D )
104 103 adantl
 |-  ( ( ( ph /\ x e. X ) /\ i e. ( D \ { j } ) ) -> i e. D )
105 104 96 syldan
 |-  ( ( ( ph /\ x e. X ) /\ i e. ( D \ { j } ) ) -> A e. CC )
106 21 102 105 fprodclf
 |-  ( ( ph /\ x e. X ) -> prod_ i e. ( D \ { j } ) A e. CC )
107 106 adantr
 |-  ( ( ( ph /\ x e. X ) /\ j e. D ) -> prod_ i e. ( D \ { j } ) A e. CC )
108 12 107 mulcld
 |-  ( ( ( ph /\ x e. X ) /\ j e. D ) -> ( C x. prod_ i e. ( D \ { j } ) A ) e. CC )
109 99 88 108 fsumclf
 |-  ( ( ph /\ x e. X ) -> sum_ j e. D ( C x. prod_ i e. ( D \ { j } ) A ) e. CC )
110 1 11 87 14 15 97 109 13 dvmptmulf
 |-  ( ph -> ( S _D ( x e. X |-> ( F x. prod_ i e. D A ) ) ) = ( x e. X |-> ( ( G x. prod_ i e. D A ) + ( sum_ j e. D ( C x. prod_ i e. ( D \ { j } ) A ) x. F ) ) ) )
111 nfcv
 |-  F/_ j x.
112 nfcv
 |-  F/_ j prod_ i e. ( ( D u. { E } ) \ { E } ) A
113 5 111 112 nfov
 |-  F/_ j ( G x. prod_ i e. ( ( D u. { E } ) \ { E } ) A )
114 58 8 syl
 |-  ( ( ph /\ x e. X ) -> E e. _V )
115 58 9 syl
 |-  ( ( ph /\ x e. X ) -> -. E e. D )
116 diffi
 |-  ( ( D u. { E } ) e. Fin -> ( ( D u. { E } ) \ { j } ) e. Fin )
117 26 116 syl
 |-  ( ph -> ( ( D u. { E } ) \ { j } ) e. Fin )
118 117 adantr
 |-  ( ( ph /\ x e. X ) -> ( ( D u. { E } ) \ { j } ) e. Fin )
119 eldifi
 |-  ( i e. ( ( D u. { E } ) \ { j } ) -> i e. ( D u. { E } ) )
120 119 adantl
 |-  ( ( ( ph /\ x e. X ) /\ i e. ( ( D u. { E } ) \ { j } ) ) -> i e. ( D u. { E } ) )
121 120 32 syldan
 |-  ( ( ( ph /\ x e. X ) /\ i e. ( ( D u. { E } ) \ { j } ) ) -> A e. CC )
122 21 118 121 fprodclf
 |-  ( ( ph /\ x e. X ) -> prod_ i e. ( ( D u. { E } ) \ { j } ) A e. CC )
123 122 adantr
 |-  ( ( ( ph /\ x e. X ) /\ j e. D ) -> prod_ i e. ( ( D u. { E } ) \ { j } ) A e. CC )
124 12 123 mulcld
 |-  ( ( ( ph /\ x e. X ) /\ j e. D ) -> ( C x. prod_ i e. ( ( D u. { E } ) \ { j } ) A ) e. CC )
125 sneq
 |-  ( j = E -> { j } = { E } )
126 125 difeq2d
 |-  ( j = E -> ( ( D u. { E } ) \ { j } ) = ( ( D u. { E } ) \ { E } ) )
127 126 prodeq1d
 |-  ( j = E -> prod_ i e. ( ( D u. { E } ) \ { j } ) A = prod_ i e. ( ( D u. { E } ) \ { E } ) A )
128 17 127 oveq12d
 |-  ( j = E -> ( C x. prod_ i e. ( ( D u. { E } ) \ { j } ) A ) = ( G x. prod_ i e. ( ( D u. { E } ) \ { E } ) A ) )
129 49 7 eqeltrd
 |-  ( ph -> ( ( D u. { E } ) \ { E } ) e. Fin )
130 129 adantr
 |-  ( ( ph /\ x e. X ) -> ( ( D u. { E } ) \ { E } ) e. Fin )
131 58 adantr
 |-  ( ( ( ph /\ x e. X ) /\ i e. ( ( D u. { E } ) \ { E } ) ) -> ph )
132 10 adantr
 |-  ( ( ph /\ i e. ( ( D u. { E } ) \ { E } ) ) -> ( D u. { E } ) C_ I )
133 eldifi
 |-  ( i e. ( ( D u. { E } ) \ { E } ) -> i e. ( D u. { E } ) )
134 133 adantl
 |-  ( ( ph /\ i e. ( ( D u. { E } ) \ { E } ) ) -> i e. ( D u. { E } ) )
135 132 134 sseldd
 |-  ( ( ph /\ i e. ( ( D u. { E } ) \ { E } ) ) -> i e. I )
136 135 adantlr
 |-  ( ( ( ph /\ x e. X ) /\ i e. ( ( D u. { E } ) \ { E } ) ) -> i e. I )
137 59 adantr
 |-  ( ( ( ph /\ x e. X ) /\ i e. ( ( D u. { E } ) \ { E } ) ) -> x e. X )
138 131 136 137 6 syl3anc
 |-  ( ( ( ph /\ x e. X ) /\ i e. ( ( D u. { E } ) \ { E } ) ) -> A e. CC )
139 21 130 138 fprodclf
 |-  ( ( ph /\ x e. X ) -> prod_ i e. ( ( D u. { E } ) \ { E } ) A e. CC )
140 14 139 mulcld
 |-  ( ( ph /\ x e. X ) -> ( G x. prod_ i e. ( ( D u. { E } ) \ { E } ) A ) e. CC )
141 99 113 88 114 115 124 128 140 fsumsplitsn
 |-  ( ( ph /\ x e. X ) -> sum_ j e. ( D u. { E } ) ( C x. prod_ i e. ( ( D u. { E } ) \ { j } ) A ) = ( sum_ j e. D ( C x. prod_ i e. ( ( D u. { E } ) \ { j } ) A ) + ( G x. prod_ i e. ( ( D u. { E } ) \ { E } ) A ) ) )
142 difundir
 |-  ( ( D u. { E } ) \ { j } ) = ( ( D \ { j } ) u. ( { E } \ { j } ) )
143 142 a1i
 |-  ( ( ph /\ j e. D ) -> ( ( D u. { E } ) \ { j } ) = ( ( D \ { j } ) u. ( { E } \ { j } ) ) )
144 nfv
 |-  F/ x j e. D
145 1 144 nfan
 |-  F/ x ( ph /\ j e. D )
146 elsni
 |-  ( x e. { E } -> x = E )
147 146 eqcomd
 |-  ( x e. { E } -> E = x )
148 147 adantr
 |-  ( ( x e. { E } /\ x = j ) -> E = x )
149 simpr
 |-  ( ( x e. { E } /\ x = j ) -> x = j )
150 eqidd
 |-  ( ( x e. { E } /\ x = j ) -> j = j )
151 148 149 150 3eqtrd
 |-  ( ( x e. { E } /\ x = j ) -> E = j )
152 151 adantll
 |-  ( ( ( ( ph /\ j e. D ) /\ x e. { E } ) /\ x = j ) -> E = j )
153 simpllr
 |-  ( ( ( ( ph /\ j e. D ) /\ x e. { E } ) /\ x = j ) -> j e. D )
154 152 153 eqeltrd
 |-  ( ( ( ( ph /\ j e. D ) /\ x e. { E } ) /\ x = j ) -> E e. D )
155 9 ad3antrrr
 |-  ( ( ( ( ph /\ j e. D ) /\ x e. { E } ) /\ x = j ) -> -. E e. D )
156 154 155 pm2.65da
 |-  ( ( ( ph /\ j e. D ) /\ x e. { E } ) -> -. x = j )
157 velsn
 |-  ( x e. { j } <-> x = j )
158 156 157 sylnibr
 |-  ( ( ( ph /\ j e. D ) /\ x e. { E } ) -> -. x e. { j } )
159 158 ex
 |-  ( ( ph /\ j e. D ) -> ( x e. { E } -> -. x e. { j } ) )
160 145 159 ralrimi
 |-  ( ( ph /\ j e. D ) -> A. x e. { E } -. x e. { j } )
161 disj
 |-  ( ( { E } i^i { j } ) = (/) <-> A. x e. { E } -. x e. { j } )
162 160 161 sylibr
 |-  ( ( ph /\ j e. D ) -> ( { E } i^i { j } ) = (/) )
163 disjdif2
 |-  ( ( { E } i^i { j } ) = (/) -> ( { E } \ { j } ) = { E } )
164 162 163 syl
 |-  ( ( ph /\ j e. D ) -> ( { E } \ { j } ) = { E } )
165 164 uneq2d
 |-  ( ( ph /\ j e. D ) -> ( ( D \ { j } ) u. ( { E } \ { j } ) ) = ( ( D \ { j } ) u. { E } ) )
166 143 165 eqtrd
 |-  ( ( ph /\ j e. D ) -> ( ( D u. { E } ) \ { j } ) = ( ( D \ { j } ) u. { E } ) )
167 166 prodeq1d
 |-  ( ( ph /\ j e. D ) -> prod_ i e. ( ( D u. { E } ) \ { j } ) A = prod_ i e. ( ( D \ { j } ) u. { E } ) A )
168 167 adantlr
 |-  ( ( ( ph /\ x e. X ) /\ j e. D ) -> prod_ i e. ( ( D u. { E } ) \ { j } ) A = prod_ i e. ( ( D \ { j } ) u. { E } ) A )
169 nfv
 |-  F/ i j e. D
170 21 169 nfan
 |-  F/ i ( ( ph /\ x e. X ) /\ j e. D )
171 102 adantr
 |-  ( ( ( ph /\ x e. X ) /\ j e. D ) -> ( D \ { j } ) e. Fin )
172 58 adantr
 |-  ( ( ( ph /\ x e. X ) /\ j e. D ) -> ph )
173 172 8 syl
 |-  ( ( ( ph /\ x e. X ) /\ j e. D ) -> E e. _V )
174 id
 |-  ( -. E e. D -> -. E e. D )
175 174 intnanrd
 |-  ( -. E e. D -> -. ( E e. D /\ -. E e. { j } ) )
176 174 175 syl
 |-  ( -. E e. D -> -. ( E e. D /\ -. E e. { j } ) )
177 eldif
 |-  ( E e. ( D \ { j } ) <-> ( E e. D /\ -. E e. { j } ) )
178 176 177 sylnibr
 |-  ( -. E e. D -> -. E e. ( D \ { j } ) )
179 9 178 syl
 |-  ( ph -> -. E e. ( D \ { j } ) )
180 172 179 syl
 |-  ( ( ( ph /\ x e. X ) /\ j e. D ) -> -. E e. ( D \ { j } ) )
181 105 adantlr
 |-  ( ( ( ( ph /\ x e. X ) /\ j e. D ) /\ i e. ( D \ { j } ) ) -> A e. CC )
182 87 adantr
 |-  ( ( ( ph /\ x e. X ) /\ j e. D ) -> F e. CC )
183 170 4 171 173 180 181 16 182 fprodsplitsn
 |-  ( ( ( ph /\ x e. X ) /\ j e. D ) -> prod_ i e. ( ( D \ { j } ) u. { E } ) A = ( prod_ i e. ( D \ { j } ) A x. F ) )
184 eqidd
 |-  ( ( ( ph /\ x e. X ) /\ j e. D ) -> ( prod_ i e. ( D \ { j } ) A x. F ) = ( prod_ i e. ( D \ { j } ) A x. F ) )
185 168 183 184 3eqtrd
 |-  ( ( ( ph /\ x e. X ) /\ j e. D ) -> prod_ i e. ( ( D u. { E } ) \ { j } ) A = ( prod_ i e. ( D \ { j } ) A x. F ) )
186 185 oveq2d
 |-  ( ( ( ph /\ x e. X ) /\ j e. D ) -> ( C x. prod_ i e. ( ( D u. { E } ) \ { j } ) A ) = ( C x. ( prod_ i e. ( D \ { j } ) A x. F ) ) )
187 12 107 182 mulassd
 |-  ( ( ( ph /\ x e. X ) /\ j e. D ) -> ( ( C x. prod_ i e. ( D \ { j } ) A ) x. F ) = ( C x. ( prod_ i e. ( D \ { j } ) A x. F ) ) )
188 187 eqcomd
 |-  ( ( ( ph /\ x e. X ) /\ j e. D ) -> ( C x. ( prod_ i e. ( D \ { j } ) A x. F ) ) = ( ( C x. prod_ i e. ( D \ { j } ) A ) x. F ) )
189 186 188 eqtrd
 |-  ( ( ( ph /\ x e. X ) /\ j e. D ) -> ( C x. prod_ i e. ( ( D u. { E } ) \ { j } ) A ) = ( ( C x. prod_ i e. ( D \ { j } ) A ) x. F ) )
190 189 ex
 |-  ( ( ph /\ x e. X ) -> ( j e. D -> ( C x. prod_ i e. ( ( D u. { E } ) \ { j } ) A ) = ( ( C x. prod_ i e. ( D \ { j } ) A ) x. F ) ) )
191 99 190 ralrimi
 |-  ( ( ph /\ x e. X ) -> A. j e. D ( C x. prod_ i e. ( ( D u. { E } ) \ { j } ) A ) = ( ( C x. prod_ i e. ( D \ { j } ) A ) x. F ) )
192 191 sumeq2d
 |-  ( ( ph /\ x e. X ) -> sum_ j e. D ( C x. prod_ i e. ( ( D u. { E } ) \ { j } ) A ) = sum_ j e. D ( ( C x. prod_ i e. ( D \ { j } ) A ) x. F ) )
193 99 88 87 108 fsummulc1f
 |-  ( ( ph /\ x e. X ) -> ( sum_ j e. D ( C x. prod_ i e. ( D \ { j } ) A ) x. F ) = sum_ j e. D ( ( C x. prod_ i e. ( D \ { j } ) A ) x. F ) )
194 193 eqcomd
 |-  ( ( ph /\ x e. X ) -> sum_ j e. D ( ( C x. prod_ i e. ( D \ { j } ) A ) x. F ) = ( sum_ j e. D ( C x. prod_ i e. ( D \ { j } ) A ) x. F ) )
195 eqidd
 |-  ( ( ph /\ x e. X ) -> ( sum_ j e. D ( C x. prod_ i e. ( D \ { j } ) A ) x. F ) = ( sum_ j e. D ( C x. prod_ i e. ( D \ { j } ) A ) x. F ) )
196 192 194 195 3eqtrd
 |-  ( ( ph /\ x e. X ) -> sum_ j e. D ( C x. prod_ i e. ( ( D u. { E } ) \ { j } ) A ) = ( sum_ j e. D ( C x. prod_ i e. ( D \ { j } ) A ) x. F ) )
197 109 87 mulcld
 |-  ( ( ph /\ x e. X ) -> ( sum_ j e. D ( C x. prod_ i e. ( D \ { j } ) A ) x. F ) e. CC )
198 196 197 eqeltrd
 |-  ( ( ph /\ x e. X ) -> sum_ j e. D ( C x. prod_ i e. ( ( D u. { E } ) \ { j } ) A ) e. CC )
199 198 140 addcomd
 |-  ( ( ph /\ x e. X ) -> ( sum_ j e. D ( C x. prod_ i e. ( ( D u. { E } ) \ { j } ) A ) + ( G x. prod_ i e. ( ( D u. { E } ) \ { E } ) A ) ) = ( ( G x. prod_ i e. ( ( D u. { E } ) \ { E } ) A ) + sum_ j e. D ( C x. prod_ i e. ( ( D u. { E } ) \ { j } ) A ) ) )
200 50 oveq2d
 |-  ( ph -> ( G x. prod_ i e. ( ( D u. { E } ) \ { E } ) A ) = ( G x. prod_ i e. D A ) )
201 200 adantr
 |-  ( ( ph /\ x e. X ) -> ( G x. prod_ i e. ( ( D u. { E } ) \ { E } ) A ) = ( G x. prod_ i e. D A ) )
202 201 196 oveq12d
 |-  ( ( ph /\ x e. X ) -> ( ( G x. prod_ i e. ( ( D u. { E } ) \ { E } ) A ) + sum_ j e. D ( C x. prod_ i e. ( ( D u. { E } ) \ { j } ) A ) ) = ( ( G x. prod_ i e. D A ) + ( sum_ j e. D ( C x. prod_ i e. ( D \ { j } ) A ) x. F ) ) )
203 141 199 202 3eqtrrd
 |-  ( ( ph /\ x e. X ) -> ( ( G x. prod_ i e. D A ) + ( sum_ j e. D ( C x. prod_ i e. ( D \ { j } ) A ) x. F ) ) = sum_ j e. ( D u. { E } ) ( C x. prod_ i e. ( ( D u. { E } ) \ { j } ) A ) )
204 1 203 mpteq2da
 |-  ( ph -> ( x e. X |-> ( ( G x. prod_ i e. D A ) + ( sum_ j e. D ( C x. prod_ i e. ( D \ { j } ) A ) x. F ) ) ) = ( x e. X |-> sum_ j e. ( D u. { E } ) ( C x. prod_ i e. ( ( D u. { E } ) \ { j } ) A ) ) )
205 55 110 204 3eqtrd
 |-  ( ph -> ( S _D ( x e. X |-> prod_ i e. ( D u. { E } ) A ) ) = ( x e. X |-> sum_ j e. ( D u. { E } ) ( C x. prod_ i e. ( ( D u. { E } ) \ { j } ) A ) ) )