Metamath Proof Explorer


Theorem dvmptfprod

Description: Function-builder for derivative, finite product rule. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses dvmptfprod.iph i φ
dvmptfprod.jph j φ
dvmptfprod.j J = K 𝑡 S
dvmptfprod.k K = TopOpen fld
dvmptfprod.s φ S
dvmptfprod.x φ X J
dvmptfprod.i φ I Fin
dvmptfprod.a φ i I x X A
dvmptfprod.b φ i I x X B
dvmptfprod.d φ i I dx X A dS x = x X B
dvmptfprod.bc i = j B = C
Assertion dvmptfprod φ dx X i I A dS x = x X j I C i I j A

Proof

Step Hyp Ref Expression
1 dvmptfprod.iph i φ
2 dvmptfprod.jph j φ
3 dvmptfprod.j J = K 𝑡 S
4 dvmptfprod.k K = TopOpen fld
5 dvmptfprod.s φ S
6 dvmptfprod.x φ X J
7 dvmptfprod.i φ I Fin
8 dvmptfprod.a φ i I x X A
9 dvmptfprod.b φ i I x X B
10 dvmptfprod.d φ i I dx X A dS x = x X B
11 dvmptfprod.bc i = j B = C
12 ssid I I
13 12 jctr φ φ I I
14 sseq1 a = a I I
15 14 anbi2d a = φ a I φ I
16 prodeq1 a = i a A = i A
17 16 mpteq2dv a = x X i a A = x X i A
18 17 oveq2d a = dx X i a A dS x = dx X i A dS x
19 sumeq1 a = j a C i a j A = j C i a j A
20 difeq1 a = a j = j
21 20 prodeq1d a = i a j A = i j A
22 21 oveq2d a = C i a j A = C i j A
23 22 sumeq2sdv a = j C i a j A = j C i j A
24 19 23 eqtrd a = j a C i a j A = j C i j A
25 24 mpteq2dv a = x X j a C i a j A = x X j C i j A
26 18 25 eqeq12d a = dx X i a A dS x = x X j a C i a j A dx X i A dS x = x X j C i j A
27 15 26 imbi12d a = φ a I dx X i a A dS x = x X j a C i a j A φ I dx X i A dS x = x X j C i j A
28 sseq1 a = b a I b I
29 28 anbi2d a = b φ a I φ b I
30 prodeq1 a = b i a A = i b A
31 30 mpteq2dv a = b x X i a A = x X i b A
32 31 oveq2d a = b dx X i a A dS x = dx X i b A dS x
33 sumeq1 a = b j a C i a j A = j b C i a j A
34 difeq1 a = b a j = b j
35 34 prodeq1d a = b i a j A = i b j A
36 35 oveq2d a = b C i a j A = C i b j A
37 36 sumeq2sdv a = b j b C i a j A = j b C i b j A
38 33 37 eqtrd a = b j a C i a j A = j b C i b j A
39 38 mpteq2dv a = b x X j a C i a j A = x X j b C i b j A
40 32 39 eqeq12d a = b dx X i a A dS x = x X j a C i a j A dx X i b A dS x = x X j b C i b j A
41 29 40 imbi12d a = b φ a I dx X i a A dS x = x X j a C i a j A φ b I dx X i b A dS x = x X j b C i b j A
42 sseq1 a = b c a I b c I
43 42 anbi2d a = b c φ a I φ b c I
44 prodeq1 a = b c i a A = i b c A
45 44 mpteq2dv a = b c x X i a A = x X i b c A
46 45 oveq2d a = b c dx X i a A dS x = dx X i b c A dS x
47 sumeq1 a = b c j a C i a j A = j b c C i a j A
48 difeq1 a = b c a j = b c j
49 48 prodeq1d a = b c i a j A = i b c j A
50 49 oveq2d a = b c C i a j A = C i b c j A
51 50 sumeq2sdv a = b c j b c C i a j A = j b c C i b c j A
52 47 51 eqtrd a = b c j a C i a j A = j b c C i b c j A
53 52 mpteq2dv a = b c x X j a C i a j A = x X j b c C i b c j A
54 46 53 eqeq12d a = b c dx X i a A dS x = x X j a C i a j A dx X i b c A dS x = x X j b c C i b c j A
55 43 54 imbi12d a = b c φ a I dx X i a A dS x = x X j a C i a j A φ b c I dx X i b c A dS x = x X j b c C i b c j A
56 sseq1 a = I a I I I
57 56 anbi2d a = I φ a I φ I I
58 prodeq1 a = I i a A = i I A
59 58 mpteq2dv a = I x X i a A = x X i I A
60 59 oveq2d a = I dx X i a A dS x = dx X i I A dS x
61 sumeq1 a = I j a C i a j A = j I C i a j A
62 difeq1 a = I a j = I j
63 62 prodeq1d a = I i a j A = i I j A
64 63 oveq2d a = I C i a j A = C i I j A
65 64 sumeq2sdv a = I j I C i a j A = j I C i I j A
66 61 65 eqtrd a = I j a C i a j A = j I C i I j A
67 66 mpteq2dv a = I x X j a C i a j A = x X j I C i I j A
68 60 67 eqeq12d a = I dx X i a A dS x = x X j a C i a j A dx X i I A dS x = x X j I C i I j A
69 57 68 imbi12d a = I φ a I dx X i a A dS x = x X j a C i a j A φ I I dx X i I A dS x = x X j I C i I j A
70 prod0 i A = 1
71 70 mpteq2i x X i A = x X 1
72 71 oveq2i dx X i A dS x = dx X 1 dS x
73 72 a1i φ dx X i A dS x = dx X 1 dS x
74 4 oveq1i K 𝑡 S = TopOpen fld 𝑡 S
75 3 74 eqtri J = TopOpen fld 𝑡 S
76 6 75 eleqtrdi φ X TopOpen fld 𝑡 S
77 1cnd φ 1
78 5 76 77 dvmptconst φ dx X 1 dS x = x X 0
79 sum0 j C i j A = 0
80 79 eqcomi 0 = j C i j A
81 80 mpteq2i x X 0 = x X j C i j A
82 81 a1i φ x X 0 = x X j C i j A
83 73 78 82 3eqtrd φ dx X i A dS x = x X j C i j A
84 83 adantr φ I dx X i A dS x = x X j C i j A
85 simp3 b Fin ¬ c b φ b I dx X i b A dS x = x X j b C i b j A φ b c I φ b c I
86 simp1r b Fin ¬ c b φ b I dx X i b A dS x = x X j b C i b j A φ b c I ¬ c b
87 ssun1 b b c
88 sstr2 b b c b c I b I
89 87 88 ax-mp b c I b I
90 89 anim2i φ b c I φ b I
91 90 adantl φ b I dx X i b A dS x = x X j b C i b j A φ b c I φ b I
92 simpl φ b I dx X i b A dS x = x X j b C i b j A φ b c I φ b I dx X i b A dS x = x X j b C i b j A
93 91 92 mpd φ b I dx X i b A dS x = x X j b C i b j A φ b c I dx X i b A dS x = x X j b C i b j A
94 93 3adant1 b Fin ¬ c b φ b I dx X i b A dS x = x X j b C i b j A φ b c I dx X i b A dS x = x X j b C i b j A
95 nfv x φ b c I ¬ c b
96 nfcv _ x S
97 nfcv _ x D
98 nfmpt1 _ x x X i b A
99 96 97 98 nfov _ x dx X i b A dS x
100 nfmpt1 _ x x X j b C i b j A
101 99 100 nfeq x dx X i b A dS x = x X j b C i b j A
102 95 101 nfan x φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A
103 nfv i b c I
104 1 103 nfan i φ b c I
105 nfv i ¬ c b
106 104 105 nfan i φ b c I ¬ c b
107 nfcv _ i S
108 nfcv _ i D
109 nfcv _ i X
110 nfcv _ i b
111 110 nfcprod1 _ i i b A
112 109 111 nfmpt _ i x X i b A
113 107 108 112 nfov _ i dx X i b A dS x
114 nfcv _ i C
115 nfcv _ i ×
116 nfcv _ i b j
117 116 nfcprod1 _ i i b j A
118 114 115 117 nfov _ i C i b j A
119 110 118 nfsum _ i j b C i b j A
120 109 119 nfmpt _ i x X j b C i b j A
121 113 120 nfeq i dx X i b A dS x = x X j b C i b j A
122 106 121 nfan i φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A
123 nfv j b c I
124 2 123 nfan j φ b c I
125 nfv j ¬ c b
126 124 125 nfan j φ b c I ¬ c b
127 nfcv _ j dx X i b A dS x
128 nfcv _ j X
129 nfcv _ j b
130 129 nfsum1 _ j j b C i b j A
131 128 130 nfmpt _ j x X j b C i b j A
132 127 131 nfeq j dx X i b A dS x = x X j b C i b j A
133 126 132 nfan j φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A
134 nfcsb1v _ i c / i A
135 nfcsb1v _ j c / j C
136 simpl φ b c I φ
137 136 ad2antrr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A φ
138 137 8 syl3an1 φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A i I x X A
139 7 ad3antrrr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A I Fin
140 89 adantl φ b c I b I
141 140 ad2antrr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A b I
142 139 141 ssfid φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A b Fin
143 vex c V
144 143 a1i φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A c V
145 simplr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A ¬ c b
146 simpllr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A b c I
147 5 ad3antrrr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A S
148 137 ad2antrr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A x X j b φ
149 141 ad2antrr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A x X j b b I
150 simpr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A x X j b j b
151 149 150 sseldd φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A x X j b j I
152 simplr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A x X j b x X
153 nfv i j I
154 nfv i x X
155 1 153 154 nf3an i φ j I x X
156 nfv i C
157 155 156 nfim i φ j I x X C
158 eleq1w i = j i I j I
159 158 3anbi2d i = j φ i I x X φ j I x X
160 11 eleq1d i = j B C
161 159 160 imbi12d i = j φ i I x X B φ j I x X C
162 157 161 9 chvarfv φ j I x X C
163 148 151 152 162 syl3anc φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A x X j b C
164 simpr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A dx X i b A dS x = x X j b C i b j A
165 136 adantr φ b c I x X φ
166 id b c I b c I
167 vsnid c c
168 elun2 c c c b c
169 167 168 mp1i b c I c b c
170 166 169 sseldd b c I c I
171 170 ad2antlr φ b c I x X c I
172 simpr φ b c I x X x X
173 nfv j c I
174 nfv j x X
175 2 173 174 nf3an j φ c I x X
176 135 nfel1 j c / j C
177 175 176 nfim j φ c I x X c / j C
178 eleq1w j = c j I c I
179 178 3anbi2d j = c φ j I x X φ c I x X
180 csbeq1a j = c C = c / j C
181 180 eleq1d j = c C c / j C
182 179 181 imbi12d j = c φ j I x X C φ c I x X c / j C
183 177 182 162 chvarfv φ c I x X c / j C
184 165 171 172 183 syl3anc φ b c I x X c / j C
185 184 ad4ant14 φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A x X c / j C
186 2 173 nfan j φ c I
187 nfcv _ j dx X c / i A dS x
188 128 135 nfmpt _ j x X c / j C
189 187 188 nfeq j dx X c / i A dS x = x X c / j C
190 186 189 nfim j φ c I dx X c / i A dS x = x X c / j C
191 178 anbi2d j = c φ j I φ c I
192 csbeq1 j = c j / i A = c / i A
193 192 mpteq2dv j = c x X j / i A = x X c / i A
194 193 oveq2d j = c dx X j / i A dS x = dx X c / i A dS x
195 180 mpteq2dv j = c x X C = x X c / j C
196 194 195 eqeq12d j = c dx X j / i A dS x = x X C dx X c / i A dS x = x X c / j C
197 191 196 imbi12d j = c φ j I dx X j / i A dS x = x X C φ c I dx X c / i A dS x = x X c / j C
198 1 153 nfan i φ j I
199 nfcsb1v _ i j / i A
200 109 199 nfmpt _ i x X j / i A
201 107 108 200 nfov _ i dx X j / i A dS x
202 nfcv _ i x X C
203 201 202 nfeq i dx X j / i A dS x = x X C
204 198 203 nfim i φ j I dx X j / i A dS x = x X C
205 158 anbi2d i = j φ i I φ j I
206 csbeq1a i = j A = j / i A
207 206 mpteq2dv i = j x X A = x X j / i A
208 207 oveq2d i = j dx X A dS x = dx X j / i A dS x
209 11 mpteq2dv i = j x X B = x X C
210 208 209 eqeq12d i = j dx X A dS x = x X B dx X j / i A dS x = x X C
211 205 210 imbi12d i = j φ i I dx X A dS x = x X B φ j I dx X j / i A dS x = x X C
212 204 211 10 chvarfv φ j I dx X j / i A dS x = x X C
213 190 197 212 chvarfv φ c I dx X c / i A dS x = x X c / j C
214 170 213 sylan2 φ b c I dx X c / i A dS x = x X c / j C
215 214 ad2antrr φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A dx X c / i A dS x = x X c / j C
216 csbeq1a i = c A = c / i A
217 102 122 133 134 135 138 142 144 145 146 147 163 164 185 215 216 180 dvmptfprodlem φ b c I ¬ c b dx X i b A dS x = x X j b C i b j A dx X i b c A dS x = x X j b c C i b c j A
218 85 86 94 217 syl21anc b Fin ¬ c b φ b I dx X i b A dS x = x X j b C i b j A φ b c I dx X i b c A dS x = x X j b c C i b c j A
219 218 3exp b Fin ¬ c b φ b I dx X i b A dS x = x X j b C i b j A φ b c I dx X i b c A dS x = x X j b c C i b c j A
220 27 41 55 69 84 219 findcard2s I Fin φ I I dx X i I A dS x = x X j I C i I j A
221 7 13 220 sylc φ dx X i I A dS x = x X j I C i I j A