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 ) − ( 𝑇 ‘ 𝑀 ) ) ) )