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 _tY
fmuldfeq.3 P=fY,gYtTftgt
fmuldfeq.4 X=seq1PUM
fmuldfeq.5 F=tTi1MUit
fmuldfeq.6 Z=tTseq1×FtM
fmuldfeq.7 φTV
fmuldfeq.8 φM
fmuldfeq.9 φU:1MY
fmuldfeq.10 φfYf:T
fmuldfeq.11 φfYgYtTftgtY
Assertion fmuldfeq φtTXt=Zt

Proof

Step Hyp Ref Expression
1 fmuldfeq.1 iφ
2 fmuldfeq.2 _tY
3 fmuldfeq.3 P=fY,gYtTftgt
4 fmuldfeq.4 X=seq1PUM
5 fmuldfeq.5 F=tTi1MUit
6 fmuldfeq.6 Z=tTseq1×FtM
7 fmuldfeq.7 φTV
8 fmuldfeq.8 φM
9 fmuldfeq.9 φU:1MY
10 fmuldfeq.10 φfYf:T
11 fmuldfeq.11 φfYgYtTftgtY
12 1zzd φtT1
13 8 nnzd φM
14 13 adantr φtTM
15 8 nnge1d φ1M
16 15 adantr φtT1M
17 nnre MM
18 leid MMM
19 8 17 18 3syl φMM
20 19 adantr φtTMM
21 12 14 14 16 20 elfzd φtTM1M
22 8 3ad2ant1 φtTM1MM
23 eleq1 m=1m1M11M
24 23 3anbi3d m=1φtTm1MφtT11M
25 fveq2 m=1seq1PUm=seq1PU1
26 25 fveq1d m=1seq1PUmt=seq1PU1t
27 fveq2 m=1seq1×Ftm=seq1×Ft1
28 26 27 eqeq12d m=1seq1PUmt=seq1×Ftmseq1PU1t=seq1×Ft1
29 24 28 imbi12d m=1φtTm1Mseq1PUmt=seq1×FtmφtT11Mseq1PU1t=seq1×Ft1
30 eleq1 m=nm1Mn1M
31 30 3anbi3d m=nφtTm1MφtTn1M
32 fveq2 m=nseq1PUm=seq1PUn
33 32 fveq1d m=nseq1PUmt=seq1PUnt
34 fveq2 m=nseq1×Ftm=seq1×Ftn
35 33 34 eqeq12d m=nseq1PUmt=seq1×Ftmseq1PUnt=seq1×Ftn
36 31 35 imbi12d m=nφtTm1Mseq1PUmt=seq1×FtmφtTn1Mseq1PUnt=seq1×Ftn
37 eleq1 m=n+1m1Mn+11M
38 37 3anbi3d m=n+1φtTm1MφtTn+11M
39 fveq2 m=n+1seq1PUm=seq1PUn+1
40 39 fveq1d m=n+1seq1PUmt=seq1PUn+1t
41 fveq2 m=n+1seq1×Ftm=seq1×Ftn+1
42 40 41 eqeq12d m=n+1seq1PUmt=seq1×Ftmseq1PUn+1t=seq1×Ftn+1
43 38 42 imbi12d m=n+1φtTm1Mseq1PUmt=seq1×FtmφtTn+11Mseq1PUn+1t=seq1×Ftn+1
44 eleq1 m=Mm1MM1M
45 44 3anbi3d m=MφtTm1MφtTM1M
46 fveq2 m=Mseq1PUm=seq1PUM
47 46 fveq1d m=Mseq1PUmt=seq1PUMt
48 fveq2 m=Mseq1×Ftm=seq1×FtM
49 47 48 eqeq12d m=Mseq1PUmt=seq1×Ftmseq1PUMt=seq1×FtM
50 45 49 imbi12d m=MφtTm1Mseq1PUmt=seq1×FtmφtTM1Mseq1PUMt=seq1×FtM
51 1z 1
52 seq1 1seq1×Ft1=Ft1
53 51 52 ax-mp seq1×Ft1=Ft1
54 1zzd φ1
55 1le1 11
56 55 a1i φ11
57 54 13 54 56 15 elfzd φ11M
58 nfv itT
59 nfcv _iT
60 nfmpt1 _ii1MUit
61 59 60 nfmpt _itTi1MUit
62 5 61 nfcxfr _iF
63 nfcv _it
64 62 63 nffv _iFt
65 nfcv _i1
66 64 65 nffv _iFt1
67 nffvmpt1 _ii1MUit1
68 66 67 nfeq iFt1=i1MUit1
69 58 68 nfim itTFt1=i1MUit1
70 fveq2 i=1Fti=Ft1
71 fveq2 i=1i1MUiti=i1MUit1
72 70 71 eqeq12d i=1Fti=i1MUitiFt1=i1MUit1
73 72 imbi2d i=1tTFti=i1MUititTFt1=i1MUit1
74 ovex 1MV
75 74 mptex i1MUitV
76 5 fvmpt2 tTi1MUitVFt=i1MUit
77 75 76 mpan2 tTFt=i1MUit
78 77 fveq1d tTFti=i1MUiti
79 69 73 78 vtoclg1f 11MtTFt1=i1MUit1
80 57 79 syl φtTFt1=i1MUit1
81 80 imp φtTFt1=i1MUit1
82 eqid i1MUit=i1MUit
83 fveq2 i=1Ui=U1
84 83 fveq1d i=1Uit=U1t
85 57 adantr φtT11M
86 9 57 ffvelrnd φU1Y
87 86 ancli φφU1Y
88 eleq1 f=U1fYU1Y
89 88 anbi2d f=U1φfYφU1Y
90 feq1 f=U1f:TU1:T
91 89 90 imbi12d f=U1φfYf:TφU1YU1:T
92 10 a1i fYφfYf:T
93 91 92 vtoclga U1YφU1YU1:T
94 86 87 93 sylc φU1:T
95 94 ffvelrnda φtTU1t
96 82 84 85 95 fvmptd3 φtTi1MUit1=U1t
97 81 96 eqtrd φtTFt1=U1t
98 seq1 1seq1PU1=U1
99 51 98 ax-mp seq1PU1=U1
100 99 fveq1i seq1PU1t=U1t
101 97 100 eqtr4di φtTFt1=seq1PU1t
102 53 101 eqtr2id φtTseq1PU1t=seq1×Ft1
103 102 3adant3 φtT11Mseq1PU1t=seq1×Ft1
104 simp31 nφtTn1Mseq1PUnt=seq1×FtnφtTn+11Mφ
105 simp1 nφtTn1Mseq1PUnt=seq1×FtnφtTn+11Mn
106 simp33 nφtTn1Mseq1PUnt=seq1×FtnφtTn+11Mn+11M
107 105 106 jca nφtTn1Mseq1PUnt=seq1×FtnφtTn+11Mnn+11M
108 elnnuz nn1
109 108 biimpi nn1
110 109 anim1i nn+11Mn1n+11M
111 peano2fzr n1n+11Mn1M
112 107 110 111 3syl nφtTn1Mseq1PUnt=seq1×FtnφtTn+11Mn1M
113 simp32 nφtTn1Mseq1PUnt=seq1×FtnφtTn+11MtT
114 simp2 nφtTn1Mseq1PUnt=seq1×FtnφtTn+11MφtTn1Mseq1PUnt=seq1×Ftn
115 104 113 112 114 mp3and nφtTn1Mseq1PUnt=seq1×FtnφtTn+11Mseq1PUnt=seq1×Ftn
116 112 106 115 3jca nφtTn1Mseq1PUnt=seq1×FtnφtTn+11Mn1Mn+11Mseq1PUnt=seq1×Ftn
117 nfv fφ
118 nfv fn1M
119 nfv fn+11M
120 nfcv _f1
121 nfmpo1 _ffY,gYtTftgt
122 3 121 nfcxfr _fP
123 nfcv _fU
124 120 122 123 nfseq _fseq1PU
125 nfcv _fn
126 124 125 nffv _fseq1PUn
127 nfcv _ft
128 126 127 nffv _fseq1PUnt
129 nfcv _fseq1×Ftn
130 128 129 nfeq fseq1PUnt=seq1×Ftn
131 118 119 130 nf3an fn1Mn+11Mseq1PUnt=seq1×Ftn
132 117 131 nfan fφn1Mn+11Mseq1PUnt=seq1×Ftn
133 nfv gφ
134 nfv gn1M
135 nfv gn+11M
136 nfcv _g1
137 nfmpo2 _gfY,gYtTftgt
138 3 137 nfcxfr _gP
139 nfcv _gU
140 136 138 139 nfseq _gseq1PU
141 nfcv _gn
142 140 141 nffv _gseq1PUn
143 nfcv _gt
144 142 143 nffv _gseq1PUnt
145 nfcv _gseq1×Ftn
146 144 145 nfeq gseq1PUnt=seq1×Ftn
147 134 135 146 nf3an gn1Mn+11Mseq1PUnt=seq1×Ftn
148 133 147 nfan gφn1Mn+11Mseq1PUnt=seq1×Ftn
149 7 adantr φn1Mn+11Mseq1PUnt=seq1×FtnTV
150 9 adantr φn1Mn+11Mseq1PUnt=seq1×FtnU:1MY
151 11 3adant1r φn1Mn+11Mseq1PUnt=seq1×FtnfYgYtTftgtY
152 simpr1 φn1Mn+11Mseq1PUnt=seq1×Ftnn1M
153 simpr2 φn1Mn+11Mseq1PUnt=seq1×Ftnn+11M
154 simpr3 φn1Mn+11Mseq1PUnt=seq1×Ftnseq1PUnt=seq1×Ftn
155 10 adantlr φn1Mn+11Mseq1PUnt=seq1×FtnfYf:T
156 132 148 2 3 5 149 150 151 152 153 154 155 fmuldfeqlem1 φn1Mn+11Mseq1PUnt=seq1×FtntTseq1PUn+1t=seq1×Ftn+1
157 104 116 113 156 syl21anc nφtTn1Mseq1PUnt=seq1×FtnφtTn+11Mseq1PUn+1t=seq1×Ftn+1
158 157 3exp nφtTn1Mseq1PUnt=seq1×FtnφtTn+11Mseq1PUn+1t=seq1×Ftn+1
159 29 36 43 50 103 158 nnind MφtTM1Mseq1PUMt=seq1×FtM
160 22 159 mpcom φtTM1Mseq1PUMt=seq1×FtM
161 21 160 mpd3an3 φtTseq1PUMt=seq1×FtM
162 4 fveq1i Xt=seq1PUMt
163 162 a1i φtTXt=seq1PUMt
164 simpr φtTtT
165 elnnuz MM1
166 8 165 sylib φM1
167 166 adantr φtTM1
168 1 58 nfan iφtT
169 nfv ik1M
170 168 169 nfan iφtTk1M
171 nfcv _ik
172 64 171 nffv _iFtk
173 172 nfel1 iFtk
174 170 173 nfim iφtTk1MFtk
175 eleq1 i=ki1Mk1M
176 175 anbi2d i=kφtTi1MφtTk1M
177 fveq2 i=kFti=Ftk
178 177 eleq1d i=kFtiFtk
179 176 178 imbi12d i=kφtTi1MFtiφtTk1MFtk
180 78 ad2antlr φtTi1MFti=i1MUiti
181 simpr φtTi1Mi1M
182 9 ffvelrnda φi1MUiY
183 simpl φi1Mφ
184 183 182 jca φi1MφUiY
185 eleq1 f=UifYUiY
186 185 anbi2d f=UiφfYφUiY
187 feq1 f=Uif:TUi:T
188 186 187 imbi12d f=UiφfYf:TφUiYUi:T
189 188 92 vtoclga UiYφUiYUi:T
190 182 184 189 sylc φi1MUi:T
191 190 adantlr φtTi1MUi:T
192 simplr φtTi1MtT
193 191 192 ffvelrnd φtTi1MUit
194 82 fvmpt2 i1MUiti1MUiti=Uit
195 181 193 194 syl2anc φtTi1Mi1MUiti=Uit
196 195 193 eqeltrd φtTi1Mi1MUiti
197 180 196 eqeltrd φtTi1MFti
198 174 179 197 chvarfv φtTk1MFtk
199 remulcl kbkb
200 199 adantl φtTkbkb
201 167 198 200 seqcl φtTseq1×FtM
202 6 fvmpt2 tTseq1×FtMZt=seq1×FtM
203 164 201 202 syl2anc φtTZt=seq1×FtM
204 161 163 203 3eqtr4d φtTXt=Zt