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 |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑋 ‘ 𝑡 ) = ( 𝑍 ‘ 𝑡 ) ) |