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 ∈ Fin , r ∈ V ⟼ m ∈ Base n Mat r ⟼ n maDet Poly 1 ⁡ r ⁡ var 1 ⁡ r ⋅ n Mat Poly 1 ⁡ r 1 n Mat Poly 1 ⁡ r - n Mat Poly 1 ⁡ r n matToPolyMat r ⁡ m

Detailed syntax breakdown

Step Hyp Ref Expression
0 cchpmat class CharPlyMat
1 vn setvar n
2 cfn class Fin
3 vr setvar r
4 cvv class V
5 vm setvar m
6 cbs class Base
7 1 cv setvar n
8 cmat class Mat
9 3 cv setvar r
10 7 9 8 co class n Mat r
11 10 6 cfv class Base n Mat r
12 cmdat class maDet
13 cpl1 class Poly 1
14 9 13 cfv class Poly 1 ⁡ r
15 7 14 12 co class n maDet Poly 1 ⁡ r
16 cv1 class var 1
17 9 16 cfv class var 1 ⁡ r
18 cvsca class ⋅ 𝑠
19 7 14 8 co class n Mat Poly 1 ⁡ r
20 19 18 cfv class ⋅ n Mat Poly 1 ⁡ r
21 cur class 1 r
22 19 21 cfv class 1 n Mat Poly 1 ⁡ r
23 17 22 20 co class var 1 ⁡ r ⋅ n Mat Poly 1 ⁡ r 1 n Mat Poly 1 ⁡ r
24 csg class - 𝑔
25 19 24 cfv class - n Mat Poly 1 ⁡ r
26 cmat2pmat class matToPolyMat
27 7 9 26 co class n matToPolyMat r
28 5 cv setvar m
29 28 27 cfv class n matToPolyMat r ⁡ m
30 23 29 25 co class var 1 ⁡ r ⋅ n Mat Poly 1 ⁡ r 1 n Mat Poly 1 ⁡ r - n Mat Poly 1 ⁡ r n matToPolyMat r ⁡ m
31 30 15 cfv class n maDet Poly 1 ⁡ r ⁡ var 1 ⁡ r ⋅ n Mat Poly 1 ⁡ r 1 n Mat Poly 1 ⁡ r - n Mat Poly 1 ⁡ r n matToPolyMat r ⁡ m
32 5 11 31 cmpt class m ∈ Base n Mat r ⟼ n maDet Poly 1 ⁡ r ⁡ var 1 ⁡ r ⋅ n Mat Poly 1 ⁡ r 1 n Mat Poly 1 ⁡ r - n Mat Poly 1 ⁡ r n matToPolyMat r ⁡ m
33 1 3 2 4 32 cmpo class n ∈ Fin , r ∈ V ⟼ m ∈ Base n Mat r ⟼ n maDet Poly 1 ⁡ r ⁡ var 1 ⁡ r ⋅ n Mat Poly 1 ⁡ r 1 n Mat Poly 1 ⁡ r - n Mat Poly 1 ⁡ r n matToPolyMat r ⁡ m
34 0 33 wceq wff CharPlyMat = n ∈ Fin , r ∈ V ⟼ m ∈ Base n Mat r ⟼ n maDet Poly 1 ⁡ r ⁡ var 1 ⁡ r ⋅ n Mat Poly 1 ⁡ r 1 n Mat Poly 1 ⁡ r - n Mat Poly 1 ⁡ r n matToPolyMat r ⁡ m