Step | Hyp | Ref
| Expression |
1 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑎𝐴 |
2 | | nfcsb1v 3515 |
. . . . . 6
⊢
Ⅎ𝑢⦋𝑎 / 𝑢⦌𝐴 |
3 | | csbeq1a 3508 |
. . . . . 6
⊢ (𝑢 = 𝑎 → 𝐴 = ⦋𝑎 / 𝑢⦌𝐴) |
4 | 1, 2, 3 | cbvmpt 4677 |
. . . . 5
⊢ (𝑢 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) = (𝑎 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦
⦋𝑎 / 𝑢⦌𝐴) |
5 | 4 | fveq1i 6104 |
. . . 4
⊢ ((𝑢 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴)‘(𝑡 ↾ (1...𝑁))) = ((𝑎 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦
⦋𝑎 / 𝑢⦌𝐴)‘(𝑡 ↾ (1...𝑁))) |
6 | | rabdiophlem2.1 |
. . . . . . 7
⊢ 𝑀 = (𝑁 + 1) |
7 | 6 | mapfzcons1cl 36299 |
. . . . . 6
⊢ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑀)) → (𝑡 ↾ (1...𝑁)) ∈ (ℤ
↑𝑚 (1...𝑁))) |
8 | 7 | adantl 481 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ (𝑢 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) ∧ 𝑡 ∈ (ℤ ↑𝑚
(1...𝑀))) → (𝑡 ↾ (1...𝑁)) ∈ (ℤ
↑𝑚 (1...𝑁))) |
9 | | mzpf 36317 |
. . . . . . . 8
⊢ ((𝑢 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) → (𝑢 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴):(ℤ
↑𝑚 (1...𝑁))⟶ℤ) |
10 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑢 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) = (𝑢 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴) |
11 | 10 | fmpt 6289 |
. . . . . . . 8
⊢
(∀𝑢 ∈
(ℤ ↑𝑚 (1...𝑁))𝐴 ∈ ℤ ↔ (𝑢 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴):(ℤ
↑𝑚 (1...𝑁))⟶ℤ) |
12 | 9, 11 | sylibr 223 |
. . . . . . 7
⊢ ((𝑢 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) → ∀𝑢 ∈ (ℤ
↑𝑚 (1...𝑁))𝐴 ∈ ℤ) |
13 | 12 | ad2antlr 759 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ (𝑢 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) ∧ 𝑡 ∈ (ℤ ↑𝑚
(1...𝑀))) →
∀𝑢 ∈ (ℤ
↑𝑚 (1...𝑁))𝐴 ∈ ℤ) |
14 | | nfcsb1v 3515 |
. . . . . . . 8
⊢
Ⅎ𝑢⦋(𝑡 ↾ (1...𝑁)) / 𝑢⦌𝐴 |
15 | 14 | nfel1 2765 |
. . . . . . 7
⊢
Ⅎ𝑢⦋(𝑡 ↾ (1...𝑁)) / 𝑢⦌𝐴 ∈ ℤ |
16 | | csbeq1a 3508 |
. . . . . . . 8
⊢ (𝑢 = (𝑡 ↾ (1...𝑁)) → 𝐴 = ⦋(𝑡 ↾ (1...𝑁)) / 𝑢⦌𝐴) |
17 | 16 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑢 = (𝑡 ↾ (1...𝑁)) → (𝐴 ∈ ℤ ↔ ⦋(𝑡 ↾ (1...𝑁)) / 𝑢⦌𝐴 ∈ ℤ)) |
18 | 15, 17 | rspc 3276 |
. . . . . 6
⊢ ((𝑡 ↾ (1...𝑁)) ∈ (ℤ
↑𝑚 (1...𝑁)) → (∀𝑢 ∈ (ℤ ↑𝑚
(1...𝑁))𝐴 ∈ ℤ → ⦋(𝑡 ↾ (1...𝑁)) / 𝑢⦌𝐴 ∈ ℤ)) |
19 | 8, 13, 18 | sylc 63 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ (𝑢 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) ∧ 𝑡 ∈ (ℤ ↑𝑚
(1...𝑀))) →
⦋(𝑡 ↾
(1...𝑁)) / 𝑢⦌𝐴 ∈ ℤ) |
20 | | csbeq1 3502 |
. . . . . 6
⊢ (𝑎 = (𝑡 ↾ (1...𝑁)) → ⦋𝑎 / 𝑢⦌𝐴 = ⦋(𝑡 ↾ (1...𝑁)) / 𝑢⦌𝐴) |
21 | | eqid 2610 |
. . . . . 6
⊢ (𝑎 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ ⦋𝑎 / 𝑢⦌𝐴) = (𝑎 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦
⦋𝑎 / 𝑢⦌𝐴) |
22 | 20, 21 | fvmptg 6189 |
. . . . 5
⊢ (((𝑡 ↾ (1...𝑁)) ∈ (ℤ
↑𝑚 (1...𝑁)) ∧ ⦋(𝑡 ↾ (1...𝑁)) / 𝑢⦌𝐴 ∈ ℤ) → ((𝑎 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦
⦋𝑎 / 𝑢⦌𝐴)‘(𝑡 ↾ (1...𝑁))) = ⦋(𝑡 ↾ (1...𝑁)) / 𝑢⦌𝐴) |
23 | 8, 19, 22 | syl2anc 691 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ (𝑢 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) ∧ 𝑡 ∈ (ℤ ↑𝑚
(1...𝑀))) → ((𝑎 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ ⦋𝑎 / 𝑢⦌𝐴)‘(𝑡 ↾ (1...𝑁))) = ⦋(𝑡 ↾ (1...𝑁)) / 𝑢⦌𝐴) |
24 | 5, 23 | syl5req 2657 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ (𝑢 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) ∧ 𝑡 ∈ (ℤ ↑𝑚
(1...𝑀))) →
⦋(𝑡 ↾
(1...𝑁)) / 𝑢⦌𝐴 = ((𝑢 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘(𝑡 ↾ (1...𝑁)))) |
25 | 24 | mpteq2dva 4672 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (𝑢 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (𝑡 ∈ (ℤ ↑𝑚
(1...𝑀)) ↦
⦋(𝑡 ↾
(1...𝑁)) / 𝑢⦌𝐴) = (𝑡 ∈ (ℤ ↑𝑚
(1...𝑀)) ↦ ((𝑢 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴)‘(𝑡 ↾ (1...𝑁))))) |
26 | | ovex 6577 |
. . . 4
⊢
(1...𝑀) ∈
V |
27 | 26 | a1i 11 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑢 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (1...𝑀) ∈ V) |
28 | | fzssp1 12255 |
. . . . 5
⊢
(1...𝑁) ⊆
(1...(𝑁 +
1)) |
29 | 6 | oveq2i 6560 |
. . . . 5
⊢
(1...𝑀) =
(1...(𝑁 +
1)) |
30 | 28, 29 | sseqtr4i 3601 |
. . . 4
⊢
(1...𝑁) ⊆
(1...𝑀) |
31 | 30 | a1i 11 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑢 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (1...𝑁) ⊆ (1...𝑀)) |
32 | | simpr 476 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑢 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (𝑢 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴) ∈
(mzPoly‘(1...𝑁))) |
33 | | mzpresrename 36331 |
. . 3
⊢
(((1...𝑀) ∈ V
∧ (1...𝑁) ⊆
(1...𝑀) ∧ (𝑢 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (𝑡 ∈ (ℤ ↑𝑚
(1...𝑀)) ↦ ((𝑢 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴)‘(𝑡 ↾ (1...𝑁)))) ∈ (mzPoly‘(1...𝑀))) |
34 | 27, 31, 32, 33 | syl3anc 1318 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (𝑢 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (𝑡 ∈ (ℤ ↑𝑚
(1...𝑀)) ↦ ((𝑢 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴)‘(𝑡 ↾ (1...𝑁)))) ∈ (mzPoly‘(1...𝑀))) |
35 | 25, 34 | eqeltrd 2688 |
1
⊢ ((𝑁 ∈ ℕ0
∧ (𝑢 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (𝑡 ∈ (ℤ ↑𝑚
(1...𝑀)) ↦
⦋(𝑡 ↾
(1...𝑁)) / 𝑢⦌𝐴) ∈ (mzPoly‘(1...𝑀))) |