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 20398
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 20397 . 2 class CharPlyMat
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cfn 7818 . . 3 class Fin
5 cvv 3172 . . 3 class V
6 vm . . . 4 setvar 𝑚
72cv 1473 . . . . . 6 class 𝑛
83cv 1473 . . . . . 6 class 𝑟
9 cmat 19979 . . . . . 6 class Mat
107, 8, 9co 6526 . . . . 5 class (𝑛 Mat 𝑟)
11 cbs 15643 . . . . 5 class Base
1210, 11cfv 5789 . . . 4 class (Base‘(𝑛 Mat 𝑟))
13 cv1 19315 . . . . . . . 8 class var1
148, 13cfv 5789 . . . . . . 7 class (var1𝑟)
15 cpl1 19316 . . . . . . . . . 10 class Poly1
168, 15cfv 5789 . . . . . . . . 9 class (Poly1𝑟)
177, 16, 9co 6526 . . . . . . . 8 class (𝑛 Mat (Poly1𝑟))
18 cur 18272 . . . . . . . 8 class 1r
1917, 18cfv 5789 . . . . . . 7 class (1r‘(𝑛 Mat (Poly1𝑟)))
20 cvsca 15720 . . . . . . . 8 class ·𝑠
2117, 20cfv 5789 . . . . . . 7 class ( ·𝑠 ‘(𝑛 Mat (Poly1𝑟)))
2214, 19, 21co 6526 . . . . . 6 class ((var1𝑟)( ·𝑠 ‘(𝑛 Mat (Poly1𝑟)))(1r‘(𝑛 Mat (Poly1𝑟))))
236cv 1473 . . . . . . 7 class 𝑚
24 cmat2pmat 20275 . . . . . . . 8 class matToPolyMat
257, 8, 24co 6526 . . . . . . 7 class (𝑛 matToPolyMat 𝑟)
2623, 25cfv 5789 . . . . . 6 class ((𝑛 matToPolyMat 𝑟)‘𝑚)
27 csg 17195 . . . . . . 7 class -g
2817, 27cfv 5789 . . . . . 6 class (-g‘(𝑛 Mat (Poly1𝑟)))
2922, 26, 28co 6526 . . . . 5 class (((var1𝑟)( ·𝑠 ‘(𝑛 Mat (Poly1𝑟)))(1r‘(𝑛 Mat (Poly1𝑟))))(-g‘(𝑛 Mat (Poly1𝑟)))((𝑛 matToPolyMat 𝑟)‘𝑚))
30 cmdat 20156 . . . . . 6 class maDet
317, 16, 30co 6526 . . . . 5 class (𝑛 maDet (Poly1𝑟))
3229, 31cfv 5789 . . . 4 class ((𝑛 maDet (Poly1𝑟))‘(((var1𝑟)( ·𝑠 ‘(𝑛 Mat (Poly1𝑟)))(1r‘(𝑛 Mat (Poly1𝑟))))(-g‘(𝑛 Mat (Poly1𝑟)))((𝑛 matToPolyMat 𝑟)‘𝑚)))
336, 12, 32cmpt 4637 . . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ ((𝑛 maDet (Poly1𝑟))‘(((var1𝑟)( ·𝑠 ‘(𝑛 Mat (Poly1𝑟)))(1r‘(𝑛 Mat (Poly1𝑟))))(-g‘(𝑛 Mat (Poly1𝑟)))((𝑛 matToPolyMat 𝑟)‘𝑚))))
342, 3, 4, 5, 33cmpt2 6528 . 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ ((𝑛 maDet (Poly1𝑟))‘(((var1𝑟)( ·𝑠 ‘(𝑛 Mat (Poly1𝑟)))(1r‘(𝑛 Mat (Poly1𝑟))))(-g‘(𝑛 Mat (Poly1𝑟)))((𝑛 matToPolyMat 𝑟)‘𝑚)))))
351, 34wceq 1474 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  20401
  Copyright terms: Public domain W3C validator