pm2mp

Description: The transformation of a sum of matrices having scaled monomials with the same power as entries into a sum of scaled monomials as a polynomial over matrices. (Contributed by AV, 12-Nov-2019) (Revised by AV, 7-Dec-2019)

	Ref	Expression
Hypotheses	monmat2matmon.p	$⊢ P = {Poly}_{1} (R)$
	monmat2matmon.c	$⊢ C = N Mat P$
	monmat2matmon.b	$⊢ B = {Base}_{C}$
	monmat2matmon.m1	$⊢ \underset{˙}{*} = \cdot_{Q}$
	monmat2matmon.e1	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Q}}$
	monmat2matmon.x	$⊢ X = {var}_{1} (A)$
	monmat2matmon.a	$⊢ A = N Mat R$
	monmat2matmon.k	$⊢ K = {Base}_{A}$
	monmat2matmon.q	$⊢ Q = {Poly}_{1} (A)$
	monmat2matmon.i	$⊢ I = N pMatToMatPoly R$
	monmat2matmon.e2	$⊢ E = \cdot_{{mulGrp}_{P}}$
	monmat2matmon.y	$⊢ Y = {var}_{1} (R)$
	monmat2matmon.m2	$⊢ \underset{˙}{\cdot} = \cdot_{C}$
	monmat2matmon.t	$⊢ T = N matToPolyMat R$
Assertion	pm2mp	$⊢ ((N \in Fin \land R \in CRing) \land (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M))) \to I (\underset{n \in ℕ_{0}}{\sum_{C}} ((n E Y) \underset{˙}{\cdot} T (M (n)))) = \underset{n \in ℕ_{0}}{\sum_{Q}} (M (n) \underset{˙}{*} (n \underset{˙}{\times} X))$

Proof

Step	Hyp	Ref	Expression
1		monmat2matmon.p	$⊢ P = {Poly}_{1} (R)$
2		monmat2matmon.c	$⊢ C = N Mat P$
3		monmat2matmon.b	$⊢ B = {Base}_{C}$
4		monmat2matmon.m1	$⊢ \underset{˙}{*} = \cdot_{Q}$
5		monmat2matmon.e1	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Q}}$
6		monmat2matmon.x	$⊢ X = {var}_{1} (A)$
7		monmat2matmon.a	$⊢ A = N Mat R$
8		monmat2matmon.k	$⊢ K = {Base}_{A}$
9		monmat2matmon.q	$⊢ Q = {Poly}_{1} (A)$
10		monmat2matmon.i	$⊢ I = N pMatToMatPoly R$
11		monmat2matmon.e2	$⊢ E = \cdot_{{mulGrp}_{P}}$
12		monmat2matmon.y	$⊢ Y = {var}_{1} (R)$
13		monmat2matmon.m2	$⊢ \underset{˙}{\cdot} = \cdot_{C}$
14		monmat2matmon.t	$⊢ T = N matToPolyMat R$
15		eqid	$⊢ 0_{C} = 0_{C}$
16		crngring	$⊢ R \in CRing \to R \in Ring$
17	16	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land R \in Ring)$
18	1 2	pmatring	$⊢ (N \in Fin \land R \in Ring) \to C \in Ring$
19		ringcmn	$⊢ C \in Ring \to C \in CMnd$
20	17 18 19	3syl	$⊢ (N \in Fin \land R \in CRing) \to C \in CMnd$
21	20	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M))) \to C \in CMnd$
22	7	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
23	16 22	sylan2	$⊢ (N \in Fin \land R \in CRing) \to A \in Ring$
24	9	ply1ring	$⊢ A \in Ring \to Q \in Ring$
25		ringmnd	$⊢ Q \in Ring \to Q \in Mnd$
26	23 24 25	3syl	$⊢ (N \in Fin \land R \in CRing) \to Q \in Mnd$
27	26	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M))) \to Q \in Mnd$
28		nn0ex	$⊢ ℕ_{0} \in V$
29	28	a1i	$⊢ ((N \in Fin \land R \in CRing) \land (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M))) \to ℕ_{0} \in V$
30		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
31	1 2 3 4 5 6 7 9 30 10	pm2mpghm	$⊢ (N \in Fin \land R \in Ring) \to I \in (C GrpHom Q)$
32	16 31	sylan2	$⊢ (N \in Fin \land R \in CRing) \to I \in (C GrpHom Q)$
33	32	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M))) \to I \in (C GrpHom Q)$
34		ghmmhm	$⊢ I \in (C GrpHom Q) \to I \in (C MndHom Q)$
35	33 34	syl	$⊢ ((N \in Fin \land R \in CRing) \land (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M))) \to I \in (C MndHom Q)$
36	17	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M))) \to (N \in Fin \land R \in Ring)$
37	36	adantr	$⊢ (((N \in Fin \land R \in CRing) \land (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M))) \land n \in ℕ_{0}) \to (N \in Fin \land R \in Ring)$
38		elmapi	$⊢ M \in (K^{ℕ_{0}}) \to M : ℕ_{0} ⟶ K$
39	38	adantr	$⊢ (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M)) \to M : ℕ_{0} ⟶ K$
40	39	adantl	$⊢ ((N \in Fin \land R \in CRing) \land (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M))) \to M : ℕ_{0} ⟶ K$
41	40	ffvelcdmda	$⊢ (((N \in Fin \land R \in CRing) \land (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M))) \land n \in ℕ_{0}) \to M (n) \in K$
42		simpr	$⊢ (((N \in Fin \land R \in CRing) \land (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M))) \land n \in ℕ_{0}) \to n \in ℕ_{0}$
43	7 8 14 1 2 3 13 11 12	mat2pmatscmxcl	$⊢ ((N \in Fin \land R \in Ring) \land (M (n) \in K \land n \in ℕ_{0})) \to (n E Y) \underset{˙}{\cdot} T (M (n)) \in B$
44	37 41 42 43	syl12anc	$⊢ (((N \in Fin \land R \in CRing) \land (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M))) \land n \in ℕ_{0}) \to (n E Y) \underset{˙}{\cdot} T (M (n)) \in B$
45		fvexd	$⊢ ((N \in Fin \land R \in CRing) \land (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M))) \to 0_{C} \in V$
46		ovexd	$⊢ (((N \in Fin \land R \in CRing) \land (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M))) \land n \in ℕ_{0}) \to (n E Y) \underset{˙}{\cdot} T (M (n)) \in V$
47		simpr	$⊢ ((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \to M \in (K^{ℕ_{0}})$
48		fvex	$⊢ 0_{A} \in V$
49		fsuppmapnn0ub	$⊢ (M \in (K^{ℕ_{0}}) \land 0_{A} \in V) \to ({finSupp}_{0_{A}} (M) \to \exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to M (x) = 0_{A}))$
50	47 48 49	sylancl	$⊢ ((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \to ({finSupp}_{0_{A}} (M) \to \exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to M (x) = 0_{A}))$
51		csbov12g	$⊢ x \in ℕ_{0} \to ⦋ x / n ⦌ ((n E Y) \underset{˙}{\cdot} T (M (n))) = ⦋ x / n ⦌ (n E Y) \underset{˙}{\cdot} ⦋ x / n ⦌ T (M (n))$
52		csbov1g	$⊢ x \in ℕ_{0} \to ⦋ x / n ⦌ (n E Y) = ⦋ x / n ⦌ n E Y$
53		csbvarg	$⊢ x \in ℕ_{0} \to ⦋ x / n ⦌ n = x$
54	53	oveq1d	$⊢ x \in ℕ_{0} \to ⦋ x / n ⦌ n E Y = x E Y$
55	52 54	eqtrd	$⊢ x \in ℕ_{0} \to ⦋ x / n ⦌ (n E Y) = x E Y$
56		csbfv2g	$⊢ x \in ℕ_{0} \to ⦋ x / n ⦌ T (M (n)) = T (⦋ x / n ⦌ M (n))$
57		csbfv2g	$⊢ x \in ℕ_{0} \to ⦋ x / n ⦌ M (n) = M (⦋ x / n ⦌ n)$
58	53	fveq2d	$⊢ x \in ℕ_{0} \to M (⦋ x / n ⦌ n) = M (x)$
59	57 58	eqtrd	$⊢ x \in ℕ_{0} \to ⦋ x / n ⦌ M (n) = M (x)$
60	59	fveq2d	$⊢ x \in ℕ_{0} \to T (⦋ x / n ⦌ M (n)) = T (M (x))$
61	56 60	eqtrd	$⊢ x \in ℕ_{0} \to ⦋ x / n ⦌ T (M (n)) = T (M (x))$
62	55 61	oveq12d	$⊢ x \in ℕ_{0} \to ⦋ x / n ⦌ (n E Y) \underset{˙}{\cdot} ⦋ x / n ⦌ T (M (n)) = (x E Y) \underset{˙}{\cdot} T (M (x))$
63	51 62	eqtrd	$⊢ x \in ℕ_{0} \to ⦋ x / n ⦌ ((n E Y) \underset{˙}{\cdot} T (M (n))) = (x E Y) \underset{˙}{\cdot} T (M (x))$
64	63	adantl	$⊢ ((((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \land y \in ℕ_{0}) \land x \in ℕ_{0}) \to ⦋ x / n ⦌ ((n E Y) \underset{˙}{\cdot} T (M (n))) = (x E Y) \underset{˙}{\cdot} T (M (x))$
65	64	adantr	$⊢ (((((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \land y \in ℕ_{0}) \land x \in ℕ_{0}) \land M (x) = 0_{A}) \to ⦋ x / n ⦌ ((n E Y) \underset{˙}{\cdot} T (M (n))) = (x E Y) \underset{˙}{\cdot} T (M (x))$
66		fveq2	$⊢ M (x) = 0_{A} \to T (M (x)) = T (0_{A})$
67	66	oveq2d	$⊢ M (x) = 0_{A} \to (x E Y) \underset{˙}{\cdot} T (M (x)) = (x E Y) \underset{˙}{\cdot} T (0_{A})$
68	14 7 8 1 2 3	mat2pmatghm	$⊢ (N \in Fin \land R \in Ring) \to T \in (A GrpHom C)$
69	16 68	sylan2	$⊢ (N \in Fin \land R \in CRing) \to T \in (A GrpHom C)$
70	69	ad3antrrr	$⊢ ((((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \land y \in ℕ_{0}) \land x \in ℕ_{0}) \to T \in (A GrpHom C)$
71		ghmmhm	$⊢ T \in (A GrpHom C) \to T \in (A MndHom C)$
72		eqid	$⊢ 0_{A} = 0_{A}$
73	72 15	mhm0	$⊢ T \in (A MndHom C) \to T (0_{A}) = 0_{C}$
74	70 71 73	3syl	$⊢ ((((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \land y \in ℕ_{0}) \land x \in ℕ_{0}) \to T (0_{A}) = 0_{C}$
75	74	oveq2d	$⊢ ((((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \land y \in ℕ_{0}) \land x \in ℕ_{0}) \to (x E Y) \underset{˙}{\cdot} T (0_{A}) = (x E Y) \underset{˙}{\cdot} 0_{C}$
76	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
77	16 76	syl	$⊢ R \in CRing \to P \in Ring$
78	2	matlmod	$⊢ (N \in Fin \land P \in Ring) \to C \in LMod$
79	77 78	sylan2	$⊢ (N \in Fin \land R \in CRing) \to C \in LMod$
80	79	ad3antrrr	$⊢ ((((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \land y \in ℕ_{0}) \land x \in ℕ_{0}) \to C \in LMod$
81		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
82		eqid	$⊢ {Base}_{P} = {Base}_{P}$
83	81 82	mgpbas	$⊢ {Base}_{P} = {Base}_{{mulGrp}_{P}}$
84	77	adantl	$⊢ (N \in Fin \land R \in CRing) \to P \in Ring$
85	81	ringmgp	$⊢ P \in Ring \to {mulGrp}_{P} \in Mnd$
86	84 85	syl	$⊢ (N \in Fin \land R \in CRing) \to {mulGrp}_{P} \in Mnd$
87	86	ad3antrrr	$⊢ ((((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \land y \in ℕ_{0}) \land x \in ℕ_{0}) \to {mulGrp}_{P} \in Mnd$
88		simpr	$⊢ ((((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \land y \in ℕ_{0}) \land x \in ℕ_{0}) \to x \in ℕ_{0}$
89	16	adantl	$⊢ (N \in Fin \land R \in CRing) \to R \in Ring$
90	12 1 82	vr1cl	$⊢ R \in Ring \to Y \in {Base}_{P}$
91	89 90	syl	$⊢ (N \in Fin \land R \in CRing) \to Y \in {Base}_{P}$
92	91	ad3antrrr	$⊢ ((((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \land y \in ℕ_{0}) \land x \in ℕ_{0}) \to Y \in {Base}_{P}$
93	83 11 87 88 92	mulgnn0cld	$⊢ ((((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \land y \in ℕ_{0}) \land x \in ℕ_{0}) \to x E Y \in {Base}_{P}$
94	1	ply1crng	$⊢ R \in CRing \to P \in CRing$
95	2	matsca2	$⊢ (N \in Fin \land P \in CRing) \to P = Scalar (C)$
96	94 95	sylan2	$⊢ (N \in Fin \land R \in CRing) \to P = Scalar (C)$
97	96	eqcomd	$⊢ (N \in Fin \land R \in CRing) \to Scalar (C) = P$
98	97	ad3antrrr	$⊢ ((((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \land y \in ℕ_{0}) \land x \in ℕ_{0}) \to Scalar (C) = P$
99	98	fveq2d	$⊢ ((((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \land y \in ℕ_{0}) \land x \in ℕ_{0}) \to {Base}_{Scalar (C)} = {Base}_{P}$
100	93 99	eleqtrrd	$⊢ ((((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \land y \in ℕ_{0}) \land x \in ℕ_{0}) \to x E Y \in {Base}_{Scalar (C)}$
101		eqid	$⊢ Scalar (C) = Scalar (C)$
102		eqid	$⊢ {Base}_{Scalar (C)} = {Base}_{Scalar (C)}$
103	101 13 102 15	lmodvs0	$⊢ (C \in LMod \land x E Y \in {Base}_{Scalar (C)}) \to (x E Y) \underset{˙}{\cdot} 0_{C} = 0_{C}$
104	80 100 103	syl2anc	$⊢ ((((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \land y \in ℕ_{0}) \land x \in ℕ_{0}) \to (x E Y) \underset{˙}{\cdot} 0_{C} = 0_{C}$
105	75 104	eqtrd	$⊢ ((((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \land y \in ℕ_{0}) \land x \in ℕ_{0}) \to (x E Y) \underset{˙}{\cdot} T (0_{A}) = 0_{C}$
106	67 105	sylan9eqr	$⊢ (((((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \land y \in ℕ_{0}) \land x \in ℕ_{0}) \land M (x) = 0_{A}) \to (x E Y) \underset{˙}{\cdot} T (M (x)) = 0_{C}$
107	65 106	eqtrd	$⊢ (((((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \land y \in ℕ_{0}) \land x \in ℕ_{0}) \land M (x) = 0_{A}) \to ⦋ x / n ⦌ ((n E Y) \underset{˙}{\cdot} T (M (n))) = 0_{C}$
108	107	ex	$⊢ ((((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \land y \in ℕ_{0}) \land x \in ℕ_{0}) \to (M (x) = 0_{A} \to ⦋ x / n ⦌ ((n E Y) \underset{˙}{\cdot} T (M (n))) = 0_{C})$
109	108	imim2d	$⊢ ((((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \land y \in ℕ_{0}) \land x \in ℕ_{0}) \to ((y < x \to M (x) = 0_{A}) \to (y < x \to ⦋ x / n ⦌ ((n E Y) \underset{˙}{\cdot} T (M (n))) = 0_{C}))$
110	109	ralimdva	$⊢ (((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \land y \in ℕ_{0}) \to (\forall x \in ℕ_{0} (y < x \to M (x) = 0_{A}) \to \forall x \in ℕ_{0} (y < x \to ⦋ x / n ⦌ ((n E Y) \underset{˙}{\cdot} T (M (n))) = 0_{C}))$
111	110	reximdva	$⊢ ((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \to (\exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to M (x) = 0_{A}) \to \exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to ⦋ x / n ⦌ ((n E Y) \underset{˙}{\cdot} T (M (n))) = 0_{C}))$
112	50 111	syld	$⊢ ((N \in Fin \land R \in CRing) \land M \in (K^{ℕ_{0}})) \to ({finSupp}_{0_{A}} (M) \to \exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to ⦋ x / n ⦌ ((n E Y) \underset{˙}{\cdot} T (M (n))) = 0_{C}))$
113	112	impr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M))) \to \exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to ⦋ x / n ⦌ ((n E Y) \underset{˙}{\cdot} T (M (n))) = 0_{C})$
114	45 46 113	mptnn0fsupp	$⊢ ((N \in Fin \land R \in CRing) \land (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M))) \to {finSupp}_{0_{C}} ((n \in ℕ_{0} ⟼ (n E Y) \underset{˙}{\cdot} T (M (n))))$
115	3 15 21 27 29 35 44 114	gsummptmhm	$⊢ ((N \in Fin \land R \in CRing) \land (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M))) \to \underset{n \in ℕ_{0}}{\sum_{Q}} I ((n E Y) \underset{˙}{\cdot} T (M (n))) = I (\underset{n \in ℕ_{0}}{\sum_{C}} ((n E Y) \underset{˙}{\cdot} T (M (n))))$
116		simpll	$⊢ (((N \in Fin \land R \in CRing) \land (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M))) \land n \in ℕ_{0}) \to (N \in Fin \land R \in CRing)$
117	1 2 3 4 5 6 7 8 9 10 11 12 13 14	monmat2matmon	$⊢ ((N \in Fin \land R \in CRing) \land (M (n) \in K \land n \in ℕ_{0})) \to I ((n E Y) \underset{˙}{\cdot} T (M (n))) = M (n) \underset{˙}{*} (n \underset{˙}{\times} X)$
118	116 41 42 117	syl12anc	$⊢ (((N \in Fin \land R \in CRing) \land (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M))) \land n \in ℕ_{0}) \to I ((n E Y) \underset{˙}{\cdot} T (M (n))) = M (n) \underset{˙}{*} (n \underset{˙}{\times} X)$
119	118	mpteq2dva	$⊢ ((N \in Fin \land R \in CRing) \land (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M))) \to (n \in ℕ_{0} ⟼ I ((n E Y) \underset{˙}{\cdot} T (M (n)))) = (n \in ℕ_{0} ⟼ M (n) \underset{˙}{*} (n \underset{˙}{\times} X))$
120	119	oveq2d	$⊢ ((N \in Fin \land R \in CRing) \land (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M))) \to \underset{n \in ℕ_{0}}{\sum_{Q}} I ((n E Y) \underset{˙}{\cdot} T (M (n))) = \underset{n \in ℕ_{0}}{\sum_{Q}} (M (n) \underset{˙}{*} (n \underset{˙}{\times} X))$
121	115 120	eqtr3d	$⊢ ((N \in Fin \land R \in CRing) \land (M \in (K^{ℕ_{0}}) \land {finSupp}_{0_{A}} (M))) \to I (\underset{n \in ℕ_{0}}{\sum_{C}} ((n E Y) \underset{˙}{\cdot} T (M (n)))) = \underset{n \in ℕ_{0}}{\sum_{Q}} (M (n) \underset{˙}{*} (n \underset{˙}{\times} X))$

Metamath Proof Explorer

Theorem pm2mp

Proof