Step | Hyp | Ref
| Expression |
1 | | chfacfisf.0 |
. . . 4
⊢ 0 =
(0g‘𝑌) |
2 | 1 | fvexi 6686 |
. . 3
⊢ 0 ∈
V |
3 | 2 | a1i 11 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 0 ∈ V) |
4 | | ovexd 7193 |
. 2
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ ℕ0) → ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) ∈ V) |
5 | | nnnn0 11907 |
. . . . 5
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℕ0) |
6 | | peano2nn0 11940 |
. . . . 5
⊢ (𝑠 ∈ ℕ0
→ (𝑠 + 1) ∈
ℕ0) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝑠 ∈ ℕ → (𝑠 + 1) ∈
ℕ0) |
8 | 7 | ad2antrl 726 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑠 + 1) ∈
ℕ0) |
9 | | vex 3499 |
. . . . . . 7
⊢ 𝑘 ∈ V |
10 | | csbov12g 7202 |
. . . . . . . 8
⊢ (𝑘 ∈ V →
⦋𝑘 / 𝑖⦌((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = (⦋𝑘 / 𝑖⦌(𝑖 ↑ 𝑋) ·
⦋𝑘 / 𝑖⦌(𝐺‘𝑖))) |
11 | | csbov1g 7203 |
. . . . . . . . . 10
⊢ (𝑘 ∈ V →
⦋𝑘 / 𝑖⦌(𝑖 ↑ 𝑋) = (⦋𝑘 / 𝑖⦌𝑖 ↑ 𝑋)) |
12 | | csbvarg 4385 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ V →
⦋𝑘 / 𝑖⦌𝑖 = 𝑘) |
13 | 12 | oveq1d 7173 |
. . . . . . . . . 10
⊢ (𝑘 ∈ V →
(⦋𝑘 / 𝑖⦌𝑖 ↑ 𝑋) = (𝑘 ↑ 𝑋)) |
14 | 11, 13 | eqtrd 2858 |
. . . . . . . . 9
⊢ (𝑘 ∈ V →
⦋𝑘 / 𝑖⦌(𝑖 ↑ 𝑋) = (𝑘 ↑ 𝑋)) |
15 | | csbfv 6717 |
. . . . . . . . . 10
⊢
⦋𝑘 /
𝑖⦌(𝐺‘𝑖) = (𝐺‘𝑘) |
16 | 15 | a1i 11 |
. . . . . . . . 9
⊢ (𝑘 ∈ V →
⦋𝑘 / 𝑖⦌(𝐺‘𝑖) = (𝐺‘𝑘)) |
17 | 14, 16 | oveq12d 7176 |
. . . . . . . 8
⊢ (𝑘 ∈ V →
(⦋𝑘 / 𝑖⦌(𝑖 ↑ 𝑋) ·
⦋𝑘 / 𝑖⦌(𝐺‘𝑖)) = ((𝑘 ↑ 𝑋) · (𝐺‘𝑘))) |
18 | 10, 17 | eqtrd 2858 |
. . . . . . 7
⊢ (𝑘 ∈ V →
⦋𝑘 / 𝑖⦌((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = ((𝑘 ↑ 𝑋) · (𝐺‘𝑘))) |
19 | 9, 18 | mp1i 13 |
. . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → ⦋𝑘 / 𝑖⦌((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = ((𝑘 ↑ 𝑋) · (𝐺‘𝑘))) |
20 | | simplll 773 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵)) |
21 | | simpllr 774 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) |
22 | 5 | adantr 483 |
. . . . . . . . . . . 12
⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑠 ∈ ℕ0) |
23 | 22 | ad2antlr 725 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) → 𝑠 ∈
ℕ0) |
24 | 23 | nn0zd 12088 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) → 𝑠 ∈
ℤ) |
25 | 24 | adantr 483 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → 𝑠 ∈ ℤ) |
26 | | 2z 12017 |
. . . . . . . . . 10
⊢ 2 ∈
ℤ |
27 | 26 | a1i 11 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → 2 ∈ ℤ) |
28 | 25, 27 | zaddcld 12094 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → (𝑠 + 2) ∈ ℤ) |
29 | | simplr 767 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → 𝑘 ∈ ℕ0) |
30 | 29 | nn0zd 12088 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → 𝑘 ∈ ℤ) |
31 | 8 | nn0zd 12088 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑠 + 1) ∈ ℤ) |
32 | | nn0z 12008 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℤ) |
33 | | zltp1le 12035 |
. . . . . . . . . . 11
⊢ (((𝑠 + 1) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑠 + 1) < 𝑘 ↔ ((𝑠 + 1) + 1) ≤ 𝑘)) |
34 | 31, 32, 33 | syl2an 597 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) → ((𝑠 + 1) < 𝑘 ↔ ((𝑠 + 1) + 1) ≤ 𝑘)) |
35 | 34 | biimpa 479 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → ((𝑠 + 1) + 1) ≤ 𝑘) |
36 | | nncn 11648 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℂ) |
37 | | add1p1 11891 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ ℂ → ((𝑠 + 1) + 1) = (𝑠 + 2)) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ℕ → ((𝑠 + 1) + 1) = (𝑠 + 2)) |
39 | 38 | breq1d 5078 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℕ → (((𝑠 + 1) + 1) ≤ 𝑘 ↔ (𝑠 + 2) ≤ 𝑘)) |
40 | 39 | bicomd 225 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ ℕ → ((𝑠 + 2) ≤ 𝑘 ↔ ((𝑠 + 1) + 1) ≤ 𝑘)) |
41 | 40 | adantr 483 |
. . . . . . . . . . 11
⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → ((𝑠 + 2) ≤ 𝑘 ↔ ((𝑠 + 1) + 1) ≤ 𝑘)) |
42 | 41 | ad2antlr 725 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) → ((𝑠 + 2) ≤ 𝑘 ↔ ((𝑠 + 1) + 1) ≤ 𝑘)) |
43 | 42 | adantr 483 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → ((𝑠 + 2) ≤ 𝑘 ↔ ((𝑠 + 1) + 1) ≤ 𝑘)) |
44 | 35, 43 | mpbird 259 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → (𝑠 + 2) ≤ 𝑘) |
45 | | eluz2 12252 |
. . . . . . . 8
⊢ (𝑘 ∈
(ℤ≥‘(𝑠 + 2)) ↔ ((𝑠 + 2) ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ (𝑠 + 2) ≤ 𝑘)) |
46 | 28, 30, 44, 45 | syl3anbrc 1339 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → 𝑘 ∈ (ℤ≥‘(𝑠 + 2))) |
47 | | chfacfisf.a |
. . . . . . . 8
⊢ 𝐴 = (𝑁 Mat 𝑅) |
48 | | chfacfisf.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐴) |
49 | | chfacfisf.p |
. . . . . . . 8
⊢ 𝑃 = (Poly1‘𝑅) |
50 | | chfacfisf.y |
. . . . . . . 8
⊢ 𝑌 = (𝑁 Mat 𝑃) |
51 | | chfacfisf.r |
. . . . . . . 8
⊢ × =
(.r‘𝑌) |
52 | | chfacfisf.s |
. . . . . . . 8
⊢ − =
(-g‘𝑌) |
53 | | chfacfisf.t |
. . . . . . . 8
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
54 | | chfacfisf.g |
. . . . . . . 8
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) |
55 | | chfacfscmulcl.x |
. . . . . . . 8
⊢ 𝑋 = (var1‘𝑅) |
56 | | chfacfscmulcl.m |
. . . . . . . 8
⊢ · = (
·𝑠 ‘𝑌) |
57 | | chfacfscmulcl.e |
. . . . . . . 8
⊢ ↑ =
(.g‘(mulGrp‘𝑃)) |
58 | 47, 48, 49, 50, 51, 52, 1, 53, 54, 55, 56, 57 | chfacfscmul0 21468 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑘 ∈ (ℤ≥‘(𝑠 + 2))) → ((𝑘 ↑ 𝑋) · (𝐺‘𝑘)) = 0 ) |
59 | 20, 21, 46, 58 | syl3anc 1367 |
. . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → ((𝑘 ↑ 𝑋) · (𝐺‘𝑘)) = 0 ) |
60 | 19, 59 | eqtrd 2858 |
. . . . 5
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → ⦋𝑘 / 𝑖⦌((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = 0 ) |
61 | 60 | ex 415 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) → ((𝑠 + 1) < 𝑘 → ⦋𝑘 / 𝑖⦌((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = 0 )) |
62 | 61 | ralrimiva 3184 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ∀𝑘 ∈ ℕ0 ((𝑠 + 1) < 𝑘 → ⦋𝑘 / 𝑖⦌((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = 0 )) |
63 | | breq1 5071 |
. . . 4
⊢ (𝑧 = (𝑠 + 1) → (𝑧 < 𝑘 ↔ (𝑠 + 1) < 𝑘)) |
64 | 63 | rspceaimv 3630 |
. . 3
⊢ (((𝑠 + 1) ∈ ℕ0
∧ ∀𝑘 ∈
ℕ0 ((𝑠 +
1) < 𝑘 →
⦋𝑘 / 𝑖⦌((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = 0 )) → ∃𝑧 ∈ ℕ0
∀𝑘 ∈
ℕ0 (𝑧 <
𝑘 →
⦋𝑘 / 𝑖⦌((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = 0 )) |
65 | 8, 62, 64 | syl2anc 586 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ∃𝑧 ∈ ℕ0 ∀𝑘 ∈ ℕ0
(𝑧 < 𝑘 → ⦋𝑘 / 𝑖⦌((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = 0 )) |
66 | 3, 4, 65 | mptnn0fsupp 13368 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))) finSupp 0 ) |