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 CharPlyMat R )
	chpmatfval.a	|- A = ( N Mat R )
	chpmatfval.b	|- B = ( Base ` A )
	chpmatfval.p	|- P = ( Poly1 ` R )
	chpmatfval.y	|- Y = ( N Mat P )
	chpmatfval.d	|- D = ( N maDet P )
	chpmatfval.s	|- .- = ( -g ` Y )
	chpmatfval.x	|- X = ( var1 ` R )
	chpmatfval.m	|- .x. = ( .s ` Y )
	chpmatfval.t	|- T = ( N matToPolyMat R )
	chpmatfval.i	|- .1. = ( 1r ` Y )
Assertion	chpmatval	|- ( ( N e. Fin /\ R e. V /\ M e. B ) -> ( C ` M ) = ( D ` ( ( X .x. .1. ) .- ( T ` M ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		chpmatfval.c	|- C = ( N CharPlyMat R )
2		chpmatfval.a	|- A = ( N Mat R )
3		chpmatfval.b	|- B = ( Base ` A )
4		chpmatfval.p	|- P = ( Poly1 ` R )
5		chpmatfval.y	|- Y = ( N Mat P )
6		chpmatfval.d	|- D = ( N maDet P )
7		chpmatfval.s	|- .- = ( -g ` Y )
8		chpmatfval.x	|- X = ( var1 ` R )
9		chpmatfval.m	|- .x. = ( .s ` Y )
10		chpmatfval.t	|- T = ( N matToPolyMat R )
11		chpmatfval.i	|- .1. = ( 1r ` Y )
12	1 2 3 4 5 6 7 8 9 10 11	chpmatfval	|- ( ( N e. Fin /\ R e. V ) -> C = ( m e. B |-> ( D ` ( ( X .x. .1. ) .- ( T ` m ) ) ) ) )
13	12	3adant3	|- ( ( N e. Fin /\ R e. V /\ M e. B ) -> C = ( m e. B |-> ( D ` ( ( X .x. .1. ) .- ( T ` m ) ) ) ) )
14		fveq2	|- ( m = M -> ( T ` m ) = ( T ` M ) )
15	14	oveq2d	|- ( m = M -> ( ( X .x. .1. ) .- ( T ` m ) ) = ( ( X .x. .1. ) .- ( T ` M ) ) )
16	15	fveq2d	|- ( m = M -> ( D ` ( ( X .x. .1. ) .- ( T ` m ) ) ) = ( D ` ( ( X .x. .1. ) .- ( T ` M ) ) ) )
17	16	adantl	|- ( ( ( N e. Fin /\ R e. V /\ M e. B ) /\ m = M ) -> ( D ` ( ( X .x. .1. ) .- ( T ` m ) ) ) = ( D ` ( ( X .x. .1. ) .- ( T ` M ) ) ) )
18		simp3	|- ( ( N e. Fin /\ R e. V /\ M e. B ) -> M e. B )
19		fvexd	|- ( ( N e. Fin /\ R e. V /\ M e. B ) -> ( D ` ( ( X .x. .1. ) .- ( T ` M ) ) ) e. _V )
20	13 17 18 19	fvmptd	|- ( ( N e. Fin /\ R e. V /\ M e. B ) -> ( C ` M ) = ( D ` ( ( X .x. .1. ) .- ( T ` M ) ) ) )