Definition df-chpmat 20632

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 = ( n e. Fin , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( ( n maDet (Poly1 ` r ) ) ` ( ( (var1 ` r ) ( .s ` ( n Mat (Poly1 ` r ) ) ) ( 1r ` ( n Mat (Poly1 ` r ) ) ) ) ( -g ` ( n Mat (Poly1 ` r ) ) ) ( ( n matToPolyMat r ) ` m ) ) ) ) )

Distinct variable group:   m, n, r

Detailed syntax breakdown of Definition df-chpmat

Step	Hyp	Ref	Expression
1		cchpmat 20631	. 2 class CharPlyMat
2		vn	. . 3 setvar n
3		vr	. . 3 setvar r
4		cfn 7955	. . 3 class Fin
5		cvv 3200	. . 3 class _V
6		vm	. . . 4 setvar m
7	2	cv 1482	. . . . . 6 class n
8	3	cv 1482	. . . . . 6 class r
9		cmat 20213	. . . . . 6 class Mat
10	7, 8, 9	co 6650	. . . . 5 class ( n Mat r )
11		cbs 15857	. . . . 5 class Base
12	10, 11	cfv 5888	. . . 4 class ( Base ` ( n Mat r ) )
13		cv1 19546	. . . . . . . 8 class var1
14	8, 13	cfv 5888	. . . . . . 7 class (var1 ` r )
15		cpl1 19547	. . . . . . . . . 10 class Poly1
16	8, 15	cfv 5888	. . . . . . . . 9 class (Poly1 ` r )
17	7, 16, 9	co 6650	. . . . . . . 8 class ( n Mat (Poly1 ` r ) )
18		cur 18501	. . . . . . . 8 class 1r
19	17, 18	cfv 5888	. . . . . . 7 class ( 1r ` ( n Mat (Poly1 ` r ) ) )
20		cvsca 15945	. . . . . . . 8 class .s
21	17, 20	cfv 5888	. . . . . . 7 class ( .s ` ( n Mat (Poly1 ` r ) ) )
22	14, 19, 21	co 6650	. . . . . 6 class ( (var1 ` r ) ( .s ` ( n Mat (Poly1 ` r ) ) ) ( 1r ` ( n Mat (Poly1 ` r ) ) ) )
23	6	cv 1482	. . . . . . 7 class m
24		cmat2pmat 20509	. . . . . . . 8 class matToPolyMat
25	7, 8, 24	co 6650	. . . . . . 7 class ( n matToPolyMat r )
26	23, 25	cfv 5888	. . . . . 6 class ( ( n matToPolyMat r ) ` m )
27		csg 17424	. . . . . . 7 class -g
28	17, 27	cfv 5888	. . . . . 6 class ( -g ` ( n Mat (Poly1 ` r ) ) )
29	22, 26, 28	co 6650	. . . . 5 class ( ( (var1 ` r ) ( .s ` ( n Mat (Poly1 ` r ) ) ) ( 1r ` ( n Mat (Poly1 ` r ) ) ) ) ( -g ` ( n Mat (Poly1 ` r ) ) ) ( ( n matToPolyMat r ) ` m ) )
30		cmdat 20390	. . . . . 6 class maDet
31	7, 16, 30	co 6650	. . . . 5 class ( n maDet (Poly1 ` r ) )
32	29, 31	cfv 5888	. . . 4 class ( ( n maDet (Poly1 ` r ) ) ` ( ( (var1 ` r ) ( .s ` ( n Mat (Poly1 ` r ) ) ) ( 1r ` ( n Mat (Poly1 ` r ) ) ) ) ( -g ` ( n Mat (Poly1 ` r ) ) ) ( ( n matToPolyMat r ) ` m ) ) )
33	6, 12, 32	cmpt 4729	. . 3 class ( m e. ( Base ` ( n Mat r ) ) |-> ( ( n maDet (Poly1 ` r ) ) ` ( ( (var1 ` r ) ( .s ` ( n Mat (Poly1 ` r ) ) ) ( 1r ` ( n Mat (Poly1 ` r ) ) ) ) ( -g ` ( n Mat (Poly1 ` r ) ) ) ( ( n matToPolyMat r ) ` m ) ) ) )
34	2, 3, 4, 5, 33	cmpt2 6652	. 2 class ( n e. Fin , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( ( n maDet (Poly1 ` r ) ) ` ( ( (var1 ` r ) ( .s ` ( n Mat (Poly1 ` r ) ) ) ( 1r ` ( n Mat (Poly1 ` r ) ) ) ) ( -g ` ( n Mat (Poly1 ` r ) ) ) ( ( n matToPolyMat r ) ` m ) ) ) ) )
35	1, 34	wceq 1483	1 wff CharPlyMat = ( n e. Fin , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( ( n maDet (Poly1 ` r ) ) ` ( ( (var1 ` r ) ( .s ` ( n Mat (Poly1 ` r ) ) ) ( 1r ` ( n Mat (Poly1 ` r ) ) ) ) ( -g ` ( n Mat (Poly1 ` r ) ) ) ( ( n matToPolyMat r ) ` m ) ) ) ) )

This definition is referenced by:  chpmatfval  20635