pmatcollpw1lem2

Description: Lemma 2 for pmatcollpw1 : An entry of a polynomial matrix is the sum of the entries of the matrix consisting of the coefficients in the entries of the polynomial matrix multiplied with the corresponding power of the variable. (Contributed by AV, 25-Sep-2019) (Revised by AV, 3-Dec-2019)

	Ref	Expression
Hypotheses	pmatcollpw1.p	$⊢ P = {Poly}_{1} (R)$
	pmatcollpw1.c	$⊢ C = N Mat P$
	pmatcollpw1.b	$⊢ B = {Base}_{C}$
	pmatcollpw1.m	$⊢ \underset{˙}{\times} = \cdot_{P}$
	pmatcollpw1.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
	pmatcollpw1.x	$⊢ X = {var}_{1} (R)$
Assertion	pmatcollpw1lem2	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to a M b = \underset{n \in ℕ_{0}}{\sum_{P}} ((a (M decompPMat n) b) \underset{˙}{\times} (n \underset{˙}{\times} X))$

Proof

Step	Hyp	Ref	Expression
1		pmatcollpw1.p	$⊢ P = {Poly}_{1} (R)$
2		pmatcollpw1.c	$⊢ C = N Mat P$
3		pmatcollpw1.b	$⊢ B = {Base}_{C}$
4		pmatcollpw1.m	$⊢ \underset{˙}{\times} = \cdot_{P}$
5		pmatcollpw1.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
6		pmatcollpw1.x	$⊢ X = {var}_{1} (R)$
7		simpl2	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to R \in Ring$
8		eqid	$⊢ {Base}_{P} = {Base}_{P}$
9		simprl	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to a \in N$
10		simprr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to b \in N$
11		simpl3	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to M \in B$
12	2 8 3 9 10 11	matecld	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to a M b \in {Base}_{P}$
13		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
14		eqid	$⊢ \cdot_{{mulGrp}_{P}} = \cdot_{{mulGrp}_{P}}$
15		eqid	$⊢ {coe}_{1} (a M b) = {coe}_{1} (a M b)$
16	1 6 8 4 13 14 15	ply1coe	$⊢ (R \in Ring \land a M b \in {Base}_{P}) \to a M b = \underset{n \in ℕ_{0}}{\sum_{P}} ({coe}_{1} (a M b) (n) \underset{˙}{\times} (n \cdot_{{mulGrp}_{P}} X))$
17	7 12 16	syl2anc	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to a M b = \underset{n \in ℕ_{0}}{\sum_{P}} ({coe}_{1} (a M b) (n) \underset{˙}{\times} (n \cdot_{{mulGrp}_{P}} X))$
18	7	adantr	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to R \in Ring$
19	11	adantr	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to M \in B$
20		simpr	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to n \in ℕ_{0}$
21		simpr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to (a \in N \land b \in N)$
22	21	adantr	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to (a \in N \land b \in N)$
23	1 2 3	decpmate	$⊢ ((R \in Ring \land M \in B \land n \in ℕ_{0}) \land (a \in N \land b \in N)) \to a (M decompPMat n) b = {coe}_{1} (a M b) (n)$
24	18 19 20 22 23	syl31anc	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to a (M decompPMat n) b = {coe}_{1} (a M b) (n)$
25	24	eqcomd	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to {coe}_{1} (a M b) (n) = a (M decompPMat n) b$
26	5	eqcomi	$⊢ \cdot_{{mulGrp}_{P}} = \underset{˙}{\times}$
27	26	oveqi	$⊢ n \cdot_{{mulGrp}_{P}} X = n \underset{˙}{\times} X$
28	27	a1i	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to n \cdot_{{mulGrp}_{P}} X = n \underset{˙}{\times} X$
29	25 28	oveq12d	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to {coe}_{1} (a M b) (n) \underset{˙}{\times} (n \cdot_{{mulGrp}_{P}} X) = (a (M decompPMat n) b) \underset{˙}{\times} (n \underset{˙}{\times} X)$
30	29	mpteq2dva	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to (n \in ℕ_{0} ⟼ {coe}_{1} (a M b) (n) \underset{˙}{\times} (n \cdot_{{mulGrp}_{P}} X)) = (n \in ℕ_{0} ⟼ (a (M decompPMat n) b) \underset{˙}{\times} (n \underset{˙}{\times} X))$
31	30	oveq2d	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to \underset{n \in ℕ_{0}}{\sum_{P}} ({coe}_{1} (a M b) (n) \underset{˙}{\times} (n \cdot_{{mulGrp}_{P}} X)) = \underset{n \in ℕ_{0}}{\sum_{P}} ((a (M decompPMat n) b) \underset{˙}{\times} (n \underset{˙}{\times} X))$
32	17 31	eqtrd	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (a \in N \land b \in N)) \to a M b = \underset{n \in ℕ_{0}}{\sum_{P}} ((a (M decompPMat n) b) \underset{˙}{\times} (n \underset{˙}{\times} X))$

Metamath Proof Explorer

Theorem pmatcollpw1lem2

Proof