Metamath Proof Explorer


Theorem chpmatval

Description: The characteristic polynomial of a (square) matrix (expressed with a determinant). (Contributed by AV, 2-Aug-2019)

Ref Expression
Hypotheses chpmatfval.c 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
chpmatfval.a 𝐴 = ( 𝑁 Mat 𝑅 )
chpmatfval.b 𝐵 = ( Base ‘ 𝐴 )
chpmatfval.p 𝑃 = ( Poly1𝑅 )
chpmatfval.y 𝑌 = ( 𝑁 Mat 𝑃 )
chpmatfval.d 𝐷 = ( 𝑁 maDet 𝑃 )
chpmatfval.s = ( -g𝑌 )
chpmatfval.x 𝑋 = ( var1𝑅 )
chpmatfval.m · = ( ·𝑠𝑌 )
chpmatfval.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
chpmatfval.i 1 = ( 1r𝑌 )
Assertion chpmatval ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝐵 ) → ( 𝐶𝑀 ) = ( 𝐷 ‘ ( ( 𝑋 · 1 ) ( 𝑇𝑀 ) ) ) )

Proof

Step Hyp Ref Expression
1 chpmatfval.c 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
2 chpmatfval.a 𝐴 = ( 𝑁 Mat 𝑅 )
3 chpmatfval.b 𝐵 = ( Base ‘ 𝐴 )
4 chpmatfval.p 𝑃 = ( Poly1𝑅 )
5 chpmatfval.y 𝑌 = ( 𝑁 Mat 𝑃 )
6 chpmatfval.d 𝐷 = ( 𝑁 maDet 𝑃 )
7 chpmatfval.s = ( -g𝑌 )
8 chpmatfval.x 𝑋 = ( var1𝑅 )
9 chpmatfval.m · = ( ·𝑠𝑌 )
10 chpmatfval.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
11 chpmatfval.i 1 = ( 1r𝑌 )
12 1 2 3 4 5 6 7 8 9 10 11 chpmatfval ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → 𝐶 = ( 𝑚𝐵 ↦ ( 𝐷 ‘ ( ( 𝑋 · 1 ) ( 𝑇𝑚 ) ) ) ) )
13 12 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝐵 ) → 𝐶 = ( 𝑚𝐵 ↦ ( 𝐷 ‘ ( ( 𝑋 · 1 ) ( 𝑇𝑚 ) ) ) ) )
14 fveq2 ( 𝑚 = 𝑀 → ( 𝑇𝑚 ) = ( 𝑇𝑀 ) )
15 14 oveq2d ( 𝑚 = 𝑀 → ( ( 𝑋 · 1 ) ( 𝑇𝑚 ) ) = ( ( 𝑋 · 1 ) ( 𝑇𝑀 ) ) )
16 15 fveq2d ( 𝑚 = 𝑀 → ( 𝐷 ‘ ( ( 𝑋 · 1 ) ( 𝑇𝑚 ) ) ) = ( 𝐷 ‘ ( ( 𝑋 · 1 ) ( 𝑇𝑀 ) ) ) )
17 16 adantl ( ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝐵 ) ∧ 𝑚 = 𝑀 ) → ( 𝐷 ‘ ( ( 𝑋 · 1 ) ( 𝑇𝑚 ) ) ) = ( 𝐷 ‘ ( ( 𝑋 · 1 ) ( 𝑇𝑀 ) ) ) )
18 simp3 ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝐵 ) → 𝑀𝐵 )
19 fvexd ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝐵 ) → ( 𝐷 ‘ ( ( 𝑋 · 1 ) ( 𝑇𝑀 ) ) ) ∈ V )
20 13 17 18 19 fvmptd ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉𝑀𝐵 ) → ( 𝐶𝑀 ) = ( 𝐷 ‘ ( ( 𝑋 · 1 ) ( 𝑇𝑀 ) ) ) )