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