monmat2matmon

Description: The transformation of a polynomial matrix having scaled monomials with the same power as entries into a scaled monomial as a polynomial over matrices. (Contributed by AV, 11-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	monmat2matmon	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0})) \to I ((L E Y) \underset{˙}{\cdot} T (M)) = M \underset{˙}{*} (L \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		crngring	$⊢ R \in CRing \to R \in Ring$
16		simpll	$⊢ ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \to N \in Fin$
17		simplr	$⊢ ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \to R \in Ring$
18	7 8 14 1 2 3 13 11 12	mat2pmatscmxcl	$⊢ ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \to (L E Y) \underset{˙}{\cdot} T (M) \in B$
19	1 2 3 4 5 6 7 9 10	pm2mpfval	$⊢ (N \in Fin \land R \in Ring \land (L E Y) \underset{˙}{\cdot} T (M) \in B) \to I ((L E Y) \underset{˙}{\cdot} T (M)) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((((L E Y) \underset{˙}{\cdot} T (M)) decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
20	16 17 18 19	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \to I ((L E Y) \underset{˙}{\cdot} T (M)) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((((L E Y) \underset{˙}{\cdot} T (M)) decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
21	15 20	sylanl2	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0})) \to I ((L E Y) \underset{˙}{\cdot} T (M)) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((((L E Y) \underset{˙}{\cdot} T (M)) decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
22		simpll	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to (N \in Fin \land R \in CRing)$
23		simpr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0})) \to (M \in K \land L \in ℕ_{0})$
24	23	anim1i	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to ((M \in K \land L \in ℕ_{0}) \land k \in ℕ_{0})$
25		df-3an	$⊢ (M \in K \land L \in ℕ_{0} \land k \in ℕ_{0}) \leftrightarrow ((M \in K \land L \in ℕ_{0}) \land k \in ℕ_{0})$
26	24 25	sylibr	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to (M \in K \land L \in ℕ_{0} \land k \in ℕ_{0})$
27		eqid	$⊢ 0_{A} = 0_{A}$
28	1 2 7 8 27 11 12 13 14	monmatcollpw	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land k \in ℕ_{0})) \to ((L E Y) \underset{˙}{\cdot} T (M)) decompPMat k = if (k = L, M, 0_{A})$
29	22 26 28	syl2anc	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to ((L E Y) \underset{˙}{\cdot} T (M)) decompPMat k = if (k = L, M, 0_{A})$
30	29	oveq1d	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to (((L E Y) \underset{˙}{\cdot} T (M)) decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X) = if (k = L, M, 0_{A}) \underset{˙}{} (k \underset{˙}{\times} X)$
31	15	a1i	$⊢ k \in ℕ_{0} \to (R \in CRing \to R \in Ring)$
32	31	anim2d	$⊢ k \in ℕ_{0} \to ((N \in Fin \land R \in CRing) \to (N \in Fin \land R \in Ring))$
33	32	anim1d	$⊢ k \in ℕ_{0} \to (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0})) \to ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})))$
34	33	imdistanri	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to (((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0})$
35		ovif	$⊢ if (k = L, M, 0_{A}) \underset{˙}{} (k \underset{˙}{\times} X) = if (k = L, M \underset{˙}{} (k \underset{˙}{\times} X), 0_{A} \underset{˙}{*} (k \underset{˙}{\times} X))$
36	7	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
37	9	ply1sca	$⊢ A \in Ring \to A = Scalar (Q)$
38	36 37	syl	$⊢ (N \in Fin \land R \in Ring) \to A = Scalar (Q)$
39	38	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to A = Scalar (Q)$
40	39	fveq2d	$⊢ (((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to 0_{A} = 0_{Scalar (Q)}$
41	40	oveq1d	$⊢ (((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to 0_{A} \underset{˙}{} (k \underset{˙}{\times} X) = 0_{Scalar (Q)} \underset{˙}{} (k \underset{˙}{\times} X)$
42	9	ply1lmod	$⊢ A \in Ring \to Q \in LMod$
43	36 42	syl	$⊢ (N \in Fin \land R \in Ring) \to Q \in LMod$
44	43	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to Q \in LMod$
45		eqid	$⊢ {mulGrp}_{Q} = {mulGrp}_{Q}$
46		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
47	45 46	mgpbas	$⊢ {Base}_{Q} = {Base}_{{mulGrp}_{Q}}$
48	9	ply1ring	$⊢ A \in Ring \to Q \in Ring$
49	36 48	syl	$⊢ (N \in Fin \land R \in Ring) \to Q \in Ring$
50	45	ringmgp	$⊢ Q \in Ring \to {mulGrp}_{Q} \in Mnd$
51	49 50	syl	$⊢ (N \in Fin \land R \in Ring) \to {mulGrp}_{Q} \in Mnd$
52	51	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to {mulGrp}_{Q} \in Mnd$
53		simpr	$⊢ (((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
54	6 9 46	vr1cl	$⊢ A \in Ring \to X \in {Base}_{Q}$
55	36 54	syl	$⊢ (N \in Fin \land R \in Ring) \to X \in {Base}_{Q}$
56	55	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to X \in {Base}_{Q}$
57	47 5 52 53 56	mulgnn0cld	$⊢ (((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to k \underset{˙}{\times} X \in {Base}_{Q}$
58		eqid	$⊢ Scalar (Q) = Scalar (Q)$
59		eqid	$⊢ 0_{Scalar (Q)} = 0_{Scalar (Q)}$
60		eqid	$⊢ 0_{Q} = 0_{Q}$
61	46 58 4 59 60	lmod0vs	$⊢ (Q \in LMod \land k \underset{˙}{\times} X \in {Base}_{Q}) \to 0_{Scalar (Q)} \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{Q}$
62	44 57 61	syl2anc	$⊢ (((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to 0_{Scalar (Q)} \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{Q}$
63	41 62	eqtrd	$⊢ (((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to 0_{A} \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{Q}$
64	63	ifeq2d	$⊢ (((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to if (k = L, M \underset{˙}{} (k \underset{˙}{\times} X), 0_{A} \underset{˙}{} (k \underset{˙}{\times} X)) = if (k = L, M \underset{˙}{*} (k \underset{˙}{\times} X), 0_{Q})$
65	35 64	eqtrid	$⊢ (((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to if (k = L, M, 0_{A}) \underset{˙}{} (k \underset{˙}{\times} X) = if (k = L, M \underset{˙}{} (k \underset{˙}{\times} X), 0_{Q})$
66	34 65	syl	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to if (k = L, M, 0_{A}) \underset{˙}{} (k \underset{˙}{\times} X) = if (k = L, M \underset{˙}{} (k \underset{˙}{\times} X), 0_{Q})$
67	30 66	eqtrd	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to (((L E Y) \underset{˙}{\cdot} T (M)) decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X) = if (k = L, M \underset{˙}{} (k \underset{˙}{\times} X), 0_{Q})$
68	67	mpteq2dva	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0})) \to (k \in ℕ_{0} ⟼ (((L E Y) \underset{˙}{\cdot} T (M)) decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X)) = (k \in ℕ_{0} ⟼ if (k = L, M \underset{˙}{} (k \underset{˙}{\times} X), 0_{Q}))$
69	68	oveq2d	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0})) \to \underset{k \in ℕ_{0}}{\sum_{Q}} ((((L E Y) \underset{˙}{\cdot} T (M)) decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X)) = \underset{k \in ℕ_{0}}{\sum_{Q}} if (k = L, M \underset{˙}{} (k \underset{˙}{\times} X), 0_{Q})$
70		ringmnd	$⊢ Q \in Ring \to Q \in Mnd$
71	49 70	syl	$⊢ (N \in Fin \land R \in Ring) \to Q \in Mnd$
72	71	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \to Q \in Mnd$
73		nn0ex	$⊢ ℕ_{0} \in V$
74	73	a1i	$⊢ ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \to ℕ_{0} \in V$
75		simprr	$⊢ ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \to L \in ℕ_{0}$
76		eqid	$⊢ (k \in ℕ_{0} ⟼ if (k = L, M \underset{˙}{} (k \underset{˙}{\times} X), 0_{Q})) = (k \in ℕ_{0} ⟼ if (k = L, M \underset{˙}{} (k \underset{˙}{\times} X), 0_{Q}))$
77	38	fveq2d	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{A} = {Base}_{Scalar (Q)}$
78	8 77	eqtrid	$⊢ (N \in Fin \land R \in Ring) \to K = {Base}_{Scalar (Q)}$
79	78	eleq2d	$⊢ (N \in Fin \land R \in Ring) \to (M \in K \leftrightarrow M \in {Base}_{Scalar (Q)})$
80	79	biimpcd	$⊢ M \in K \to ((N \in Fin \land R \in Ring) \to M \in {Base}_{Scalar (Q)})$
81	80	adantr	$⊢ (M \in K \land L \in ℕ_{0}) \to ((N \in Fin \land R \in Ring) \to M \in {Base}_{Scalar (Q)})$
82	81	impcom	$⊢ ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \to M \in {Base}_{Scalar (Q)}$
83	82	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to M \in {Base}_{Scalar (Q)}$
84		eqid	$⊢ {Base}_{Scalar (Q)} = {Base}_{Scalar (Q)}$
85	46 58 4 84	lmodvscl	$⊢ (Q \in LMod \land M \in {Base}_{Scalar (Q)} \land k \underset{˙}{\times} X \in {Base}_{Q}) \to M \underset{˙}{*} (k \underset{˙}{\times} X) \in {Base}_{Q}$
86	44 83 57 85	syl3anc	$⊢ (((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to M \underset{˙}{*} (k \underset{˙}{\times} X) \in {Base}_{Q}$
87	86	ralrimiva	$⊢ ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \to \forall k \in ℕ_{0} M \underset{˙}{*} (k \underset{˙}{\times} X) \in {Base}_{Q}$
88	60 72 74 75 76 87	gsummpt1n0	$⊢ ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \to \underset{k \in ℕ_{0}}{\sum_{Q}} if (k = L, M \underset{˙}{} (k \underset{˙}{\times} X), 0_{Q}) = ⦋ L / k ⦌ (M \underset{˙}{} (k \underset{˙}{\times} X))$
89	15 88	sylanl2	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0})) \to \underset{k \in ℕ_{0}}{\sum_{Q}} if (k = L, M \underset{˙}{} (k \underset{˙}{\times} X), 0_{Q}) = ⦋ L / k ⦌ (M \underset{˙}{} (k \underset{˙}{\times} X))$
90	69 89	eqtrd	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0})) \to \underset{k \in ℕ_{0}}{\sum_{Q}} ((((L E Y) \underset{˙}{\cdot} T (M)) decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X)) = ⦋ L / k ⦌ (M \underset{˙}{} (k \underset{˙}{\times} X))$
91		csbov2g	$⊢ L \in ℕ_{0} \to ⦋ L / k ⦌ (M \underset{˙}{} (k \underset{˙}{\times} X)) = M \underset{˙}{} ⦋ L / k ⦌ (k \underset{˙}{\times} X)$
92		csbov1g	$⊢ L \in ℕ_{0} \to ⦋ L / k ⦌ (k \underset{˙}{\times} X) = ⦋ L / k ⦌ k \underset{˙}{\times} X$
93		csbvarg	$⊢ L \in ℕ_{0} \to ⦋ L / k ⦌ k = L$
94	93	oveq1d	$⊢ L \in ℕ_{0} \to ⦋ L / k ⦌ k \underset{˙}{\times} X = L \underset{˙}{\times} X$
95	92 94	eqtrd	$⊢ L \in ℕ_{0} \to ⦋ L / k ⦌ (k \underset{˙}{\times} X) = L \underset{˙}{\times} X$
96	95	oveq2d	$⊢ L \in ℕ_{0} \to M \underset{˙}{} ⦋ L / k ⦌ (k \underset{˙}{\times} X) = M \underset{˙}{} (L \underset{˙}{\times} X)$
97	91 96	eqtrd	$⊢ L \in ℕ_{0} \to ⦋ L / k ⦌ (M \underset{˙}{} (k \underset{˙}{\times} X)) = M \underset{˙}{} (L \underset{˙}{\times} X)$
98	97	ad2antll	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0})) \to ⦋ L / k ⦌ (M \underset{˙}{} (k \underset{˙}{\times} X)) = M \underset{˙}{} (L \underset{˙}{\times} X)$
99	21 90 98	3eqtrd	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0})) \to I ((L E Y) \underset{˙}{\cdot} T (M)) = M \underset{˙}{*} (L \underset{˙}{\times} X)$

Metamath Proof Explorer

Theorem monmat2matmon

Proof