Theorem cpmidgsum

Description: Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as group sum. (Contributed by AV, 7-Nov-2019)

	Ref	Expression
Hypotheses	cpmidgsum.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	cpmidgsum.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	cpmidgsum.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	cpmidgsum.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
	cpmidgsum.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	cpmidgsum.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	cpmidgsum.m	⊢ · = ( ·𝑠 ‘ 𝑌 )
	cpmidgsum.1	⊢ 1 = ( 1r ‘ 𝑌 )
	cpmidgsum.u	⊢ 𝑈 = ( algSc ‘ 𝑃 )
	cpmidgsum.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
	cpmidgsum.k	⊢ 𝐾 = ( 𝐶 ‘ 𝑀 )
	cpmidgsum.h	⊢ 𝐻 = ( 𝐾 · 1 )
Assertion	cpmidgsum	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐻 = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( ( 𝑈 ‘ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ) · 1 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cpmidgsum.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		cpmidgsum.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		cpmidgsum.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4		cpmidgsum.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
5		cpmidgsum.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
6		cpmidgsum.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
7		cpmidgsum.m	⊢ · = ( ·𝑠 ‘ 𝑌 )
8		cpmidgsum.1	⊢ 1 = ( 1r ‘ 𝑌 )
9		cpmidgsum.u	⊢ 𝑈 = ( algSc ‘ 𝑃 )
10		cpmidgsum.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
11		cpmidgsum.k	⊢ 𝐾 = ( 𝐶 ‘ 𝑀 )
12		cpmidgsum.h	⊢ 𝐻 = ( 𝐾 · 1 )
13		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
14	10 1 2 3 13	chpmatply1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 ‘ 𝑀 ) ∈ ( Base ‘ 𝑃 ) )
15	11 14	eqeltrid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐾 ∈ ( Base ‘ 𝑃 ) )
16		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
17		eqid	⊢ ( 𝑁 matToPolyMat 𝑅 ) = ( 𝑁 matToPolyMat 𝑅 )
18		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
19	3 4 16 7 6 5 17 1 2 9 18 13 9 8 12	pmatcollpwscmat	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐾 ∈ ( Base ‘ 𝑃 ) ) → 𝐻 = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( ( 𝑈 ‘ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ) · 1 ) ) ) ) )
20	15 19	syld3an3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐻 = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( ( 𝑈 ‘ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ) · 1 ) ) ) ) )