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 \in Fin, r \in V ⟼ (m \in {Base}_{(n Mat r)} ⟼ (n maDet {Poly}_{1} (r)) (({var}_{1} (r) \cdot_{(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 \cdot_{𝑠}$
19	7 14 8	co	$class (n Mat {Poly}_{1} (r))$
20	19 18	cfv	$class \cdot_{(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) \cdot_{(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) \cdot_{(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) \cdot_{(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 \in {Base}_{(n Mat r)} ⟼ (n maDet {Poly}_{1} (r)) (({var}_{1} (r) \cdot_{(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 \in Fin, r \in V ⟼ (m \in {Base}_{(n Mat r)} ⟼ (n maDet {Poly}_{1} (r)) (({var}_{1} (r) \cdot_{(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 \in Fin, r \in V ⟼ (m \in {Base}_{(n Mat r)} ⟼ (n maDet {Poly}_{1} (r)) (({var}_{1} (r) \cdot_{(n Mat {Poly}_{1} (r))} 1_{(n Mat {Poly}_{1} (r))}) -_{(n Mat {Poly}_{1} (r))} (n matToPolyMat r) (m))))$

Metamath Proof Explorer

Definition df-chpmat

Detailed syntax breakdown