Theorem pm2mpcoe1

Description: A coefficient of the polynomial over matrices which is the result of the transformation of a polynomial matrix is the matrix consisting of the coefficients in the polynomial entries of the polynomial matrix. (Contributed by AV, 20-Oct-2019) (Revised by AV, 5-Dec-2019)

	Ref	Expression
Hypotheses	pm2mpval.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	pm2mpval.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	pm2mpval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	pm2mpval.m	⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
	pm2mpval.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
	pm2mpval.x	⊢ 𝑋 = ( var1 ‘ 𝐴 )
	pm2mpval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	pm2mpval.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
	pm2mpval.t	⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
Assertion	pm2mpcoe1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → ( ( coe1 ‘ ( 𝑇 ‘ 𝑀 ) ) ‘ 𝐾 ) = ( 𝑀 decompPMat 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		pm2mpval.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		pm2mpval.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		pm2mpval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		pm2mpval.m	⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
5		pm2mpval.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
6		pm2mpval.x	⊢ 𝑋 = ( var1 ‘ 𝐴 )
7		pm2mpval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
8		pm2mpval.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
9		pm2mpval.t	⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
10		simpll	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → 𝑁 ∈ Fin )
11		simplr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → 𝑅 ∈ Ring )
12		simprl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → 𝑀 ∈ 𝐵 )
13	1 2 3 4 5 6 7 8 9	pm2mpfval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑀 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
14	10 11 12 13	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → ( 𝑇 ‘ 𝑀 ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑀 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
15	14	fveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → ( coe1 ‘ ( 𝑇 ‘ 𝑀 ) ) = ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑀 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
16	15	fveq1d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → ( ( coe1 ‘ ( 𝑇 ‘ 𝑀 ) ) ‘ 𝐾 ) = ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑀 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐾 ) )
17		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
18	7	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
19	18	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → 𝐴 ∈ Ring )
20		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
21		eqid	⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
22	11	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑅 ∈ Ring )
23	12	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ∈ 𝐵 )
24		simpr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
25	1 2 3 7 20	decpmatcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
26	22 23 24 25	syl3anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
27	26	ralrimiva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → ∀ 𝑘 ∈ ℕ0 ( 𝑀 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
28	1 2 3 7 21	decpmatfsupp	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝑀 decompPMat 𝑘 ) ) finSupp ( 0g ‘ 𝐴 ) )
29	28	ad2ant2lr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝑀 decompPMat 𝑘 ) ) finSupp ( 0g ‘ 𝐴 ) )
30		simpr	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ℕ0 )
31	30	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → 𝐾 ∈ ℕ0 )
32	8 17 6 5 19 20 4 21 27 29 31	gsummoncoe1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑀 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐾 ) = ⦋ 𝐾 / 𝑘 ⦌ ( 𝑀 decompPMat 𝑘 ) )
33		csbov2g	⊢ ( 𝐾 ∈ ℕ0 → ⦋ 𝐾 / 𝑘 ⦌ ( 𝑀 decompPMat 𝑘 ) = ( 𝑀 decompPMat ⦋ 𝐾 / 𝑘 ⦌ 𝑘 ) )
34		csbvarg	⊢ ( 𝐾 ∈ ℕ0 → ⦋ 𝐾 / 𝑘 ⦌ 𝑘 = 𝐾 )
35	34	oveq2d	⊢ ( 𝐾 ∈ ℕ0 → ( 𝑀 decompPMat ⦋ 𝐾 / 𝑘 ⦌ 𝑘 ) = ( 𝑀 decompPMat 𝐾 ) )
36	33 35	eqtrd	⊢ ( 𝐾 ∈ ℕ0 → ⦋ 𝐾 / 𝑘 ⦌ ( 𝑀 decompPMat 𝑘 ) = ( 𝑀 decompPMat 𝐾 ) )
37	36	adantl	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) → ⦋ 𝐾 / 𝑘 ⦌ ( 𝑀 decompPMat 𝑘 ) = ( 𝑀 decompPMat 𝐾 ) )
38	37	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → ⦋ 𝐾 / 𝑘 ⦌ ( 𝑀 decompPMat 𝑘 ) = ( 𝑀 decompPMat 𝐾 ) )
39	16 32 38	3eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ) → ( ( coe1 ‘ ( 𝑇 ‘ 𝑀 ) ) ‘ 𝐾 ) = ( 𝑀 decompPMat 𝐾 ) )