MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-chpmat Structured version   Visualization version   GIF version

Definition df-chpmat 20849
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 pA(t), is the polynomial defined by pA ( 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 PM(t) to be the determinant det ( t In - M ) where In 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
StepHypRef Expression
1 cchpmat 20848 . 2 class CharPlyMat
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cfn 8195 . . 3 class Fin
5 cvv 3398 . . 3 class V
6 vm . . . 4 setvar 𝑚
72cv 1636 . . . . . 6 class 𝑛
83cv 1636 . . . . . 6 class 𝑟
9 cmat 20427 . . . . . 6 class Mat
107, 8, 9co 6877 . . . . 5 class (𝑛 Mat 𝑟)
11 cbs 16071 . . . . 5 class Base
1210, 11cfv 6104 . . . 4 class (Base‘(𝑛 Mat 𝑟))
13 cv1 19757 . . . . . . . 8 class var1
148, 13cfv 6104 . . . . . . 7 class (var1𝑟)
15 cpl1 19758 . . . . . . . . . 10 class Poly1
168, 15cfv 6104 . . . . . . . . 9 class (Poly1𝑟)
177, 16, 9co 6877 . . . . . . . 8 class (𝑛 Mat (Poly1𝑟))
18 cur 18706 . . . . . . . 8 class 1r
1917, 18cfv 6104 . . . . . . 7 class (1r‘(𝑛 Mat (Poly1𝑟)))
20 cvsca 16160 . . . . . . . 8 class ·𝑠
2117, 20cfv 6104 . . . . . . 7 class ( ·𝑠 ‘(𝑛 Mat (Poly1𝑟)))
2214, 19, 21co 6877 . . . . . 6 class ((var1𝑟)( ·𝑠 ‘(𝑛 Mat (Poly1𝑟)))(1r‘(𝑛 Mat (Poly1𝑟))))
236cv 1636 . . . . . . 7 class 𝑚
24 cmat2pmat 20726 . . . . . . . 8 class matToPolyMat
257, 8, 24co 6877 . . . . . . 7 class (𝑛 matToPolyMat 𝑟)
2623, 25cfv 6104 . . . . . 6 class ((𝑛 matToPolyMat 𝑟)‘𝑚)
27 csg 17632 . . . . . . 7 class -g
2817, 27cfv 6104 . . . . . 6 class (-g‘(𝑛 Mat (Poly1𝑟)))
2922, 26, 28co 6877 . . . . 5 class (((var1𝑟)( ·𝑠 ‘(𝑛 Mat (Poly1𝑟)))(1r‘(𝑛 Mat (Poly1𝑟))))(-g‘(𝑛 Mat (Poly1𝑟)))((𝑛 matToPolyMat 𝑟)‘𝑚))
30 cmdat 20605 . . . . . 6 class maDet
317, 16, 30co 6877 . . . . 5 class (𝑛 maDet (Poly1𝑟))
3229, 31cfv 6104 . . . 4 class ((𝑛 maDet (Poly1𝑟))‘(((var1𝑟)( ·𝑠 ‘(𝑛 Mat (Poly1𝑟)))(1r‘(𝑛 Mat (Poly1𝑟))))(-g‘(𝑛 Mat (Poly1𝑟)))((𝑛 matToPolyMat 𝑟)‘𝑚)))
336, 12, 32cmpt 4930 . . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ ((𝑛 maDet (Poly1𝑟))‘(((var1𝑟)( ·𝑠 ‘(𝑛 Mat (Poly1𝑟)))(1r‘(𝑛 Mat (Poly1𝑟))))(-g‘(𝑛 Mat (Poly1𝑟)))((𝑛 matToPolyMat 𝑟)‘𝑚))))
342, 3, 4, 5, 33cmpt2 6879 . 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ ((𝑛 maDet (Poly1𝑟))‘(((var1𝑟)( ·𝑠 ‘(𝑛 Mat (Poly1𝑟)))(1r‘(𝑛 Mat (Poly1𝑟))))(-g‘(𝑛 Mat (Poly1𝑟)))((𝑛 matToPolyMat 𝑟)‘𝑚)))))
351, 34wceq 1637 1 wff CharPlyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ ((𝑛 maDet (Poly1𝑟))‘(((var1𝑟)( ·𝑠 ‘(𝑛 Mat (Poly1𝑟)))(1r‘(𝑛 Mat (Poly1𝑟))))(-g‘(𝑛 Mat (Poly1𝑟)))((𝑛 matToPolyMat 𝑟)‘𝑚)))))
Colors of variables: wff setvar class
This definition is referenced by:  chpmatfval  20852
  Copyright terms: Public domain W3C validator