This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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