Theorem coe1sclmul2

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

	Ref	Expression
Hypotheses	coe1sclmul.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	coe1sclmul.b	$$⊢B={\mathrm{Base}}_P$$
	coe1sclmul.k	$$⊢K={\mathrm{Base}}_R$$
	coe1sclmul.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
	coe1sclmul.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_P$$
	coe1sclmul.u	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	coe1sclmul2	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\wedge Y\in B\right)\to {\mathrm{coe}}_1\left(Y\underset{\dot{}}{\bullet }A\left(X\right)\right)={\mathrm{coe}}_1\left(Y\right){\underset{\dot{}}{·}}_f\left({\mathbb{N}}_0\times \left\{X\right\}\right)$$

Proof

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