Theorem chpmatval2

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

	Ref	Expression
Hypotheses	chpmatply1.c	$$⊢C=N\mathrm{CharPlyMat}R$$
	chpmatply1.a	$$⊢A=N\mathrm{Mat}R$$
	chpmatply1.b	$$⊢B={\mathrm{Base}}_A$$
	chpmatply1.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	chpmatval2.y	$$⊢Y=N\mathrm{Mat}P$$
	chpmatval2.m1	$$⊢\underset{\dot{}}{-}={-}_Y$$
	chpmatval2.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	chpmatval2.t1	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
	chpmatval2.t	$$⊢T=N\mathrm{matToPolyMat}R$$
	chpmatval2.i	$$⊢\underset{\dot{}}{1}=1_Y$$
	chpmatval2.g	$$⊢G=\mathrm{SymGrp}\left(N\right)$$
	chpmatval2.h	$$⊢H={\mathrm{Base}}_G$$
	chpmatval2.z	$$⊢Z=\mathrm{\mathbb{Z}RHom}\left(P\right)$$
	chpmatval2.s	$$⊢S=\mathrm{pmSgn}\left(N\right)$$
	chpmatval2.u	$$⊢U={\mathrm{mulGrp}}_P$$
	chpmatval2.rm	$$⊢\underset{\dot{}}{\times }={\cdot }_P$$
Assertion	chpmatval2	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge M\in B\right)\to C\left(M\right)=\underset{p\in H}{{\sum }_P}\left(\left(Z\circ S\right)\left(p\right)\underset{\dot{}}{\times }\left(\underset{x\in N}{{\sum }_U},\left(p\left(x\right)\left(\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(M\right)\right)x\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		chpmatply1.c	$$⊢C=N\mathrm{CharPlyMat}R$$
2		chpmatply1.a	$$⊢A=N\mathrm{Mat}R$$
3		chpmatply1.b	$$⊢B={\mathrm{Base}}_A$$
4		chpmatply1.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
5		chpmatval2.y	$$⊢Y=N\mathrm{Mat}P$$
6		chpmatval2.m1	$$⊢\underset{\dot{}}{-}={-}_Y$$
7		chpmatval2.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
8		chpmatval2.t1	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
9		chpmatval2.t	$$⊢T=N\mathrm{matToPolyMat}R$$
10		chpmatval2.i	$$⊢\underset{\dot{}}{1}=1_Y$$
11		chpmatval2.g	$$⊢G=\mathrm{SymGrp}\left(N\right)$$
12		chpmatval2.h	$$⊢H={\mathrm{Base}}_G$$
13		chpmatval2.z	$$⊢Z=\mathrm{\mathbb{Z}RHom}\left(P\right)$$
14		chpmatval2.s	$$⊢S=\mathrm{pmSgn}\left(N\right)$$
15		chpmatval2.u	$$⊢U={\mathrm{mulGrp}}_P$$
16		chpmatval2.rm	$$⊢\underset{\dot{}}{\times }={\cdot }_P$$
17		eqid	$$⊢N\mathrm{maDet}P=N\mathrm{maDet}P$$
18	1 2 3 4 5 17 6 7 8 9 10	chpmatval	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge M\in B\right)\to C\left(M\right)=\left(N\mathrm{maDet}P\right)\left(\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(M\right)\right)$$
19		eqid	$$⊢N\mathrm{Mat}P=N\mathrm{Mat}P$$
20	5	fveq2i	$$⊢{-}_Y={-}_{\left(N\mathrm{Mat}P\right)}$$
21	6 20	eqtri	$$⊢\underset{\dot{}}{-}={-}_{\left(N\mathrm{Mat}P\right)}$$
22	5	fveq2i	$$⊢{\cdot }_Y={\cdot }_{\left(N\mathrm{Mat}P\right)}$$
23	8 22	eqtri	$$⊢\underset{\dot{}}{·}={\cdot }_{\left(N\mathrm{Mat}P\right)}$$
24	5	fveq2i	$$⊢1_Y=1_{\left(N\mathrm{Mat}P\right)}$$
25	10 24	eqtri	$$⊢\underset{\dot{}}{1}=1_{\left(N\mathrm{Mat}P\right)}$$
26		eqid	$$⊢\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)$$
27	2 3 4 19 7 9 21 23 25 26	chmatcl	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge M\in B\right)\to \left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(M\right)\in {\mathrm{Base}}_{\left(N\mathrm{Mat}P\right)}$$
28	5	eqcomi	$$⊢N\mathrm{Mat}P=Y$$
29	28	fveq2i	$$⊢{\mathrm{Base}}_{\left(N\mathrm{Mat}P\right)}={\mathrm{Base}}_Y$$
30	11	fveq2i	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}$$
31	12 30	eqtri	$$⊢H={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}$$
32	17 5 29 31 13 14 16 15	mdetleib	$$⊢\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(M\right)\in {\mathrm{Base}}_{\left(N\mathrm{Mat}P\right)}\to \left(N\mathrm{maDet}P\right)\left(\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(M\right)\right)=\underset{p\in H}{{\sum }_P}\left(\left(Z\circ S\right)\left(p\right)\underset{\dot{}}{\times }\left(\underset{x\in N}{{\sum }_U},\left(p\left(x\right)\left(\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(M\right)\right)x\right)\right)\right)$$
33	27 32	syl	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge M\in B\right)\to \left(N\mathrm{maDet}P\right)\left(\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(M\right)\right)=\underset{p\in H}{{\sum }_P}\left(\left(Z\circ S\right)\left(p\right)\underset{\dot{}}{\times }\left(\underset{x\in N}{{\sum }_U},\left(p\left(x\right)\left(\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(M\right)\right)x\right)\right)\right)$$
34	18 33	eqtrd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge M\in B\right)\to C\left(M\right)=\underset{p\in H}{{\sum }_P}\left(\left(Z\circ S\right)\left(p\right)\underset{\dot{}}{\times }\left(\underset{x\in N}{{\sum }_U},\left(p\left(x\right)\left(\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(M\right)\right)x\right)\right)\right)$$