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	9	ply1ring	$⊢ A \in Ring \to Q \in Ring$
46	36 45	syl	$⊢ (N \in Fin \land R \in Ring) \to Q \in Ring$
47		eqid	$⊢ {mulGrp}_{Q} = {mulGrp}_{Q}$
48	47	ringmgp	$⊢ Q \in Ring \to {mulGrp}_{Q} \in Mnd$
49	46 48	syl	$⊢ (N \in Fin \land R \in Ring) \to {mulGrp}_{Q} \in Mnd$
50	49	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$
51		simpr	$⊢ (((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
52		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
53	6 9 52	vr1cl	$⊢ A \in Ring \to X \in {Base}_{Q}$
54	36 53	syl	$⊢ (N \in Fin \land R \in Ring) \to X \in {Base}_{Q}$
55	54	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}$
56	47 52	mgpbas	$⊢ {Base}_{Q} = {Base}_{{mulGrp}_{Q}}$
57	56 5	mulgnn0cl	$⊢ ({mulGrp}_{Q} \in Mnd \land k \in ℕ_{0} \land X \in {Base}_{Q}) \to k \underset{˙}{\times} X \in {Base}_{Q}$
58	50 51 55 57	syl3anc	$⊢ (((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}$
59		eqid	$⊢ Scalar (Q) = Scalar (Q)$
60		eqid	$⊢ 0_{Scalar (Q)} = 0_{Scalar (Q)}$
61		eqid	$⊢ 0_{Q} = 0_{Q}$
62	52 59 4 60 61	lmod0vs	$⊢ (Q \in LMod \land k \underset{˙}{\times} X \in {Base}_{Q}) \to 0_{Scalar (Q)} \underset{˙}{*} (k \underset{˙}{\times} X) = 0_{Q}$
63	44 58 62	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}$
64	41 63	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}$
65	64	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})$
66	35 65	syl5eq	$⊢ (((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})$
67	34 66	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})$
68	30 67	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})$
69	68	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}))$
70	69	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})$
71		ringmnd	$⊢ Q \in Ring \to Q \in Mnd$
72	46 71	syl	$⊢ (N \in Fin \land R \in Ring) \to Q \in Mnd$
73	72	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \to Q \in Mnd$
74		nn0ex	$⊢ ℕ_{0} \in V$
75	74	a1i	$⊢ ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \to ℕ_{0} \in V$
76		simprr	$⊢ ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \to L \in ℕ_{0}$
77		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}))$
78	38	fveq2d	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{A} = {Base}_{Scalar (Q)}$
79	8 78	syl5eq	$⊢ (N \in Fin \land R \in Ring) \to K = {Base}_{Scalar (Q)}$
80	79	eleq2d	$⊢ (N \in Fin \land R \in Ring) \to (M \in K \leftrightarrow M \in {Base}_{Scalar (Q)})$
81	80	biimpcd	$⊢ M \in K \to ((N \in Fin \land R \in Ring) \to M \in {Base}_{Scalar (Q)})$
82	81	adantr	$⊢ (M \in K \land L \in ℕ_{0}) \to ((N \in Fin \land R \in Ring) \to M \in {Base}_{Scalar (Q)})$
83	82	impcom	$⊢ ((N \in Fin \land R \in Ring) \land (M \in K \land L \in ℕ_{0})) \to M \in {Base}_{Scalar (Q)}$
84	83	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)}$
85		eqid	$⊢ {Base}_{Scalar (Q)} = {Base}_{Scalar (Q)}$
86	52 59 4 85	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}$
87	44 84 58 86	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}$
88	87	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}$
89	61 73 75 76 77 88	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))$
90	15 89	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))$
91	70 90	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))$
92		csbov2g	$⊢ L \in ℕ_{0} \to ⦋ L / k ⦌ (M \underset{˙}{} (k \underset{˙}{\times} X)) = M \underset{˙}{} ⦋ L / k ⦌ (k \underset{˙}{\times} X)$
93		csbov1g	$⊢ L \in ℕ_{0} \to ⦋ L / k ⦌ (k \underset{˙}{\times} X) = ⦋ L / k ⦌ k \underset{˙}{\times} X$
94		csbvarg	$⊢ L \in ℕ_{0} \to ⦋ L / k ⦌ k = L$
95	94	oveq1d	$⊢ L \in ℕ_{0} \to ⦋ L / k ⦌ k \underset{˙}{\times} X = L \underset{˙}{\times} X$
96	93 95	eqtrd	$⊢ L \in ℕ_{0} \to ⦋ L / k ⦌ (k \underset{˙}{\times} X) = L \underset{˙}{\times} X$
97	96	oveq2d	$⊢ L \in ℕ_{0} \to M \underset{˙}{} ⦋ L / k ⦌ (k \underset{˙}{\times} X) = M \underset{˙}{} (L \underset{˙}{\times} X)$
98	92 97	eqtrd	$⊢ L \in ℕ_{0} \to ⦋ L / k ⦌ (M \underset{˙}{} (k \underset{˙}{\times} X)) = M \underset{˙}{} (L \underset{˙}{\times} X)$
99	98	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)$
100	21 91 99	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