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