coe1sclmul

Description: Coefficient vector of a polynomial multiplied on the left by a scalar. (Contributed by Stefan O'Rear, 29-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		coe1sclmul.p	$⊢ P = {Poly}_{1} (R)$
2		coe1sclmul.b	$⊢ B = {Base}_{P}$
3		coe1sclmul.k	$⊢ K = {Base}_{R}$
4		coe1sclmul.a	$⊢ A = algSc (P)$
5		coe1sclmul.t	$⊢ \underset{˙}{∙} = \cdot_{P}$
6		coe1sclmul.u	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
7		eqid	$⊢ 0_{R} = 0_{R}$
8		eqid	$⊢ {var}_{1} (R) = {var}_{1} (R)$
9		eqid	$⊢ \cdot_{P} = \cdot_{P}$
10		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
11		eqid	$⊢ \cdot_{{mulGrp}_{P}} = \cdot_{{mulGrp}_{P}}$
12		simp3	$⊢ (R \in Ring \land X \in K \land Y \in B) \to Y \in B$
13		simp1	$⊢ (R \in Ring \land X \in K \land Y \in B) \to R \in Ring$
14		simp2	$⊢ (R \in Ring \land X \in K \land Y \in B) \to X \in K$
15		0nn0	$⊢ 0 \in ℕ_{0}$
16	15	a1i	$⊢ (R \in Ring \land X \in K \land Y \in B) \to 0 \in ℕ_{0}$
17	7 3 1 8 9 10 11 2 5 6 12 13 14 16	coe1tmmul	$⊢ (R \in Ring \land X \in K \land Y \in B) \to {coe}_{1} ((X \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))) \underset{˙}{∙} Y) = (x \in ℕ_{0} ⟼ if (0 \leq x, X \underset{˙}{\cdot} {coe}_{1} (Y) (x - 0), 0_{R}))$
18	3 1 8 9 10 11 4	ply1scltm	$⊢ (R \in Ring \land X \in K) \to A (X) = X \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))$
19	18	3adant3	$⊢ (R \in Ring \land X \in K \land Y \in B) \to A (X) = X \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))$
20	19	fvoveq1d	$⊢ (R \in Ring \land X \in K \land Y \in B) \to {coe}_{1} (A (X) \underset{˙}{∙} Y) = {coe}_{1} ((X \cdot_{P} (0 \cdot_{{mulGrp}_{P}} {var}_{1} (R))) \underset{˙}{∙} Y)$
21		nn0ex	$⊢ ℕ_{0} \in V$
22	21	a1i	$⊢ (R \in Ring \land X \in K \land Y \in B) \to ℕ_{0} \in V$
23		simpl2	$⊢ ((R \in Ring \land X \in K \land Y \in B) \land x \in ℕ_{0}) \to X \in K$
24		fvexd	$⊢ ((R \in Ring \land X \in K \land Y \in B) \land x \in ℕ_{0}) \to {coe}_{1} (Y) (x) \in V$
25		fconstmpt	$⊢ ℕ_{0} \times \{X\} = (x \in ℕ_{0} ⟼ X)$
26	25	a1i	$⊢ (R \in Ring \land X \in K \land Y \in B) \to ℕ_{0} \times \{X\} = (x \in ℕ_{0} ⟼ X)$
27		eqid	$⊢ {coe}_{1} (Y) = {coe}_{1} (Y)$
28	27 2 1 3	coe1f	$⊢ Y \in B \to {coe}_{1} (Y) : ℕ_{0} ⟶ K$
29	28	3ad2ant3	$⊢ (R \in Ring \land X \in K \land Y \in B) \to {coe}_{1} (Y) : ℕ_{0} ⟶ K$
30	29	feqmptd	$⊢ (R \in Ring \land X \in K \land Y \in B) \to {coe}_{1} (Y) = (x \in ℕ_{0} ⟼ {coe}_{1} (Y) (x))$
31	22 23 24 26 30	offval2	$⊢ (R \in Ring \land X \in K \land Y \in B) \to (ℕ_{0} \times \{X\}) {\underset{˙}{\cdot}}_{f} {coe}_{1} (Y) = (x \in ℕ_{0} ⟼ X \underset{˙}{\cdot} {coe}_{1} (Y) (x))$
32		nn0ge0	$⊢ x \in ℕ_{0} \to 0 \leq x$
33	32	iftrued	$⊢ x \in ℕ_{0} \to if (0 \leq x, X \underset{˙}{\cdot} {coe}_{1} (Y) (x - 0), 0_{R}) = X \underset{˙}{\cdot} {coe}_{1} (Y) (x - 0)$
34		nn0cn	$⊢ x \in ℕ_{0} \to x \in ℂ$
35	34	subid1d	$⊢ x \in ℕ_{0} \to x - 0 = x$
36	35	fveq2d	$⊢ x \in ℕ_{0} \to {coe}_{1} (Y) (x - 0) = {coe}_{1} (Y) (x)$
37	36	oveq2d	$⊢ x \in ℕ_{0} \to X \underset{˙}{\cdot} {coe}_{1} (Y) (x - 0) = X \underset{˙}{\cdot} {coe}_{1} (Y) (x)$
38	33 37	eqtrd	$⊢ x \in ℕ_{0} \to if (0 \leq x, X \underset{˙}{\cdot} {coe}_{1} (Y) (x - 0), 0_{R}) = X \underset{˙}{\cdot} {coe}_{1} (Y) (x)$
39	38	mpteq2ia	$⊢ (x \in ℕ_{0} ⟼ if (0 \leq x, X \underset{˙}{\cdot} {coe}_{1} (Y) (x - 0), 0_{R})) = (x \in ℕ_{0} ⟼ X \underset{˙}{\cdot} {coe}_{1} (Y) (x))$
40	31 39	eqtr4di	$⊢ (R \in Ring \land X \in K \land Y \in B) \to (ℕ_{0} \times \{X\}) {\underset{˙}{\cdot}}_{f} {coe}_{1} (Y) = (x \in ℕ_{0} ⟼ if (0 \leq x, X \underset{˙}{\cdot} {coe}_{1} (Y) (x - 0), 0_{R}))$
41	17 20 40	3eqtr4d	$⊢ (R \in Ring \land X \in K \land Y \in B) \to {coe}_{1} (A (X) \underset{˙}{∙} Y) = (ℕ_{0} \times \{X\}) {\underset{˙}{\cdot}}_{f} {coe}_{1} (Y)$

Metamath Proof Explorer

Theorem coe1sclmul

Proof