pm2mpcoe1

Description: A coefficient of the polynomial over matrices which is the result of the transformation of a polynomial matrix is the matrix consisting of the coefficients in the polynomial entries of the polynomial matrix. (Contributed by AV, 20-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$
Assertion	pm2mpcoe1	$⊢ ((N \in Fin \land R \in Ring) \land (M \in B \land K \in ℕ_{0})) \to {coe}_{1} (T (M)) (K) = M decompPMat K$

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		simpll	$⊢ ((N \in Fin \land R \in Ring) \land (M \in B \land K \in ℕ_{0})) \to N \in Fin$
11		simplr	$⊢ ((N \in Fin \land R \in Ring) \land (M \in B \land K \in ℕ_{0})) \to R \in Ring$
12		simprl	$⊢ ((N \in Fin \land R \in Ring) \land (M \in B \land K \in ℕ_{0})) \to M \in B$
13	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))$
14	10 11 12 13	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (M \in B \land K \in ℕ_{0})) \to T (M) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((M decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
15	14	fveq2d	$⊢ ((N \in Fin \land R \in Ring) \land (M \in B \land K \in ℕ_{0})) \to {coe}_{1} (T (M)) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((M decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X)))$
16	15	fveq1d	$⊢ ((N \in Fin \land R \in Ring) \land (M \in B \land K \in ℕ_{0})) \to {coe}_{1} (T (M)) (K) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((M decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))) (K)$
17		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
18	7	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
19	18	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (M \in B \land K \in ℕ_{0})) \to A \in Ring$
20		eqid	$⊢ {Base}_{A} = {Base}_{A}$
21		eqid	$⊢ 0_{A} = 0_{A}$
22	11	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (M \in B \land K \in ℕ_{0})) \land k \in ℕ_{0}) \to R \in Ring$
23	12	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (M \in B \land K \in ℕ_{0})) \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})) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
25	1 2 3 7 20	decpmatcl	$⊢ (R \in Ring \land M \in B \land k \in ℕ_{0}) \to M decompPMat k \in {Base}_{A}$
26	22 23 24 25	syl3anc	$⊢ (((N \in Fin \land R \in Ring) \land (M \in B \land K \in ℕ_{0})) \land k \in ℕ_{0}) \to M decompPMat k \in {Base}_{A}$
27	26	ralrimiva	$⊢ ((N \in Fin \land R \in Ring) \land (M \in B \land K \in ℕ_{0})) \to \forall k \in ℕ_{0} M decompPMat k \in {Base}_{A}$
28	1 2 3 7 21	decpmatfsupp	$⊢ (R \in Ring \land M \in B) \to {finSupp}_{0_{A}} ((k \in ℕ_{0} ⟼ M decompPMat k))$
29	28	ad2ant2lr	$⊢ ((N \in Fin \land R \in Ring) \land (M \in B \land K \in ℕ_{0})) \to {finSupp}_{0_{A}} ((k \in ℕ_{0} ⟼ M decompPMat k))$
30		simpr	$⊢ (M \in B \land K \in ℕ_{0}) \to K \in ℕ_{0}$
31	30	adantl	$⊢ ((N \in Fin \land R \in Ring) \land (M \in B \land K \in ℕ_{0})) \to K \in ℕ_{0}$
32	8 17 6 5 19 20 4 21 27 29 31	gsummoncoe1	$⊢ ((N \in Fin \land R \in Ring) \land (M \in B \land K \in ℕ_{0})) \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((M decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))) (K) = ⦋ K / k ⦌ (M decompPMat k)$
33		csbov2g	$⊢ K \in ℕ_{0} \to ⦋ K / k ⦌ (M decompPMat k) = M decompPMat ⦋ K / k ⦌ k$
34		csbvarg	$⊢ K \in ℕ_{0} \to ⦋ K / k ⦌ k = K$
35	34	oveq2d	$⊢ K \in ℕ_{0} \to M decompPMat ⦋ K / k ⦌ k = M decompPMat K$
36	33 35	eqtrd	$⊢ K \in ℕ_{0} \to ⦋ K / k ⦌ (M decompPMat k) = M decompPMat K$
37	36	adantl	$⊢ (M \in B \land K \in ℕ_{0}) \to ⦋ K / k ⦌ (M decompPMat k) = M decompPMat K$
38	37	adantl	$⊢ ((N \in Fin \land R \in Ring) \land (M \in B \land K \in ℕ_{0})) \to ⦋ K / k ⦌ (M decompPMat k) = M decompPMat K$
39	16 32 38	3eqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (M \in B \land K \in ℕ_{0})) \to {coe}_{1} (T (M)) (K) = M decompPMat K$

Metamath Proof Explorer

Theorem pm2mpcoe1

Proof