Theorem chpmatval

Description: The characteristic polynomial of a (square) matrix (expressed with a determinant). (Contributed by AV, 2-Aug-2019)

	Ref	Expression
Hypotheses	chpmatfval.c	$$⊢C=N\mathrm{CharPlyMat}R$$
	chpmatfval.a	$$⊢A=N\mathrm{Mat}R$$
	chpmatfval.b	$$⊢B={\mathrm{Base}}_A$$
	chpmatfval.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	chpmatfval.y	$$⊢Y=N\mathrm{Mat}P$$
	chpmatfval.d	$$⊢D=N\mathrm{maDet}P$$
	chpmatfval.s	$$⊢\underset{\dot{}}{-}={-}_Y$$
	chpmatfval.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	chpmatfval.m	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
	chpmatfval.t	$$⊢T=N\mathrm{matToPolyMat}R$$
	chpmatfval.i	$$⊢\underset{\dot{}}{1}=1_Y$$
Assertion	chpmatval	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\wedge M\in B\right)\to C\left(M\right)=D\left(\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(M\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		chpmatfval.c	$$⊢C=N\mathrm{CharPlyMat}R$$
2		chpmatfval.a	$$⊢A=N\mathrm{Mat}R$$
3		chpmatfval.b	$$⊢B={\mathrm{Base}}_A$$
4		chpmatfval.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
5		chpmatfval.y	$$⊢Y=N\mathrm{Mat}P$$
6		chpmatfval.d	$$⊢D=N\mathrm{maDet}P$$
7		chpmatfval.s	$$⊢\underset{\dot{}}{-}={-}_Y$$
8		chpmatfval.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
9		chpmatfval.m	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
10		chpmatfval.t	$$⊢T=N\mathrm{matToPolyMat}R$$
11		chpmatfval.i	$$⊢\underset{\dot{}}{1}=1_Y$$
12	1 2 3 4 5 6 7 8 9 10 11	chpmatfval	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to C=\left(m\in B⟼D\left(\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(m\right)\right)\right)$$
13	12	3adant3	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\wedge M\in B\right)\to C=\left(m\in B⟼D\left(\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(m\right)\right)\right)$$
14		fveq2	$$⊢m=M\to T\left(m\right)=T\left(M\right)$$
15	14	oveq2d	$$⊢m=M\to \left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(m\right)=\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(M\right)$$
16	15	fveq2d	$$⊢m=M\to D\left(\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(m\right)\right)=D\left(\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(M\right)\right)$$
17	16	adantl	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in V\wedge M\in B\right)\wedge m=M\right)\to D\left(\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(m\right)\right)=D\left(\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(M\right)\right)$$
18		simp3	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\wedge M\in B\right)\to M\in B$$
19		fvexd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\wedge M\in B\right)\to D\left(\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(M\right)\right)\in \mathrm{V}$$
20	13 17 18 19	fvmptd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\wedge M\in B\right)\to C\left(M\right)=D\left(\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(M\right)\right)$$