Definition df-chpmat 21976

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.)

Assertion

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

Distinct variable group:   𝑚,𝑛,𝑟

Detailed syntax breakdown of Definition df-chpmat

Step	Hyp	Ref	Expression
1		cchpmat 21975	. 2 class CharPlyMat
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cfn 8733	. . 3 class Fin
5		cvv 3432	. . 3 class V
6		vm	. . . 4 setvar 𝑚
7	2	cv 1538	. . . . . 6 class 𝑛
8	3	cv 1538	. . . . . 6 class 𝑟
9		cmat 21554	. . . . . 6 class Mat
10	7, 8, 9	co 7275	. . . . 5 class (𝑛 Mat 𝑟)
11		cbs 16912	. . . . 5 class Base
12	10, 11	cfv 6433	. . . 4 class (Base‘(𝑛 Mat 𝑟))
13		cv1 21347	. . . . . . . 8 class var1
14	8, 13	cfv 6433	. . . . . . 7 class (var1‘𝑟)
15		cpl1 21348	. . . . . . . . . 10 class Poly1
16	8, 15	cfv 6433	. . . . . . . . 9 class (Poly1‘𝑟)
17	7, 16, 9	co 7275	. . . . . . . 8 class (𝑛 Mat (Poly1‘𝑟))
18		cur 19737	. . . . . . . 8 class 1r
19	17, 18	cfv 6433	. . . . . . 7 class (1r‘(𝑛 Mat (Poly1‘𝑟)))
20		cvsca 16966	. . . . . . . 8 class ·𝑠
21	17, 20	cfv 6433	. . . . . . 7 class ( ·𝑠 ‘(𝑛 Mat (Poly1‘𝑟)))
22	14, 19, 21	co 7275	. . . . . 6 class ((var1‘𝑟)( ·𝑠 ‘(𝑛 Mat (Poly1‘𝑟)))(1r‘(𝑛 Mat (Poly1‘𝑟))))
23	6	cv 1538	. . . . . . 7 class 𝑚
24		cmat2pmat 21853	. . . . . . . 8 class matToPolyMat
25	7, 8, 24	co 7275	. . . . . . 7 class (𝑛 matToPolyMat 𝑟)
26	23, 25	cfv 6433	. . . . . 6 class ((𝑛 matToPolyMat 𝑟)‘𝑚)
27		csg 18579	. . . . . . 7 class -g
28	17, 27	cfv 6433	. . . . . 6 class (-g‘(𝑛 Mat (Poly1‘𝑟)))
29	22, 26, 28	co 7275	. . . . 5 class (((var1‘𝑟)( ·𝑠 ‘(𝑛 Mat (Poly1‘𝑟)))(1r‘(𝑛 Mat (Poly1‘𝑟))))(-g‘(𝑛 Mat (Poly1‘𝑟)))((𝑛 matToPolyMat 𝑟)‘𝑚))
30		cmdat 21733	. . . . . 6 class maDet
31	7, 16, 30	co 7275	. . . . 5 class (𝑛 maDet (Poly1‘𝑟))
32	29, 31	cfv 6433	. . . 4 class ((𝑛 maDet (Poly1‘𝑟))‘(((var1‘𝑟)( ·𝑠 ‘(𝑛 Mat (Poly1‘𝑟)))(1r‘(𝑛 Mat (Poly1‘𝑟))))(-g‘(𝑛 Mat (Poly1‘𝑟)))((𝑛 matToPolyMat 𝑟)‘𝑚)))
33	6, 12, 32	cmpt 5157	. . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ ((𝑛 maDet (Poly1‘𝑟))‘(((var1‘𝑟)( ·𝑠 ‘(𝑛 Mat (Poly1‘𝑟)))(1r‘(𝑛 Mat (Poly1‘𝑟))))(-g‘(𝑛 Mat (Poly1‘𝑟)))((𝑛 matToPolyMat 𝑟)‘𝑚))))
34	2, 3, 4, 5, 33	cmpo 7277	. 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ ((𝑛 maDet (Poly1‘𝑟))‘(((var1‘𝑟)( ·𝑠 ‘(𝑛 Mat (Poly1‘𝑟)))(1r‘(𝑛 Mat (Poly1‘𝑟))))(-g‘(𝑛 Mat (Poly1‘𝑟)))((𝑛 matToPolyMat 𝑟)‘𝑚)))))
35	1, 34	wceq 1539	1 wff CharPlyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ ((𝑛 maDet (Poly1‘𝑟))‘(((var1‘𝑟)( ·𝑠 ‘(𝑛 Mat (Poly1‘𝑟)))(1r‘(𝑛 Mat (Poly1‘𝑟))))(-g‘(𝑛 Mat (Poly1‘𝑟)))((𝑛 matToPolyMat 𝑟)‘𝑚)))))

This definition is referenced by:  chpmatfval  21979