Theorem pmatcollpwscmat

Description: Write a scalar matrix over polynomials (over a commutative ring) as a sum of the product of variable powers and constant scalar matrices with scalar entries. (Contributed by AV, 2-Nov-2019) (Revised by AV, 4-Dec-2019)

	Ref	Expression
Hypotheses	pmatcollpwscmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	pmatcollpwscmat.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	pmatcollpwscmat.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	pmatcollpwscmat.m1	⊢ ∗ = ( ·𝑠 ‘ 𝐶 )
	pmatcollpwscmat.e1	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	pmatcollpwscmat.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	pmatcollpwscmat.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	pmatcollpwscmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	pmatcollpwscmat.d	⊢ 𝐷 = ( Base ‘ 𝐴 )
	pmatcollpwscmat.u	⊢ 𝑈 = ( algSc ‘ 𝑃 )
	pmatcollpwscmat.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	pmatcollpwscmat.e2	⊢ 𝐸 = ( Base ‘ 𝑃 )
	pmatcollpwscmat.s	⊢ 𝑆 = ( algSc ‘ 𝑃 )
	pmatcollpwscmat.1	⊢ 1 = ( 1r ‘ 𝐶 )
	pmatcollpwscmat.m2	⊢ 𝑀 = ( 𝑄 ∗ 1 )
Assertion	pmatcollpwscmat	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑄 ∈ 𝐸 ) → 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝑛 ) ) ∗ 1 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pmatcollpwscmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		pmatcollpwscmat.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		pmatcollpwscmat.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		pmatcollpwscmat.m1	⊢ ∗ = ( ·𝑠 ‘ 𝐶 )
5		pmatcollpwscmat.e1	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
6		pmatcollpwscmat.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
7		pmatcollpwscmat.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
8		pmatcollpwscmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
9		pmatcollpwscmat.d	⊢ 𝐷 = ( Base ‘ 𝐴 )
10		pmatcollpwscmat.u	⊢ 𝑈 = ( algSc ‘ 𝑃 )
11		pmatcollpwscmat.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
12		pmatcollpwscmat.e2	⊢ 𝐸 = ( Base ‘ 𝑃 )
13		pmatcollpwscmat.s	⊢ 𝑆 = ( algSc ‘ 𝑃 )
14		pmatcollpwscmat.1	⊢ 1 = ( 1r ‘ 𝐶 )
15		pmatcollpwscmat.m2	⊢ 𝑀 = ( 𝑄 ∗ 1 )
16		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
17	1 2 3 12 4 14	1pmatscmul	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝐸 ) → ( 𝑄 ∗ 1 ) ∈ 𝐵 )
18	15 17	eqeltrid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝐸 ) → 𝑀 ∈ 𝐵 )
19	16 18	syl3an2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑄 ∈ 𝐸 ) → 𝑀 ∈ 𝐵 )
20	1 2 3 4 5 6 7	pmatcollpw	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) )
21	19 20	syld3an3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑄 ∈ 𝐸 ) → 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) )
22	16	anim2i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
23	22	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑄 ∈ 𝐸 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
24		simp3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑄 ∈ 𝐸 ) → 𝑄 ∈ 𝐸 )
25	24	anim1ci	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑄 ∈ 𝐸 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) )
26	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	pmatcollpwscmatlem2	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) = ( ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝑛 ) ) ∗ 1 ) )
27	23 25 26	syl2an2r	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑄 ∈ 𝐸 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) = ( ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝑛 ) ) ∗ 1 ) )
28	27	oveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑄 ∈ 𝐸 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) = ( ( 𝑛 ↑ 𝑋 ) ∗ ( ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝑛 ) ) ∗ 1 ) ) )
29	28	mpteq2dva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑄 ∈ 𝐸 ) → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝑛 ) ) ∗ 1 ) ) ) )
30	29	oveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑄 ∈ 𝐸 ) → ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝑛 ) ) ∗ 1 ) ) ) ) )
31	21 30	eqtrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑄 ∈ 𝐸 ) → 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝑛 ) ) ∗ 1 ) ) ) ) )