Metamath Proof Explorer


Theorem fmuldfeq

Description: X and Z are two equivalent definitions of the finite product of real functions. Y is a set of real functions from a common domain T, Y is closed under function multiplication and U is a finite sequence of functions in Y. M is the number of functions multiplied together. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses fmuldfeq.1 i φ
fmuldfeq.2 _ t Y
fmuldfeq.3 P = f Y , g Y t T f t g t
fmuldfeq.4 X = seq 1 P U M
fmuldfeq.5 F = t T i 1 M U i t
fmuldfeq.6 Z = t T seq 1 × F t M
fmuldfeq.7 φ T V
fmuldfeq.8 φ M
fmuldfeq.9 φ U : 1 M Y
fmuldfeq.10 φ f Y f : T
fmuldfeq.11 φ f Y g Y t T f t g t Y
Assertion fmuldfeq φ t T X t = Z t

Proof

Step Hyp Ref Expression
1 fmuldfeq.1 i φ
2 fmuldfeq.2 _ t Y
3 fmuldfeq.3 P = f Y , g Y t T f t g t
4 fmuldfeq.4 X = seq 1 P U M
5 fmuldfeq.5 F = t T i 1 M U i t
6 fmuldfeq.6 Z = t T seq 1 × F t M
7 fmuldfeq.7 φ T V
8 fmuldfeq.8 φ M
9 fmuldfeq.9 φ U : 1 M Y
10 fmuldfeq.10 φ f Y f : T
11 fmuldfeq.11 φ f Y g Y t T f t g t Y
12 8 nnge1d φ 1 M
13 12 adantr φ t T 1 M
14 nnre M M
15 leid M M M
16 8 14 15 3syl φ M M
17 16 adantr φ t T M M
18 8 nnzd φ M
19 18 adantr φ t T M
20 1zzd φ t T 1
21 elfz M 1 M M 1 M 1 M M M
22 19 20 19 21 syl3anc φ t T M 1 M 1 M M M
23 13 17 22 mpbir2and φ t T M 1 M
24 8 3ad2ant1 φ t T M 1 M M
25 eleq1 m = 1 m 1 M 1 1 M
26 25 3anbi3d m = 1 φ t T m 1 M φ t T 1 1 M
27 fveq2 m = 1 seq 1 P U m = seq 1 P U 1
28 27 fveq1d m = 1 seq 1 P U m t = seq 1 P U 1 t
29 fveq2 m = 1 seq 1 × F t m = seq 1 × F t 1
30 28 29 eqeq12d m = 1 seq 1 P U m t = seq 1 × F t m seq 1 P U 1 t = seq 1 × F t 1
31 26 30 imbi12d m = 1 φ t T m 1 M seq 1 P U m t = seq 1 × F t m φ t T 1 1 M seq 1 P U 1 t = seq 1 × F t 1
32 eleq1 m = n m 1 M n 1 M
33 32 3anbi3d m = n φ t T m 1 M φ t T n 1 M
34 fveq2 m = n seq 1 P U m = seq 1 P U n
35 34 fveq1d m = n seq 1 P U m t = seq 1 P U n t
36 fveq2 m = n seq 1 × F t m = seq 1 × F t n
37 35 36 eqeq12d m = n seq 1 P U m t = seq 1 × F t m seq 1 P U n t = seq 1 × F t n
38 33 37 imbi12d m = n φ t T m 1 M seq 1 P U m t = seq 1 × F t m φ t T n 1 M seq 1 P U n t = seq 1 × F t n
39 eleq1 m = n + 1 m 1 M n + 1 1 M
40 39 3anbi3d m = n + 1 φ t T m 1 M φ t T n + 1 1 M
41 fveq2 m = n + 1 seq 1 P U m = seq 1 P U n + 1
42 41 fveq1d m = n + 1 seq 1 P U m t = seq 1 P U n + 1 t
43 fveq2 m = n + 1 seq 1 × F t m = seq 1 × F t n + 1
44 42 43 eqeq12d m = n + 1 seq 1 P U m t = seq 1 × F t m seq 1 P U n + 1 t = seq 1 × F t n + 1
45 40 44 imbi12d m = n + 1 φ t T m 1 M seq 1 P U m t = seq 1 × F t m φ t T n + 1 1 M seq 1 P U n + 1 t = seq 1 × F t n + 1
46 eleq1 m = M m 1 M M 1 M
47 46 3anbi3d m = M φ t T m 1 M φ t T M 1 M
48 fveq2 m = M seq 1 P U m = seq 1 P U M
49 48 fveq1d m = M seq 1 P U m t = seq 1 P U M t
50 fveq2 m = M seq 1 × F t m = seq 1 × F t M
51 49 50 eqeq12d m = M seq 1 P U m t = seq 1 × F t m seq 1 P U M t = seq 1 × F t M
52 47 51 imbi12d m = M φ t T m 1 M seq 1 P U m t = seq 1 × F t m φ t T M 1 M seq 1 P U M t = seq 1 × F t M
53 1z 1
54 seq1 1 seq 1 × F t 1 = F t 1
55 53 54 ax-mp seq 1 × F t 1 = F t 1
56 1le1 1 1
57 56 a1i φ 1 1
58 1zzd φ 1
59 elfz 1 1 M 1 1 M 1 1 1 M
60 58 58 18 59 syl3anc φ 1 1 M 1 1 1 M
61 57 12 60 mpbir2and φ 1 1 M
62 nfv i t T
63 nfcv _ i T
64 nfmpt1 _ i i 1 M U i t
65 63 64 nfmpt _ i t T i 1 M U i t
66 5 65 nfcxfr _ i F
67 nfcv _ i t
68 66 67 nffv _ i F t
69 nfcv _ i 1
70 68 69 nffv _ i F t 1
71 nffvmpt1 _ i i 1 M U i t 1
72 70 71 nfeq i F t 1 = i 1 M U i t 1
73 62 72 nfim i t T F t 1 = i 1 M U i t 1
74 fveq2 i = 1 F t i = F t 1
75 fveq2 i = 1 i 1 M U i t i = i 1 M U i t 1
76 74 75 eqeq12d i = 1 F t i = i 1 M U i t i F t 1 = i 1 M U i t 1
77 76 imbi2d i = 1 t T F t i = i 1 M U i t i t T F t 1 = i 1 M U i t 1
78 ovex 1 M V
79 78 mptex i 1 M U i t V
80 5 fvmpt2 t T i 1 M U i t V F t = i 1 M U i t
81 79 80 mpan2 t T F t = i 1 M U i t
82 81 fveq1d t T F t i = i 1 M U i t i
83 73 77 82 vtoclg1f 1 1 M t T F t 1 = i 1 M U i t 1
84 61 83 syl φ t T F t 1 = i 1 M U i t 1
85 84 imp φ t T F t 1 = i 1 M U i t 1
86 eqid i 1 M U i t = i 1 M U i t
87 fveq2 i = 1 U i = U 1
88 87 fveq1d i = 1 U i t = U 1 t
89 61 adantr φ t T 1 1 M
90 9 61 ffvelrnd φ U 1 Y
91 90 ancli φ φ U 1 Y
92 eleq1 f = U 1 f Y U 1 Y
93 92 anbi2d f = U 1 φ f Y φ U 1 Y
94 feq1 f = U 1 f : T U 1 : T
95 93 94 imbi12d f = U 1 φ f Y f : T φ U 1 Y U 1 : T
96 10 a1i f Y φ f Y f : T
97 95 96 vtoclga U 1 Y φ U 1 Y U 1 : T
98 90 91 97 sylc φ U 1 : T
99 98 ffvelrnda φ t T U 1 t
100 86 88 89 99 fvmptd3 φ t T i 1 M U i t 1 = U 1 t
101 85 100 eqtrd φ t T F t 1 = U 1 t
102 seq1 1 seq 1 P U 1 = U 1
103 53 102 ax-mp seq 1 P U 1 = U 1
104 103 fveq1i seq 1 P U 1 t = U 1 t
105 101 104 syl6eqr φ t T F t 1 = seq 1 P U 1 t
106 55 105 syl5req φ t T seq 1 P U 1 t = seq 1 × F t 1
107 106 3adant3 φ t T 1 1 M seq 1 P U 1 t = seq 1 × F t 1
108 simp31 n φ t T n 1 M seq 1 P U n t = seq 1 × F t n φ t T n + 1 1 M φ
109 simp1 n φ t T n 1 M seq 1 P U n t = seq 1 × F t n φ t T n + 1 1 M n
110 simp33 n φ t T n 1 M seq 1 P U n t = seq 1 × F t n φ t T n + 1 1 M n + 1 1 M
111 109 110 jca n φ t T n 1 M seq 1 P U n t = seq 1 × F t n φ t T n + 1 1 M n n + 1 1 M
112 elnnuz n n 1
113 112 biimpi n n 1
114 113 anim1i n n + 1 1 M n 1 n + 1 1 M
115 peano2fzr n 1 n + 1 1 M n 1 M
116 111 114 115 3syl n φ t T n 1 M seq 1 P U n t = seq 1 × F t n φ t T n + 1 1 M n 1 M
117 simp32 n φ t T n 1 M seq 1 P U n t = seq 1 × F t n φ t T n + 1 1 M t T
118 simp2 n φ t T n 1 M seq 1 P U n t = seq 1 × F t n φ t T n + 1 1 M φ t T n 1 M seq 1 P U n t = seq 1 × F t n
119 108 117 116 118 mp3and n φ t T n 1 M seq 1 P U n t = seq 1 × F t n φ t T n + 1 1 M seq 1 P U n t = seq 1 × F t n
120 116 110 119 3jca n φ t T n 1 M seq 1 P U n t = seq 1 × F t n φ t T n + 1 1 M n 1 M n + 1 1 M seq 1 P U n t = seq 1 × F t n
121 nfv f φ
122 nfv f n 1 M
123 nfv f n + 1 1 M
124 nfcv _ f 1
125 nfmpo1 _ f f Y , g Y t T f t g t
126 3 125 nfcxfr _ f P
127 nfcv _ f U
128 124 126 127 nfseq _ f seq 1 P U
129 nfcv _ f n
130 128 129 nffv _ f seq 1 P U n
131 nfcv _ f t
132 130 131 nffv _ f seq 1 P U n t
133 nfcv _ f seq 1 × F t n
134 132 133 nfeq f seq 1 P U n t = seq 1 × F t n
135 122 123 134 nf3an f n 1 M n + 1 1 M seq 1 P U n t = seq 1 × F t n
136 121 135 nfan f φ n 1 M n + 1 1 M seq 1 P U n t = seq 1 × F t n
137 nfv g φ
138 nfv g n 1 M
139 nfv g n + 1 1 M
140 nfcv _ g 1
141 nfmpo2 _ g f Y , g Y t T f t g t
142 3 141 nfcxfr _ g P
143 nfcv _ g U
144 140 142 143 nfseq _ g seq 1 P U
145 nfcv _ g n
146 144 145 nffv _ g seq 1 P U n
147 nfcv _ g t
148 146 147 nffv _ g seq 1 P U n t
149 nfcv _ g seq 1 × F t n
150 148 149 nfeq g seq 1 P U n t = seq 1 × F t n
151 138 139 150 nf3an g n 1 M n + 1 1 M seq 1 P U n t = seq 1 × F t n
152 137 151 nfan g φ n 1 M n + 1 1 M seq 1 P U n t = seq 1 × F t n
153 7 adantr φ n 1 M n + 1 1 M seq 1 P U n t = seq 1 × F t n T V
154 9 adantr φ n 1 M n + 1 1 M seq 1 P U n t = seq 1 × F t n U : 1 M Y
155 11 3adant1r φ n 1 M n + 1 1 M seq 1 P U n t = seq 1 × F t n f Y g Y t T f t g t Y
156 simpr1 φ n 1 M n + 1 1 M seq 1 P U n t = seq 1 × F t n n 1 M
157 simpr2 φ n 1 M n + 1 1 M seq 1 P U n t = seq 1 × F t n n + 1 1 M
158 simpr3 φ n 1 M n + 1 1 M seq 1 P U n t = seq 1 × F t n seq 1 P U n t = seq 1 × F t n
159 10 adantlr φ n 1 M n + 1 1 M seq 1 P U n t = seq 1 × F t n f Y f : T
160 136 152 2 3 5 153 154 155 156 157 158 159 fmuldfeqlem1 φ n 1 M n + 1 1 M seq 1 P U n t = seq 1 × F t n t T seq 1 P U n + 1 t = seq 1 × F t n + 1
161 108 120 117 160 syl21anc n φ t T n 1 M seq 1 P U n t = seq 1 × F t n φ t T n + 1 1 M seq 1 P U n + 1 t = seq 1 × F t n + 1
162 161 3exp n φ t T n 1 M seq 1 P U n t = seq 1 × F t n φ t T n + 1 1 M seq 1 P U n + 1 t = seq 1 × F t n + 1
163 31 38 45 52 107 162 nnind M φ t T M 1 M seq 1 P U M t = seq 1 × F t M
164 24 163 mpcom φ t T M 1 M seq 1 P U M t = seq 1 × F t M
165 23 164 mpd3an3 φ t T seq 1 P U M t = seq 1 × F t M
166 4 fveq1i X t = seq 1 P U M t
167 166 a1i φ t T X t = seq 1 P U M t
168 simpr φ t T t T
169 elnnuz M M 1
170 8 169 sylib φ M 1
171 170 adantr φ t T M 1
172 1 62 nfan i φ t T
173 nfv i k 1 M
174 172 173 nfan i φ t T k 1 M
175 nfcv _ i k
176 68 175 nffv _ i F t k
177 176 nfel1 i F t k
178 174 177 nfim i φ t T k 1 M F t k
179 eleq1 i = k i 1 M k 1 M
180 179 anbi2d i = k φ t T i 1 M φ t T k 1 M
181 fveq2 i = k F t i = F t k
182 181 eleq1d i = k F t i F t k
183 180 182 imbi12d i = k φ t T i 1 M F t i φ t T k 1 M F t k
184 82 ad2antlr φ t T i 1 M F t i = i 1 M U i t i
185 simpr φ t T i 1 M i 1 M
186 9 ffvelrnda φ i 1 M U i Y
187 simpl φ i 1 M φ
188 187 186 jca φ i 1 M φ U i Y
189 eleq1 f = U i f Y U i Y
190 189 anbi2d f = U i φ f Y φ U i Y
191 feq1 f = U i f : T U i : T
192 190 191 imbi12d f = U i φ f Y f : T φ U i Y U i : T
193 192 96 vtoclga U i Y φ U i Y U i : T
194 186 188 193 sylc φ i 1 M U i : T
195 194 adantlr φ t T i 1 M U i : T
196 simplr φ t T i 1 M t T
197 195 196 ffvelrnd φ t T i 1 M U i t
198 86 fvmpt2 i 1 M U i t i 1 M U i t i = U i t
199 185 197 198 syl2anc φ t T i 1 M i 1 M U i t i = U i t
200 199 197 eqeltrd φ t T i 1 M i 1 M U i t i
201 184 200 eqeltrd φ t T i 1 M F t i
202 178 183 201 chvarfv φ t T k 1 M F t k
203 remulcl k b k b
204 203 adantl φ t T k b k b
205 171 202 204 seqcl φ t T seq 1 × F t M
206 6 fvmpt2 t T seq 1 × F t M Z t = seq 1 × F t M
207 168 205 206 syl2anc φ t T Z t = seq 1 × F t M
208 165 167 207 3eqtr4d φ t T X t = Z t