Theorem cpmidgsumm2pm

Description: Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as group sum with a matrix to polynomial matrix transformation. (Contributed by AV, 13-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 )
	cpmidgsumm2pm.o	⊢ 𝑂 = ( 1r ‘ 𝐴 )
	cpmidgsumm2pm.m	⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
	cpmidgsumm2pm.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
Assertion	cpmidgsumm2pm	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐻 = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) ) ) ) ) )

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		cpmidgsumm2pm.o	⊢ 𝑂 = ( 1r ‘ 𝐴 )
14		cpmidgsumm2pm.m	⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
15		cpmidgsumm2pm.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
16	1 2 3 4 5 6 7 8 9 10 11 12	cpmidgsum	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐻 = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( ( 𝑈 ‘ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ) · 1 ) ) ) ) )
17		3simpa	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) )
18	17	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) )
19		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
20	10 1 2 3 19	chpmatply1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 ‘ 𝑀 ) ∈ ( Base ‘ 𝑃 ) )
21	11 20	eqeltrid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐾 ∈ ( Base ‘ 𝑃 ) )
22		eqid	⊢ ( coe1 ‘ 𝐾 ) = ( coe1 ‘ 𝐾 )
23		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
24	22 19 3 23	coe1fvalcl	⊢ ( ( 𝐾 ∈ ( Base ‘ 𝑃 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∈ ( Base ‘ 𝑅 ) )
25	21 24	sylan	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∈ ( Base ‘ 𝑅 ) )
26		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
27	26	anim2i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
28	1	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
29	2 13	ringidcl	⊢ ( 𝐴 ∈ Ring → 𝑂 ∈ 𝐵 )
30	27 28 29	3syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑂 ∈ 𝐵 )
31	30	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑂 ∈ 𝐵 )
32	31	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑂 ∈ 𝐵 )
33		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
34	15 1 2 3 4 33 23 9 14 7	mat2pmatlin	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑂 ∈ 𝐵 ) ) → ( 𝑇 ‘ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) ) = ( ( 𝑈 ‘ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ) · ( 𝑇 ‘ 𝑂 ) ) )
35	18 25 32 34	syl12anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑇 ‘ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) ) = ( ( 𝑈 ‘ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ) · ( 𝑇 ‘ 𝑂 ) ) )
36	15 1 2 3 4 33	mat2pmatrhm	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( 𝐴 RingHom 𝑌 ) )
37	13 8	rhm1	⊢ ( 𝑇 ∈ ( 𝐴 RingHom 𝑌 ) → ( 𝑇 ‘ 𝑂 ) = 1 )
38	17 36 37	3syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑂 ) = 1 )
39	38	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑇 ‘ 𝑂 ) = 1 )
40	39	oveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑈 ‘ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ) · ( 𝑇 ‘ 𝑂 ) ) = ( ( 𝑈 ‘ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ) · 1 ) )
41	35 40	eqtr2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑈 ‘ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ) · 1 ) = ( 𝑇 ‘ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) ) )
42	41	oveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ↑ 𝑋 ) · ( ( 𝑈 ‘ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ) · 1 ) ) = ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) ) ) )
43	42	mpteq2dva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( ( 𝑈 ‘ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ) · 1 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) ) ) ) )
44	43	oveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( ( 𝑈 ‘ ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ) · 1 ) ) ) ) = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) ) ) ) ) )
45	16 44	eqtrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐻 = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 𝑂 ) ) ) ) ) )