coe1sclmulval

Description: The value of the coefficient vector of a polynomial multiplied on the left by a scalar. (Contributed by AV, 14-Aug-2019)

	Ref	Expression
Hypotheses	coe1sclmulval.p	$⊢ P = {Poly}_{1} (R)$
	coe1sclmulval.b	$⊢ B = {Base}_{P}$
	coe1sclmulval.k	$⊢ K = {Base}_{R}$
	coe1sclmulval.a	$⊢ A = algSc (P)$
	coe1sclmulval.s	$⊢ S = \cdot_{P}$
	coe1sclmulval.t	$⊢ \underset{˙}{∙} = \cdot_{P}$
	coe1sclmulval.u	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	coe1sclmulval	$⊢ (R \in Ring \land (Y \in K \land Z \in B) \land N \in ℕ_{0}) \to {coe}_{1} (Y S Z) (N) = Y \underset{˙}{\cdot} {coe}_{1} (Z) (N)$

Proof

Step	Hyp	Ref	Expression
1		coe1sclmulval.p	$⊢ P = {Poly}_{1} (R)$
2		coe1sclmulval.b	$⊢ B = {Base}_{P}$
3		coe1sclmulval.k	$⊢ K = {Base}_{R}$
4		coe1sclmulval.a	$⊢ A = algSc (P)$
5		coe1sclmulval.s	$⊢ S = \cdot_{P}$
6		coe1sclmulval.t	$⊢ \underset{˙}{∙} = \cdot_{P}$
7		coe1sclmulval.u	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
8		simp1	$⊢ (R \in Ring \land (Y \in K \land Z \in B) \land N \in ℕ_{0}) \to R \in Ring$
9		simp2l	$⊢ (R \in Ring \land (Y \in K \land Z \in B) \land N \in ℕ_{0}) \to Y \in K$
10		simp2r	$⊢ (R \in Ring \land (Y \in K \land Z \in B) \land N \in ℕ_{0}) \to Z \in B$
11		eqid	$⊢ {var}_{1} (R) = {var}_{1} (R)$
12		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
13		eqid	$⊢ \cdot_{{mulGrp}_{P}} = \cdot_{{mulGrp}_{P}}$
14		eqid	$⊢ algSc (P) = algSc (P)$
15	3 1 2 11 5 6 12 13 14	ply1sclrmsm	$⊢ (R \in Ring \land Y \in K \land Z \in B) \to algSc (P) (Y) \underset{˙}{∙} Z = Y S Z$
16	8 9 10 15	syl3anc	$⊢ (R \in Ring \land (Y \in K \land Z \in B) \land N \in ℕ_{0}) \to algSc (P) (Y) \underset{˙}{∙} Z = Y S Z$
17	16	eqcomd	$⊢ (R \in Ring \land (Y \in K \land Z \in B) \land N \in ℕ_{0}) \to Y S Z = algSc (P) (Y) \underset{˙}{∙} Z$
18	17	fveq2d	$⊢ (R \in Ring \land (Y \in K \land Z \in B) \land N \in ℕ_{0}) \to {coe}_{1} (Y S Z) = {coe}_{1} (algSc (P) (Y) \underset{˙}{∙} Z)$
19	18	fveq1d	$⊢ (R \in Ring \land (Y \in K \land Z \in B) \land N \in ℕ_{0}) \to {coe}_{1} (Y S Z) (N) = {coe}_{1} (algSc (P) (Y) \underset{˙}{∙} Z) (N)$
20	1 2 3 14 6 7	coe1sclmulfv	$⊢ (R \in Ring \land (Y \in K \land Z \in B) \land N \in ℕ_{0}) \to {coe}_{1} (algSc (P) (Y) \underset{˙}{∙} Z) (N) = Y \underset{˙}{\cdot} {coe}_{1} (Z) (N)$
21	19 20	eqtrd	$⊢ (R \in Ring \land (Y \in K \land Z \in B) \land N \in ℕ_{0}) \to {coe}_{1} (Y S Z) (N) = Y \underset{˙}{\cdot} {coe}_{1} (Z) (N)$

Metamath Proof Explorer

Theorem coe1sclmulval

Proof