Step | Hyp | Ref
| Expression |
1 | | fmuldfeq.8 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
2 | 1 | nnge1d 10940 |
. . . . 5
⊢ (𝜑 → 1 ≤ 𝑀) |
3 | 2 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 ≤ 𝑀) |
4 | | nnre 10904 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
5 | | leid 10012 |
. . . . . 6
⊢ (𝑀 ∈ ℝ → 𝑀 ≤ 𝑀) |
6 | 1, 4, 5 | 3syl 18 |
. . . . 5
⊢ (𝜑 → 𝑀 ≤ 𝑀) |
7 | 6 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑀 ≤ 𝑀) |
8 | 1 | nnzd 11357 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
9 | 8 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑀 ∈ ℤ) |
10 | | 1zzd 11285 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 ∈ ℤ) |
11 | | elfz 12203 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 1 ∈
ℤ ∧ 𝑀 ∈
ℤ) → (𝑀 ∈
(1...𝑀) ↔ (1 ≤
𝑀 ∧ 𝑀 ≤ 𝑀))) |
12 | 9, 10, 9, 11 | syl3anc 1318 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑀 ∈ (1...𝑀) ↔ (1 ≤ 𝑀 ∧ 𝑀 ≤ 𝑀))) |
13 | 3, 7, 12 | mpbir2and 959 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑀 ∈ (1...𝑀)) |
14 | 1 | 3ad2ant1 1075 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀)) → 𝑀 ∈ ℕ) |
15 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑚 = 1 → (𝑚 ∈ (1...𝑀) ↔ 1 ∈ (1...𝑀))) |
16 | 15 | 3anbi3d 1397 |
. . . . . 6
⊢ (𝑚 = 1 → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 1 ∈ (1...𝑀)))) |
17 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑚 = 1 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘1)) |
18 | 17 | fveq1d 6105 |
. . . . . . 7
⊢ (𝑚 = 1 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘1)‘𝑡)) |
19 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑚 = 1 → (seq1( · ,
(𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘1)) |
20 | 18, 19 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑚 = 1 → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘1))) |
21 | 16, 20 | imbi12d 333 |
. . . . 5
⊢ (𝑚 = 1 → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 1 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘1)))) |
22 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (𝑚 ∈ (1...𝑀) ↔ 𝑛 ∈ (1...𝑀))) |
23 | 22 | 3anbi3d 1397 |
. . . . . 6
⊢ (𝑚 = 𝑛 → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)))) |
24 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘𝑛)) |
25 | 24 | fveq1d 6105 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡)) |
26 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘𝑛)) |
27 | 25, 26 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑚 = 𝑛 → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) |
28 | 23, 27 | imbi12d 333 |
. . . . 5
⊢ (𝑚 = 𝑛 → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)))) |
29 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑚 = (𝑛 + 1) → (𝑚 ∈ (1...𝑀) ↔ (𝑛 + 1) ∈ (1...𝑀))) |
30 | 29 | 3anbi3d 1397 |
. . . . . 6
⊢ (𝑚 = (𝑛 + 1) → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀)))) |
31 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑚 = (𝑛 + 1) → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘(𝑛 + 1))) |
32 | 31 | fveq1d 6105 |
. . . . . . 7
⊢ (𝑚 = (𝑛 + 1) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡)) |
33 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑚 = (𝑛 + 1) → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1))) |
34 | 32, 33 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑚 = (𝑛 + 1) → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1)))) |
35 | 30, 34 | imbi12d 333 |
. . . . 5
⊢ (𝑚 = (𝑛 + 1) → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1))))) |
36 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (𝑚 ∈ (1...𝑀) ↔ 𝑀 ∈ (1...𝑀))) |
37 | 36 | 3anbi3d 1397 |
. . . . . 6
⊢ (𝑚 = 𝑀 → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀)))) |
38 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘𝑀)) |
39 | 38 | fveq1d 6105 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡)) |
40 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (seq1( · , (𝐹‘𝑡))‘𝑚) = (seq1( · , (𝐹‘𝑡))‘𝑀)) |
41 | 39, 40 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))) |
42 | 37, 41 | imbi12d 333 |
. . . . 5
⊢ (𝑚 = 𝑀 → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑚)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀)))) |
43 | | 1z 11284 |
. . . . . . . 8
⊢ 1 ∈
ℤ |
44 | | seq1 12676 |
. . . . . . . 8
⊢ (1 ∈
ℤ → (seq1( · , (𝐹‘𝑡))‘1) = ((𝐹‘𝑡)‘1)) |
45 | 43, 44 | ax-mp 5 |
. . . . . . 7
⊢ (seq1(
· , (𝐹‘𝑡))‘1) = ((𝐹‘𝑡)‘1) |
46 | | 1le1 10534 |
. . . . . . . . . . . . 13
⊢ 1 ≤
1 |
47 | 46 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ≤ 1) |
48 | | 1zzd 11285 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈
ℤ) |
49 | | elfz 12203 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (1 ∈ (1...𝑀) ↔ (1 ≤ 1 ∧ 1 ≤
𝑀))) |
50 | 48, 48, 8, 49 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 ∈ (1...𝑀) ↔ (1 ≤ 1 ∧ 1 ≤
𝑀))) |
51 | 47, 2, 50 | mpbir2and 959 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈ (1...𝑀)) |
52 | | nfv 1830 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑖 𝑡 ∈ 𝑇 |
53 | | fmuldfeq.5 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))) |
54 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑖𝑇 |
55 | | nfmpt1 4675 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑖(𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) |
56 | 54, 55 | nfmpt 4674 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑖(𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))) |
57 | 53, 56 | nfcxfr 2749 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑖𝐹 |
58 | | nfcv 2751 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑖𝑡 |
59 | 57, 58 | nffv 6110 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑖(𝐹‘𝑡) |
60 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑖1 |
61 | 59, 60 | nffv 6110 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑖((𝐹‘𝑡)‘1) |
62 | | nffvmpt1 6111 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑖((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1) |
63 | 61, 62 | nfeq 2762 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑖((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1) |
64 | 52, 63 | nfim 1813 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖(𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)) |
65 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 1 → ((𝐹‘𝑡)‘𝑖) = ((𝐹‘𝑡)‘1)) |
66 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 1 → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)) |
67 | 65, 66 | eqeq12d 2625 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 1 → (((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) ↔ ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1))) |
68 | 67 | imbi2d 329 |
. . . . . . . . . . . 12
⊢ (𝑖 = 1 → ((𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖)) ↔ (𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)))) |
69 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑀) ∈
V |
70 | 69 | mptex 6390 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) ∈ V |
71 | 53 | fvmpt2 6200 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ 𝑇 ∧ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) ∈ V) → (𝐹‘𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))) |
72 | 70, 71 | mpan2 703 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ 𝑇 → (𝐹‘𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))) |
73 | 72 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖)) |
74 | 64, 68, 73 | vtoclg1f 3238 |
. . . . . . . . . . 11
⊢ (1 ∈
(1...𝑀) → (𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1))) |
75 | 51, 74 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑡 ∈ 𝑇 → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1))) |
76 | 75 | imp 444 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1)) |
77 | 51 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 ∈ (1...𝑀)) |
78 | | fmuldfeq.9 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈:(1...𝑀)⟶𝑌) |
79 | 78, 51 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑈‘1) ∈ 𝑌) |
80 | 79 | ancli 572 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝜑 ∧ (𝑈‘1) ∈ 𝑌)) |
81 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑈‘1) → (𝑓 ∈ 𝑌 ↔ (𝑈‘1) ∈ 𝑌)) |
82 | 81 | anbi2d 736 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑈‘1) → ((𝜑 ∧ 𝑓 ∈ 𝑌) ↔ (𝜑 ∧ (𝑈‘1) ∈ 𝑌))) |
83 | | feq1 5939 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑈‘1) → (𝑓:𝑇⟶ℝ ↔ (𝑈‘1):𝑇⟶ℝ)) |
84 | 82, 83 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑈‘1) → (((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝑈‘1) ∈ 𝑌) → (𝑈‘1):𝑇⟶ℝ))) |
85 | | fmuldfeq.10 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ) |
86 | 85 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ 𝑌 → ((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ)) |
87 | 84, 86 | vtoclga 3245 |
. . . . . . . . . . . 12
⊢ ((𝑈‘1) ∈ 𝑌 → ((𝜑 ∧ (𝑈‘1) ∈ 𝑌) → (𝑈‘1):𝑇⟶ℝ)) |
88 | 79, 80, 87 | sylc 63 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑈‘1):𝑇⟶ℝ) |
89 | 88 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑈‘1)‘𝑡) ∈ ℝ) |
90 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑖 = 1 → (𝑈‘𝑖) = (𝑈‘1)) |
91 | 90 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ (𝑖 = 1 → ((𝑈‘𝑖)‘𝑡) = ((𝑈‘1)‘𝑡)) |
92 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)) |
93 | 91, 92 | fvmptg 6189 |
. . . . . . . . . 10
⊢ ((1
∈ (1...𝑀) ∧
((𝑈‘1)‘𝑡) ∈ ℝ) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1) = ((𝑈‘1)‘𝑡)) |
94 | 77, 89, 93 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘1) = ((𝑈‘1)‘𝑡)) |
95 | 76, 94 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡)‘1) = ((𝑈‘1)‘𝑡)) |
96 | | seq1 12676 |
. . . . . . . . . 10
⊢ (1 ∈
ℤ → (seq1(𝑃,
𝑈)‘1) = (𝑈‘1)) |
97 | 43, 96 | ax-mp 5 |
. . . . . . . . 9
⊢
(seq1(𝑃, 𝑈)‘1) = (𝑈‘1) |
98 | 97 | fveq1i 6104 |
. . . . . . . 8
⊢
((seq1(𝑃, 𝑈)‘1)‘𝑡) = ((𝑈‘1)‘𝑡) |
99 | 95, 98 | syl6eqr 2662 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡)‘1) = ((seq1(𝑃, 𝑈)‘1)‘𝑡)) |
100 | 45, 99 | syl5req 2657 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘1)) |
101 | 100 | 3adant3 1074 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 1 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘1)) |
102 | | simp31 1090 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝜑) |
103 | | simp1 1054 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝑛 ∈ ℕ) |
104 | | simp33 1092 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → (𝑛 + 1) ∈ (1...𝑀)) |
105 | 103, 104 | jca 553 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑀))) |
106 | | elnnuz 11600 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈
(ℤ≥‘1)) |
107 | 106 | biimpi 205 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
(ℤ≥‘1)) |
108 | 107 | anim1i 590 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑀)) → (𝑛 ∈ (ℤ≥‘1)
∧ (𝑛 + 1) ∈
(1...𝑀))) |
109 | | peano2fzr 12225 |
. . . . . . . . 9
⊢ ((𝑛 ∈
(ℤ≥‘1) ∧ (𝑛 + 1) ∈ (1...𝑀)) → 𝑛 ∈ (1...𝑀)) |
110 | 105, 108,
109 | 3syl 18 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝑛 ∈ (1...𝑀)) |
111 | | simp32 1091 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝑡 ∈ 𝑇) |
112 | | simp2 1055 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) |
113 | 102, 111,
110, 112 | mp3and 1419 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) |
114 | 110, 104,
113 | 3jca 1235 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) |
115 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑓𝜑 |
116 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑓 𝑛 ∈ (1...𝑀) |
117 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑓(𝑛 + 1) ∈ (1...𝑀) |
118 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑓1 |
119 | | fmuldfeq.3 |
. . . . . . . . . . . . . . 15
⊢ 𝑃 = (𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡)))) |
120 | | nfmpt21 6620 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑓(𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡)))) |
121 | 119, 120 | nfcxfr 2749 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑓𝑃 |
122 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑓𝑈 |
123 | 118, 121,
122 | nfseq 12673 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑓seq1(𝑃, 𝑈) |
124 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑓𝑛 |
125 | 123, 124 | nffv 6110 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑓(seq1(𝑃, 𝑈)‘𝑛) |
126 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑓𝑡 |
127 | 125, 126 | nffv 6110 |
. . . . . . . . . . 11
⊢
Ⅎ𝑓((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) |
128 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑓(seq1( · , (𝐹‘𝑡))‘𝑛) |
129 | 127, 128 | nfeq 2762 |
. . . . . . . . . 10
⊢
Ⅎ𝑓((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛) |
130 | 116, 117,
129 | nf3an 1819 |
. . . . . . . . 9
⊢
Ⅎ𝑓(𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) |
131 | 115, 130 | nfan 1816 |
. . . . . . . 8
⊢
Ⅎ𝑓(𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) |
132 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑔𝜑 |
133 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑔 𝑛 ∈ (1...𝑀) |
134 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑔(𝑛 + 1) ∈ (1...𝑀) |
135 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑔1 |
136 | | nfmpt22 6621 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑔(𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡)))) |
137 | 119, 136 | nfcxfr 2749 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑔𝑃 |
138 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑔𝑈 |
139 | 135, 137,
138 | nfseq 12673 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑔seq1(𝑃, 𝑈) |
140 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑔𝑛 |
141 | 139, 140 | nffv 6110 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑔(seq1(𝑃, 𝑈)‘𝑛) |
142 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑔𝑡 |
143 | 141, 142 | nffv 6110 |
. . . . . . . . . . 11
⊢
Ⅎ𝑔((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) |
144 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑔(seq1( · , (𝐹‘𝑡))‘𝑛) |
145 | 143, 144 | nfeq 2762 |
. . . . . . . . . 10
⊢
Ⅎ𝑔((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛) |
146 | 133, 134,
145 | nf3an 1819 |
. . . . . . . . 9
⊢
Ⅎ𝑔(𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) |
147 | 132, 146 | nfan 1816 |
. . . . . . . 8
⊢
Ⅎ𝑔(𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) |
148 | | fmuldfeq.2 |
. . . . . . . 8
⊢
Ⅎ𝑡𝑌 |
149 | | fmuldfeq.7 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ V) |
150 | 149 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) → 𝑇 ∈ V) |
151 | 78 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) → 𝑈:(1...𝑀)⟶𝑌) |
152 | | fmuldfeq.11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝑌) |
153 | 152 | 3adant1r 1311 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝑌) |
154 | | simpr1 1060 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) → 𝑛 ∈ (1...𝑀)) |
155 | | simpr2 1061 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) → (𝑛 + 1) ∈ (1...𝑀)) |
156 | | simpr3 1062 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) |
157 | 85 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ) |
158 | 131, 147,
148, 119, 53, 150, 151, 153, 154, 155, 156, 157 | fmuldfeqlem1 38649 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛))) ∧ 𝑡 ∈ 𝑇) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1))) |
159 | 102, 114,
111, 158 | syl21anc 1317 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ ∧ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) ∧ (𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1))) |
160 | 159 | 3exp 1256 |
. . . . 5
⊢ (𝑛 ∈ ℕ → (((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑛)) → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑛 + 1))))) |
161 | 21, 28, 35, 42, 101, 160 | nnind 10915 |
. . . 4
⊢ (𝑀 ∈ ℕ → ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀))) |
162 | 14, 161 | mpcom 37 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑀 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀)) |
163 | 13, 162 | mpd3an3 1417 |
. 2
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀)) |
164 | | fmuldfeq.4 |
. . . 4
⊢ 𝑋 = (seq1(𝑃, 𝑈)‘𝑀) |
165 | 164 | fveq1i 6104 |
. . 3
⊢ (𝑋‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) |
166 | 165 | a1i 11 |
. 2
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑋‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡)) |
167 | | simpr 476 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇) |
168 | | elnnuz 11600 |
. . . . . 6
⊢ (𝑀 ∈ ℕ ↔ 𝑀 ∈
(ℤ≥‘1)) |
169 | 1, 168 | sylib 207 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
170 | 169 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑀 ∈
(ℤ≥‘1)) |
171 | | fmuldfeq.1 |
. . . . . . . 8
⊢
Ⅎ𝑖𝜑 |
172 | 171, 52 | nfan 1816 |
. . . . . . 7
⊢
Ⅎ𝑖(𝜑 ∧ 𝑡 ∈ 𝑇) |
173 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑖 𝑘 ∈ (1...𝑀) |
174 | 172, 173 | nfan 1816 |
. . . . . 6
⊢
Ⅎ𝑖((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀)) |
175 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑖𝑘 |
176 | 59, 175 | nffv 6110 |
. . . . . . 7
⊢
Ⅎ𝑖((𝐹‘𝑡)‘𝑘) |
177 | 176 | nfel1 2765 |
. . . . . 6
⊢
Ⅎ𝑖((𝐹‘𝑡)‘𝑘) ∈ ℝ |
178 | 174, 177 | nfim 1813 |
. . . . 5
⊢
Ⅎ𝑖(((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑘) ∈ ℝ) |
179 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑖 = 𝑘 → (𝑖 ∈ (1...𝑀) ↔ 𝑘 ∈ (1...𝑀))) |
180 | 179 | anbi2d 736 |
. . . . . 6
⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀)))) |
181 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑖 = 𝑘 → ((𝐹‘𝑡)‘𝑖) = ((𝐹‘𝑡)‘𝑘)) |
182 | 181 | eleq1d 2672 |
. . . . . 6
⊢ (𝑖 = 𝑘 → (((𝐹‘𝑡)‘𝑖) ∈ ℝ ↔ ((𝐹‘𝑡)‘𝑘) ∈ ℝ)) |
183 | 180, 182 | imbi12d 333 |
. . . . 5
⊢ (𝑖 = 𝑘 → ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑖) ∈ ℝ) ↔ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑘) ∈ ℝ))) |
184 | 73 | ad2antlr 759 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖)) |
185 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (1...𝑀)) |
186 | 78 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖) ∈ 𝑌) |
187 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝜑) |
188 | 187, 186 | jca 553 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌)) |
189 | | eleq1 2676 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑈‘𝑖) → (𝑓 ∈ 𝑌 ↔ (𝑈‘𝑖) ∈ 𝑌)) |
190 | 189 | anbi2d 736 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑈‘𝑖) → ((𝜑 ∧ 𝑓 ∈ 𝑌) ↔ (𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌))) |
191 | | feq1 5939 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑈‘𝑖) → (𝑓:𝑇⟶ℝ ↔ (𝑈‘𝑖):𝑇⟶ℝ)) |
192 | 190, 191 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑈‘𝑖) → (((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌) → (𝑈‘𝑖):𝑇⟶ℝ))) |
193 | 192, 86 | vtoclga 3245 |
. . . . . . . . . . 11
⊢ ((𝑈‘𝑖) ∈ 𝑌 → ((𝜑 ∧ (𝑈‘𝑖) ∈ 𝑌) → (𝑈‘𝑖):𝑇⟶ℝ)) |
194 | 186, 188,
193 | sylc 63 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖):𝑇⟶ℝ) |
195 | 194 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖):𝑇⟶ℝ) |
196 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 𝑡 ∈ 𝑇) |
197 | 195, 196 | ffvelrnd 6268 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈‘𝑖)‘𝑡) ∈ ℝ) |
198 | 92 | fvmpt2 6200 |
. . . . . . . 8
⊢ ((𝑖 ∈ (1...𝑀) ∧ ((𝑈‘𝑖)‘𝑡) ∈ ℝ) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) = ((𝑈‘𝑖)‘𝑡)) |
199 | 185, 197,
198 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) = ((𝑈‘𝑖)‘𝑡)) |
200 | 199, 197 | eqeltrd 2688 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))‘𝑖) ∈ ℝ) |
201 | 184, 200 | eqeltrd 2688 |
. . . . 5
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑖) ∈ ℝ) |
202 | 178, 183,
201 | chvar 2250 |
. . . 4
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹‘𝑡)‘𝑘) ∈ ℝ) |
203 | | remulcl 9900 |
. . . . 5
⊢ ((𝑘 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑘 · 𝑏) ∈ ℝ) |
204 | 203 | adantl 481 |
. . . 4
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑘 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (𝑘 · 𝑏) ∈ ℝ) |
205 | 170, 202,
204 | seqcl 12683 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (seq1( · , (𝐹‘𝑡))‘𝑀) ∈ ℝ) |
206 | | fmuldfeq.6 |
. . . 4
⊢ 𝑍 = (𝑡 ∈ 𝑇 ↦ (seq1( · , (𝐹‘𝑡))‘𝑀)) |
207 | 206 | fvmpt2 6200 |
. . 3
⊢ ((𝑡 ∈ 𝑇 ∧ (seq1( · , (𝐹‘𝑡))‘𝑀) ∈ ℝ) → (𝑍‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀)) |
208 | 167, 205,
207 | syl2anc 691 |
. 2
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑍‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑀)) |
209 | 163, 166,
208 | 3eqtr4d 2654 |
1
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑋‘𝑡) = (𝑍‘𝑡)) |