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	$⊢ P = {Poly}_{1} (R)$
	pm2mpval.c	$⊢ C = N Mat P$
	pm2mpval.b	$⊢ B = {Base}_{C}$
	pm2mpval.m	$⊢ \underset{˙}{*} = \cdot_{Q}$
	pm2mpval.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Q}}$
	pm2mpval.x	$⊢ X = {var}_{1} (A)$
	pm2mpval.a	$⊢ A = N Mat R$
	pm2mpval.q	$⊢ Q = {Poly}_{1} (A)$
	pm2mpval.t	$⊢ T = N pMatToMatPoly R$
	pm2mpcl.l	$⊢ L = {Base}_{Q}$
Assertion	pm2mpcl	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in L$

Proof

Step	Hyp	Ref	Expression
1		pm2mpval.p	$⊢ P = {Poly}_{1} (R)$
2		pm2mpval.c	$⊢ C = N Mat P$
3		pm2mpval.b	$⊢ B = {Base}_{C}$
4		pm2mpval.m	$⊢ \underset{˙}{*} = \cdot_{Q}$
5		pm2mpval.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Q}}$
6		pm2mpval.x	$⊢ X = {var}_{1} (A)$
7		pm2mpval.a	$⊢ A = N Mat R$
8		pm2mpval.q	$⊢ Q = {Poly}_{1} (A)$
9		pm2mpval.t	$⊢ T = N pMatToMatPoly R$
10		pm2mpcl.l	$⊢ L = {Base}_{Q}$
11	1 2 3 4 5 6 7 8 9	pm2mpfval	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((M decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
12		eqid	$⊢ 0_{Q} = 0_{Q}$
13	7	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
14	8	ply1ring	$⊢ A \in Ring \to Q \in Ring$
15		ringcmn	$⊢ Q \in Ring \to Q \in CMnd$
16	13 14 15	3syl	$⊢ (N \in Fin \land R \in Ring) \to Q \in CMnd$
17	16	3adant3	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to Q \in CMnd$
18		nn0ex	$⊢ ℕ_{0} \in V$
19	18	a1i	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to ℕ_{0} \in V$
20	13	3adant3	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to A \in Ring$
21	20	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land k \in ℕ_{0}) \to A \in Ring$
22		simpl2	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land k \in ℕ_{0}) \to R \in Ring$
23		simpl3	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land k \in ℕ_{0}) \to M \in B$
24		simpr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
25		eqid	$⊢ {Base}_{A} = {Base}_{A}$
26	1 2 3 7 25	decpmatcl	$⊢ (R \in Ring \land M \in B \land k \in ℕ_{0}) \to M decompPMat k \in {Base}_{A}$
27	22 23 24 26	syl3anc	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land k \in ℕ_{0}) \to M decompPMat k \in {Base}_{A}$
28		eqid	$⊢ {mulGrp}_{Q} = {mulGrp}_{Q}$
29	25 8 6 4 28 5 10	ply1tmcl	$⊢ (A \in Ring \land M decompPMat k \in {Base}_{A} \land k \in ℕ_{0}) \to (M decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X) \in L$
30	21 27 24 29	syl3anc	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land k \in ℕ_{0}) \to (M decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X) \in L$
31	30	fmpttd	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (k \in ℕ_{0} ⟼ (M decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X)) : ℕ_{0} ⟶ L$
32	8	ply1lmod	$⊢ A \in Ring \to Q \in LMod$
33	20 32	syl	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to Q \in LMod$
34		eqidd	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to Scalar (Q) = Scalar (Q)$
35	8 6 28 5 10	ply1moncl	$⊢ (A \in Ring \land k \in ℕ_{0}) \to k \underset{˙}{\times} X \in L$
36	20 35	sylan	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land k \in ℕ_{0}) \to k \underset{˙}{\times} X \in L$
37		eqid	$⊢ 0_{Scalar (Q)} = 0_{Scalar (Q)}$
38		eqid	$⊢ 0_{A} = 0_{A}$
39	1 2 3 7 38	decpmatfsupp	$⊢ (R \in Ring \land M \in B) \to {finSupp}_{0_{A}} ((k \in ℕ_{0} ⟼ M decompPMat k))$
40	39	3adant1	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to {finSupp}_{0_{A}} ((k \in ℕ_{0} ⟼ M decompPMat k))$
41	8	ply1sca	$⊢ A \in Ring \to A = Scalar (Q)$
42	41	eqcomd	$⊢ A \in Ring \to Scalar (Q) = A$
43	20 42	syl	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to Scalar (Q) = A$
44	43	fveq2d	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to 0_{Scalar (Q)} = 0_{A}$
45	40 44	breqtrrd	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to {finSupp}_{0_{Scalar (Q)}} ((k \in ℕ_{0} ⟼ M decompPMat k))$
46	19 33 34 10 27 36 12 37 4 45	mptscmfsupp0	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to {finSupp}_{0_{Q}} ((k \in ℕ_{0} ⟼ (M decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X)))$
47	10 12 17 19 31 46	gsumcl	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \underset{k \in ℕ_{0}}{\sum_{Q}} ((M decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X)) \in L$
48	11 47	eqeltrd	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in L$

Metamath Proof Explorer

Theorem pm2mpcl

Proof