Metamath Proof Explorer

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 = ( 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 ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cchpmat 
 |-  CharPlyMat
1 vn 
 |-  n
2 cfn 
 |-  Fin
3 vr 
 |-  r
4 cvv 
 |-  _V
5 vm 
 |-  m
6 cbs 
 |-  Base
7 1 cv 
 |-  n
8 cmat 
 |-  Mat
9 3 cv 
 |-  r
10 7 9 8 co 
 |-  ( n Mat r )
11 10 6 cfv 
 |-  ( Base ` ( n Mat r ) )
12 cmdat 
 |-  maDet
13 cpl1 
 |-  Poly1
14 9 13 cfv 
 |-  ( Poly1 ` r )
15 7 14 12 co 
 |-  ( n maDet ( Poly1 ` r ) )
16 cv1 
 |-  var1
17 9 16 cfv 
 |-  ( var1 ` r )
18 cvsca 
 |-  .s
19 7 14 8 co 
 |-  ( n Mat ( Poly1 ` r ) )
20 19 18 cfv 
 |-  ( .s ` ( n Mat ( Poly1 ` r ) ) )
21 cur 
 |-  1r
22 19 21 cfv 
 |-  ( 1r ` ( n Mat ( Poly1 ` r ) ) )
23 17 22 20 co 
 |-  ( ( var1 ` r ) ( .s ` ( n Mat ( Poly1 ` r ) ) ) ( 1r ` ( n Mat ( Poly1 ` r ) ) ) )
24 csg 
 |-  -g
25 19 24 cfv 
 |-  ( -g ` ( n Mat ( Poly1 ` r ) ) )
26 cmat2pmat 
 |-  matToPolyMat
27 7 9 26 co 
 |-  ( n matToPolyMat r )
28 5 cv 
 |-  m
29 28 27 cfv 
 |-  ( ( n matToPolyMat r ) ` m )
30 23 29 25 co 
 |-  ( ( ( var1 ` r ) ( .s ` ( n Mat ( Poly1 ` r ) ) ) ( 1r ` ( n Mat ( Poly1 ` r ) ) ) ) ( -g ` ( n Mat ( Poly1 ` r ) ) ) ( ( n matToPolyMat r ) ` m ) )
31 30 15 cfv 
 |-  ( ( 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 ) ) )
32 5 11 31 cmpt 
 |-  ( 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 ) ) ) )
33 1 3 2 4 32 cmpo 
 |-  ( 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 ) ) ) ) )
34 0 33 wceq 
 |-  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 ) ) ) ) )