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	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
	chpmatply1.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	chpmatply1.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	chpmatply1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	chpmatval2.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
	chpmatval2.m1	⊢ − = ( -g ‘ 𝑌 )
	chpmatval2.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	chpmatval2.t1	⊢ · = ( ·𝑠 ‘ 𝑌 )
	chpmatval2.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	chpmatval2.i	⊢ 1 = ( 1r ‘ 𝑌 )
	chpmatval2.g	⊢ 𝐺 = ( SymGrp ‘ 𝑁 )
	chpmatval2.h	⊢ 𝐻 = ( Base ‘ 𝐺 )
	chpmatval2.z	⊢ 𝑍 = ( ℤRHom ‘ 𝑃 )
	chpmatval2.s	⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
	chpmatval2.u	⊢ 𝑈 = ( mulGrp ‘ 𝑃 )
	chpmatval2.rm	⊢ × = ( .r ‘ 𝑃 )
Assertion	chpmatval2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 ‘ 𝑀 ) = ( 𝑃 Σg ( 𝑝 ∈ 𝐻 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) × ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) 𝑥 ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		chpmatply1.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
2		chpmatply1.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3		chpmatply1.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
4		chpmatply1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
5		chpmatval2.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
6		chpmatval2.m1	⊢ − = ( -g ‘ 𝑌 )
7		chpmatval2.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
8		chpmatval2.t1	⊢ · = ( ·𝑠 ‘ 𝑌 )
9		chpmatval2.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
10		chpmatval2.i	⊢ 1 = ( 1r ‘ 𝑌 )
11		chpmatval2.g	⊢ 𝐺 = ( SymGrp ‘ 𝑁 )
12		chpmatval2.h	⊢ 𝐻 = ( Base ‘ 𝐺 )
13		chpmatval2.z	⊢ 𝑍 = ( ℤRHom ‘ 𝑃 )
14		chpmatval2.s	⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
15		chpmatval2.u	⊢ 𝑈 = ( mulGrp ‘ 𝑃 )
16		chpmatval2.rm	⊢ × = ( .r ‘ 𝑃 )
17		eqid	⊢ ( 𝑁 maDet 𝑃 ) = ( 𝑁 maDet 𝑃 )
18	1 2 3 4 5 17 6 7 8 9 10	chpmatval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 ‘ 𝑀 ) = ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) )
19		eqid	⊢ ( 𝑁 Mat 𝑃 ) = ( 𝑁 Mat 𝑃 )
20	5	fveq2i	⊢ ( -g ‘ 𝑌 ) = ( -g ‘ ( 𝑁 Mat 𝑃 ) )
21	6 20	eqtri	⊢ − = ( -g ‘ ( 𝑁 Mat 𝑃 ) )
22	5	fveq2i	⊢ ( ·𝑠 ‘ 𝑌 ) = ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) )
23	8 22	eqtri	⊢ · = ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) )
24	5	fveq2i	⊢ ( 1r ‘ 𝑌 ) = ( 1r ‘ ( 𝑁 Mat 𝑃 ) )
25	10 24	eqtri	⊢ 1 = ( 1r ‘ ( 𝑁 Mat 𝑃 ) )
26		eqid	⊢ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) )
27	2 3 4 19 7 9 21 23 25 26	chmatcl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) )
28	5	eqcomi	⊢ ( 𝑁 Mat 𝑃 ) = 𝑌
29	28	fveq2i	⊢ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) = ( Base ‘ 𝑌 )
30	11	fveq2i	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
31	12 30	eqtri	⊢ 𝐻 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
32	17 5 29 31 13 14 16 15	mdetleib	⊢ ( ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) → ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) = ( 𝑃 Σg ( 𝑝 ∈ 𝐻 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) × ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) 𝑥 ) ) ) ) ) ) )
33	27 32	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) = ( 𝑃 Σg ( 𝑝 ∈ 𝐻 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) × ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) 𝑥 ) ) ) ) ) ) )
34	18 33	eqtrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 ‘ 𝑀 ) = ( 𝑃 Σg ( 𝑝 ∈ 𝐻 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) × ( 𝑈 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) 𝑥 ) ) ) ) ) ) )