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 ⊢ Ⅎ 𝑖 𝜑
fmuldfeq.2 ⊢ Ⅎ 𝑡 𝑌
fmuldfeq.3 ⊢ 𝑃 = ( 𝑓 ∈ 𝑌 , 𝑔 ∈ 𝑌 ↦ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) )
fmuldfeq.4 ⊢ 𝑋 = ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑀 )
fmuldfeq.5 ⊢ 𝐹 = ( 𝑡 ∈ 𝑇 ↦ ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ) )
fmuldfeq.6 ⊢ 𝑍 = ( 𝑡 ∈ 𝑇 ↦ ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ 𝑀 ) )
fmuldfeq.7 ⊢ ( 𝜑 → 𝑇 ∈ V )
fmuldfeq.8 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fmuldfeq.9 ⊢ ( 𝜑 → 𝑈 : ( 1 ... 𝑀 ) ⟶ 𝑌 )
fmuldfeq.10 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ) → 𝑓 : 𝑇 ⟶ ℝ )
fmuldfeq.11 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝑌 )
Assertion fmuldfeq ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑋 ‘ 𝑡 ) = ( 𝑍 ‘ 𝑡 ) )

Proof

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