Theorem 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={\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	coe1sclmul	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\wedge Y\in B\right)\to {\mathrm{coe}}_1\left(A\left(X\right)\underset{\dot{}}{\bullet }Y\right)=\left({\mathbb{N}}_0\times \left\{X\right\}\right){\underset{\dot{}}{·}}_f{\mathrm{coe}}_1\left(Y\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	coe1tmmul	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\wedge Y\in B\right)\to {\mathrm{coe}}_1\left(\left(X{\cdot }_P\left(0{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)\right)\underset{\dot{}}{\bullet }Y\right)=\left(x\in {\mathbb{N}}_0⟼if\left(0\le x,X\underset{\dot{}}{·}{\mathrm{coe}}_1\left(Y\right)\left(x-0\right),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	fvoveq1d	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\wedge Y\in B\right)\to {\mathrm{coe}}_1\left(A\left(X\right)\underset{\dot{}}{\bullet }Y\right)={\mathrm{coe}}_1\left(\left(X{\cdot }_P\left(0{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)\right)\underset{\dot{}}{\bullet }Y\right)$$
21		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
22	21	a1i	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\wedge Y\in B\right)\to {\mathbb{N}}_0\in \mathrm{V}$$
23		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$$
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		fconstmpt	$$⊢{\mathbb{N}}_0\times \left\{X\right\}=\left(x\in {\mathbb{N}}_0⟼X\right)$$
26	25	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)$$
27		eqid	$$⊢{\mathrm{coe}}_1\left(Y\right)={\mathrm{coe}}_1\left(Y\right)$$
28	27 2 1 3	coe1f	$$⊢Y\in B\to {\mathrm{coe}}_1\left(Y\right):{\mathbb{N}}_0⟶K$$
29	28	3ad2ant3	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\wedge Y\in B\right)\to {\mathrm{coe}}_1\left(Y\right):{\mathbb{N}}_0⟶K$$
30	29	feqmptd	$$⊢\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)$$
31	22 23 24 26 30	offval2	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\wedge Y\in B\right)\to \left({\mathbb{N}}_0\times \left\{X\right\}\right){\underset{\dot{}}{·}}_f{\mathrm{coe}}_1\left(Y\right)=\left(x\in {\mathbb{N}}_0⟼X\underset{\dot{}}{·}{\mathrm{coe}}_1\left(Y\right)\left(x\right)\right)$$
32		nn0ge0	$$⊢x\in {\mathbb{N}}_0\to 0\le x$$
33	32	iftrued	$$⊢x\in {\mathbb{N}}_0\to if\left(0\le x,X\underset{\dot{}}{·}{\mathrm{coe}}_1\left(Y\right)\left(x-0\right),0_R\right)=X\underset{\dot{}}{·}{\mathrm{coe}}_1\left(Y\right)\left(x-0\right)$$
34		nn0cn	$$⊢x\in {\mathbb{N}}_0\to x\in ℂ$$
35	34	subid1d	$$⊢x\in {\mathbb{N}}_0\to x-0=x$$
36	35	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)$$
37	36	oveq2d	$$⊢x\in {\mathbb{N}}_0\to X\underset{\dot{}}{·}{\mathrm{coe}}_1\left(Y\right)\left(x-0\right)=X\underset{\dot{}}{·}{\mathrm{coe}}_1\left(Y\right)\left(x\right)$$
38	33 37	eqtrd	$$⊢x\in {\mathbb{N}}_0\to if\left(0\le x,X\underset{\dot{}}{·}{\mathrm{coe}}_1\left(Y\right)\left(x-0\right),0_R\right)=X\underset{\dot{}}{·}{\mathrm{coe}}_1\left(Y\right)\left(x\right)$$
39	38	mpteq2ia	$$⊢\left(x\in {\mathbb{N}}_0⟼if\left(0\le x,X\underset{\dot{}}{·}{\mathrm{coe}}_1\left(Y\right)\left(x-0\right),0_R\right)\right)=\left(x\in {\mathbb{N}}_0⟼X\underset{\dot{}}{·}{\mathrm{coe}}_1\left(Y\right)\left(x\right)\right)$$
40	31 39	syl6eqr	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\wedge Y\in B\right)\to \left({\mathbb{N}}_0\times \left\{X\right\}\right){\underset{\dot{}}{·}}_f{\mathrm{coe}}_1\left(Y\right)=\left(x\in {\mathbb{N}}_0⟼if\left(0\le x,X\underset{\dot{}}{·}{\mathrm{coe}}_1\left(Y\right)\left(x-0\right),0_R\right)\right)$$
41	17 20 40	3eqtr4d	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\wedge Y\in B\right)\to {\mathrm{coe}}_1\left(A\left(X\right)\underset{\dot{}}{\bullet }Y\right)=\left({\mathbb{N}}_0\times \left\{X\right\}\right){\underset{\dot{}}{·}}_f{\mathrm{coe}}_1\left(Y\right)$$