Step |
Hyp |
Ref |
Expression |
1 |
|
chpmatply1.c |
⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 ) |
2 |
|
chpmatply1.a |
⊢ 𝐴 = ( 𝑁 Mat 𝑅 ) |
3 |
|
chpmatply1.b |
⊢ 𝐵 = ( Base ‘ 𝐴 ) |
4 |
|
chpmatply1.p |
⊢ 𝑃 = ( Poly1 ‘ 𝑅 ) |
5 |
|
chpmatval2.y |
⊢ 𝑌 = ( 𝑁 Mat 𝑃 ) |
6 |
|
chpmatval2.m1 |
⊢ − = ( -g ‘ 𝑌 ) |
7 |
|
chpmatval2.x |
⊢ 𝑋 = ( var1 ‘ 𝑅 ) |
8 |
|
chpmatval2.t1 |
⊢ · = ( ·𝑠 ‘ 𝑌 ) |
9 |
|
chpmatval2.t |
⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 ) |
10 |
|
chpmatval2.i |
⊢ 1 = ( 1r ‘ 𝑌 ) |
11 |
|
chpmatval2.g |
⊢ 𝐺 = ( SymGrp ‘ 𝑁 ) |
12 |
|
chpmatval2.h |
⊢ 𝐻 = ( Base ‘ 𝐺 ) |
13 |
|
chpmatval2.z |
⊢ 𝑍 = ( ℤRHom ‘ 𝑃 ) |
14 |
|
chpmatval2.s |
⊢ 𝑆 = ( pmSgn ‘ 𝑁 ) |
15 |
|
chpmatval2.u |
⊢ 𝑈 = ( mulGrp ‘ 𝑃 ) |
16 |
|
chpmatval2.rm |
⊢ × = ( .r ‘ 𝑃 ) |
17 |
|
eqid |
⊢ ( 𝑁 maDet 𝑃 ) = ( 𝑁 maDet 𝑃 ) |
18 |
1 2 3 4 5 17 6 7 8 9 10
|
chpmatval |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 ‘ 𝑀 ) = ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) ) |
19 |
|
eqid |
⊢ ( 𝑁 Mat 𝑃 ) = ( 𝑁 Mat 𝑃 ) |
20 |
5
|
fveq2i |
⊢ ( -g ‘ 𝑌 ) = ( -g ‘ ( 𝑁 Mat 𝑃 ) ) |
21 |
6 20
|
eqtri |
⊢ − = ( -g ‘ ( 𝑁 Mat 𝑃 ) ) |
22 |
5
|
fveq2i |
⊢ ( ·𝑠 ‘ 𝑌 ) = ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) |
23 |
8 22
|
eqtri |
⊢ · = ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) |
24 |
5
|
fveq2i |
⊢ ( 1r ‘ 𝑌 ) = ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) |
25 |
10 24
|
eqtri |
⊢ 1 = ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) |
26 |
|
eqid |
⊢ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) |
27 |
2 3 4 19 7 9 21 23 25 26
|
chmatcl |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) ) |
28 |
5
|
eqcomi |
⊢ ( 𝑁 Mat 𝑃 ) = 𝑌 |
29 |
28
|
fveq2i |
⊢ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) = ( Base ‘ 𝑌 ) |
30 |
11
|
fveq2i |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) ) |
31 |
12 30
|
eqtri |
⊢ 𝐻 = ( Base ‘ ( SymGrp ‘ 𝑁 ) ) |
32 |
17 5 29 31 13 14 16 15
|
mdetleib |
⊢ ( ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) → ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) = ( 𝑃 Σg ( 𝑝 ∈ 𝐻 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) × ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) 𝑥 ) ) ) ) ) ) ) |
33 |
27 32
|
syl |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) = ( 𝑃 Σg ( 𝑝 ∈ 𝐻 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) × ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) 𝑥 ) ) ) ) ) ) ) |
34 |
18 33
|
eqtrd |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 ‘ 𝑀 ) = ( 𝑃 Σg ( 𝑝 ∈ 𝐻 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) × ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) 𝑥 ) ) ) ) ) ) ) |