Definition df-chpmat

Description: Define the characteristic polynomial of a square matrix. According to Wikipedia ("Characteristic polynomial", 31-Jul-2019, https://en.wikipedia.org/wiki/Characteristic_polynomial ): "The characteristic polynomial of [an n x n matrix] A, denoted by p_A(t), is the polynomial defined by p_A ( t ) = det ( t I - A ) where I denotes the n-by-n identity matrix.". In addition, however, the underlying ring must be commutative, see definition in Lang, p. 561: " Let k be a commutative ring ... Let M be any n x n matrix in k ... We define the characteristic polynomial P_M(t) to be the determinant det ( t I_n - M ) where I_n is the unit n x n matrix." To be more precise, the matrices A and I on the right hand side are matrices with coefficients of a polynomial ring. Therefore, the original matrix A over a given commutative ring must be transformed into corresponding matrices over the polynomial ring over the given ring. (Contributed by AV, 2-Aug-2019)

	Ref	Expression
Assertion	df-chpmat	⊢ CharPlyMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( ( 𝑛 maDet ( Poly1 ‘ 𝑟 ) ) ‘ ( ( ( var1 ‘ 𝑟 ) ( ·𝑠 ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( 1r ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ) ( -g ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( ( 𝑛 matToPolyMat 𝑟 ) ‘ 𝑚 ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cchpmat	⊢ CharPlyMat
1		vn	⊢ 𝑛
2		cfn	⊢ Fin
3		vr	⊢ 𝑟
4		cvv	⊢ V
5		vm	⊢ 𝑚
6		cbs	⊢ Base
7	1	cv	⊢ 𝑛
8		cmat	⊢ Mat
9	3	cv	⊢ 𝑟
10	7 9 8	co	⊢ ( 𝑛 Mat 𝑟 )
11	10 6	cfv	⊢ ( Base ‘ ( 𝑛 Mat 𝑟 ) )
12		cmdat	⊢ maDet
13		cpl1	⊢ Poly1
14	9 13	cfv	⊢ ( Poly1 ‘ 𝑟 )
15	7 14 12	co	⊢ ( 𝑛 maDet ( Poly1 ‘ 𝑟 ) )
16		cv1	⊢ var1
17	9 16	cfv	⊢ ( var1 ‘ 𝑟 )
18		cvsca	⊢ ·𝑠
19	7 14 8	co	⊢ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) )
20	19 18	cfv	⊢ ( ·𝑠 ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) )
21		cur	⊢ 1r
22	19 21	cfv	⊢ ( 1r ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) )
23	17 22 20	co	⊢ ( ( var1 ‘ 𝑟 ) ( ·𝑠 ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( 1r ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) )
24		csg	⊢ -g
25	19 24	cfv	⊢ ( -g ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) )
26		cmat2pmat	⊢ matToPolyMat
27	7 9 26	co	⊢ ( 𝑛 matToPolyMat 𝑟 )
28	5	cv	⊢ 𝑚
29	28 27	cfv	⊢ ( ( 𝑛 matToPolyMat 𝑟 ) ‘ 𝑚 )
30	23 29 25	co	⊢ ( ( ( var1 ‘ 𝑟 ) ( ·𝑠 ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( 1r ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ) ( -g ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( ( 𝑛 matToPolyMat 𝑟 ) ‘ 𝑚 ) )
31	30 15	cfv	⊢ ( ( 𝑛 maDet ( Poly1 ‘ 𝑟 ) ) ‘ ( ( ( var1 ‘ 𝑟 ) ( ·𝑠 ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( 1r ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ) ( -g ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( ( 𝑛 matToPolyMat 𝑟 ) ‘ 𝑚 ) ) )
32	5 11 31	cmpt	⊢ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( ( 𝑛 maDet ( Poly1 ‘ 𝑟 ) ) ‘ ( ( ( var1 ‘ 𝑟 ) ( ·𝑠 ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( 1r ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ) ( -g ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( ( 𝑛 matToPolyMat 𝑟 ) ‘ 𝑚 ) ) ) )
33	1 3 2 4 32	cmpo	⊢ ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( ( 𝑛 maDet ( Poly1 ‘ 𝑟 ) ) ‘ ( ( ( var1 ‘ 𝑟 ) ( ·𝑠 ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( 1r ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ) ( -g ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( ( 𝑛 matToPolyMat 𝑟 ) ‘ 𝑚 ) ) ) ) )
34	0 33	wceq	⊢ CharPlyMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( ( 𝑛 maDet ( Poly1 ‘ 𝑟 ) ) ‘ ( ( ( var1 ‘ 𝑟 ) ( ·𝑠 ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( 1r ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ) ( -g ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ( ( 𝑛 matToPolyMat 𝑟 ) ‘ 𝑚 ) ) ) ) )