Theorem pm2mpcl

Description: The transformation of polynomial matrices into polynomials over matrices maps polynomial matrices to polynomials over matrices. (Contributed by AV, 5-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 𝑅 )
	pm2mpcl.l	⊢ 𝐿 = ( Base ‘ 𝑄 )
Assertion	pm2mpcl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ 𝐿 )

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		pm2mpcl.l	⊢ 𝐿 = ( Base ‘ 𝑄 )
11	1 2 3 4 5 6 7 8 9	pm2mpfval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑀 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
12		eqid	⊢ ( 0g ‘ 𝑄 ) = ( 0g ‘ 𝑄 )
13	7	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
14	8	ply1ring	⊢ ( 𝐴 ∈ Ring → 𝑄 ∈ Ring )
15		ringcmn	⊢ ( 𝑄 ∈ Ring → 𝑄 ∈ CMnd )
16	13 14 15	3syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ CMnd )
17	16	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑄 ∈ CMnd )
18		nn0ex	⊢ ℕ0 ∈ V
19	18	a1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ℕ0 ∈ V )
20	13	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝐴 ∈ Ring )
21	20	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ Ring )
22		simpl2	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑅 ∈ Ring )
23		simpl3	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ∈ 𝐵 )
24		simpr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
25		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
26	1 2 3 7 25	decpmatcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
27	22 23 24 26	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
28		eqid	⊢ ( mulGrp ‘ 𝑄 ) = ( mulGrp ‘ 𝑄 )
29	25 8 6 4 28 5 10	ply1tmcl	⊢ ( ( 𝐴 ∈ Ring ∧ ( 𝑀 decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑀 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐿 )
30	21 27 24 29	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑀 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐿 )
31	30	fmpttd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑀 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) : ℕ0 ⟶ 𝐿 )
32	8	ply1lmod	⊢ ( 𝐴 ∈ Ring → 𝑄 ∈ LMod )
33	20 32	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑄 ∈ LMod )
34		eqidd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( Scalar ‘ 𝑄 ) = ( Scalar ‘ 𝑄 ) )
35	8 6 28 5 10	ply1moncl	⊢ ( ( 𝐴 ∈ Ring ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐿 )
36	20 35	sylan	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐿 )
37		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑄 ) ) = ( 0g ‘ ( Scalar ‘ 𝑄 ) )
38		eqid	⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
39	1 2 3 7 38	decpmatfsupp	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝑀 decompPMat 𝑘 ) ) finSupp ( 0g ‘ 𝐴 ) )
40	39	3adant1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝑀 decompPMat 𝑘 ) ) finSupp ( 0g ‘ 𝐴 ) )
41	8	ply1sca	⊢ ( 𝐴 ∈ Ring → 𝐴 = ( Scalar ‘ 𝑄 ) )
42	41	eqcomd	⊢ ( 𝐴 ∈ Ring → ( Scalar ‘ 𝑄 ) = 𝐴 )
43	20 42	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( Scalar ‘ 𝑄 ) = 𝐴 )
44	43	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 0g ‘ ( Scalar ‘ 𝑄 ) ) = ( 0g ‘ 𝐴 ) )
45	40 44	breqtrrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝑀 decompPMat 𝑘 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑄 ) ) )
46	19 33 34 10 27 36 12 37 4 45	mptscmfsupp0	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑀 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑄 ) )
47	10 12 17 19 31 46	gsumcl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑀 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ∈ 𝐿 )
48	11 47	eqeltrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ 𝐿 )