# 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}\phantom{\rule{.4em}{0ex}}{\phi }$
fmuldfeq.2 ${⊢}\underset{_}{Ⅎ}{t}\phantom{\rule{.4em}{0ex}}{Y}$
fmuldfeq.3 ${⊢}{P}=\left({f}\in {Y},{g}\in {Y}⟼\left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)\right)$
fmuldfeq.4 ${⊢}{X}=seq1\left({P},{U}\right)\left({M}\right)$
fmuldfeq.5 ${⊢}{F}=\left({t}\in {T}⟼\left({i}\in \left(1\dots {M}\right)⟼{U}\left({i}\right)\left({t}\right)\right)\right)$
fmuldfeq.6 ${⊢}{Z}=\left({t}\in {T}⟼seq1\left(×,{F}\left({t}\right)\right)\left({M}\right)\right)$
fmuldfeq.7 ${⊢}{\phi }\to {T}\in \mathrm{V}$
fmuldfeq.8 ${⊢}{\phi }\to {M}\in ℕ$
fmuldfeq.9 ${⊢}{\phi }\to {U}:\left(1\dots {M}\right)⟶{Y}$
fmuldfeq.10 ${⊢}\left({\phi }\wedge {f}\in {Y}\right)\to {f}:{T}⟶ℝ$
fmuldfeq.11 ${⊢}\left({\phi }\wedge {f}\in {Y}\wedge {g}\in {Y}\right)\to \left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)\in {Y}$
Assertion fmuldfeq ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to {X}\left({t}\right)={Z}\left({t}\right)$

### Proof

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