Theorem coe1pwmul

Description: Coefficient vector of a polynomial multiplied on the left by a variable power. (Contributed by Stefan O'Rear, 1-Apr-2015)

	Ref	Expression
Hypotheses	coe1pwmul.z	$$⊢\underset{\dot{}}{0}=0_R$$
	coe1pwmul.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	coe1pwmul.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	coe1pwmul.n	$$⊢N={\mathrm{mulGrp}}_P$$
	coe1pwmul.e	$$⊢\underset{\dot{}}{\times }={\cdot }_N$$
	coe1pwmul.b	$$⊢B={\mathrm{Base}}_P$$
	coe1pwmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
	coe1pwmul.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	coe1pwmul.a	$$⊢\phi \to A\in B$$
	coe1pwmul.d	$$⊢\phi \to D\in {\mathbb{N}}_0$$
Assertion	coe1pwmul	$$⊢\phi \to {\mathrm{coe}}_1\left(\left(D\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}A\right)=\left(x\in {\mathbb{N}}_0⟼if\left(D\le x,{\mathrm{coe}}_1\left(A\right)\left(x-D\right),\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		coe1pwmul.z	$$⊢\underset{\dot{}}{0}=0_R$$
2		coe1pwmul.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		coe1pwmul.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
4		coe1pwmul.n	$$⊢N={\mathrm{mulGrp}}_P$$
5		coe1pwmul.e	$$⊢\underset{\dot{}}{\times }={\cdot }_N$$
6		coe1pwmul.b	$$⊢B={\mathrm{Base}}_P$$
7		coe1pwmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
8		coe1pwmul.r	$$⊢\phi \to R\in \mathrm{Ring}$$
9		coe1pwmul.a	$$⊢\phi \to A\in B$$
10		coe1pwmul.d	$$⊢\phi \to D\in {\mathbb{N}}_0$$
11		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
12		eqid	$$⊢{\cdot }_P={\cdot }_P$$
13		eqid	$$⊢{\cdot }_R={\cdot }_R$$
14		eqid	$$⊢1_R=1_R$$
15	11 14	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in {\mathrm{Base}}_R$$
16	8 15	syl	$$⊢\phi \to 1_R\in {\mathrm{Base}}_R$$
17	1 11 2 3 12 4 5 6 7 13 9 8 16 10	coe1tmmul	$$⊢\phi \to {\mathrm{coe}}_1\left(\left(1_R{\cdot }_P\left(D\underset{\dot{}}{\times }X\right)\right)\underset{\dot{}}{·}A\right)=\left(x\in {\mathbb{N}}_0⟼if\left(D\le x,1_R{\cdot }_R{\mathrm{coe}}_1\left(A\right)\left(x-D\right),\underset{\dot{}}{0}\right)\right)$$
18	2	ply1sca	$$⊢R\in \mathrm{Ring}\to R=\mathrm{Scalar}\left(P\right)$$
19	8 18	syl	$$⊢\phi \to R=\mathrm{Scalar}\left(P\right)$$
20	19	fveq2d	$$⊢\phi \to 1_R=1_{\mathrm{Scalar}\left(P\right)}$$
21	20	oveq1d	$$⊢\phi \to 1_R{\cdot }_P\left(D\underset{\dot{}}{\times }X\right)=1_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\left(D\underset{\dot{}}{\times }X\right)$$
22	2	ply1lmod	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{LMod}$$
23	8 22	syl	$$⊢\phi \to P\in \mathrm{LMod}$$
24	4 6	mgpbas	$$⊢B={\mathrm{Base}}_N$$
25	2	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
26	4	ringmgp	$$⊢P\in \mathrm{Ring}\to N\in \mathrm{Mnd}$$
27	8 25 26	3syl	$$⊢\phi \to N\in \mathrm{Mnd}$$
28	3 2 6	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in B$$
29	8 28	syl	$$⊢\phi \to X\in B$$
30	24 5 27 10 29	mulgnn0cld	$$⊢\phi \to D\underset{\dot{}}{\times }X\in B$$
31		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
32		eqid	$$⊢1_{\mathrm{Scalar}\left(P\right)}=1_{\mathrm{Scalar}\left(P\right)}$$
33	6 31 12 32	lmodvs1	$$⊢\left(P\in \mathrm{LMod}\wedge D\underset{\dot{}}{\times }X\in B\right)\to 1_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\left(D\underset{\dot{}}{\times }X\right)=D\underset{\dot{}}{\times }X$$
34	23 30 33	syl2anc	$$⊢\phi \to 1_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\left(D\underset{\dot{}}{\times }X\right)=D\underset{\dot{}}{\times }X$$
35	21 34	eqtrd	$$⊢\phi \to 1_R{\cdot }_P\left(D\underset{\dot{}}{\times }X\right)=D\underset{\dot{}}{\times }X$$
36	35	fvoveq1d	$$⊢\phi \to {\mathrm{coe}}_1\left(\left(1_R{\cdot }_P\left(D\underset{\dot{}}{\times }X\right)\right)\underset{\dot{}}{·}A\right)={\mathrm{coe}}_1\left(\left(D\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}A\right)$$
37	8	ad2antrr	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge D\le x\right)\to R\in \mathrm{Ring}$$
38		eqid	$$⊢{\mathrm{coe}}_1\left(A\right)={\mathrm{coe}}_1\left(A\right)$$
39	38 6 2 11	coe1f	$$⊢A\in B\to {\mathrm{coe}}_1\left(A\right):{\mathbb{N}}_0⟶{\mathrm{Base}}_R$$
40	9 39	syl	$$⊢\phi \to {\mathrm{coe}}_1\left(A\right):{\mathbb{N}}_0⟶{\mathrm{Base}}_R$$
41	40	ad2antrr	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge D\le x\right)\to {\mathrm{coe}}_1\left(A\right):{\mathbb{N}}_0⟶{\mathrm{Base}}_R$$
42	10	ad2antrr	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge D\le x\right)\to D\in {\mathbb{N}}_0$$
43		simplr	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge D\le x\right)\to x\in {\mathbb{N}}_0$$
44		simpr	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge D\le x\right)\to D\le x$$
45		nn0sub2	$$⊢\left(D\in {\mathbb{N}}_0\wedge x\in {\mathbb{N}}_0\wedge D\le x\right)\to x-D\in {\mathbb{N}}_0$$
46	42 43 44 45	syl3anc	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge D\le x\right)\to x-D\in {\mathbb{N}}_0$$
47	41 46	ffvelcdmd	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge D\le x\right)\to {\mathrm{coe}}_1\left(A\right)\left(x-D\right)\in {\mathrm{Base}}_R$$
48	11 13 14	ringlidm	$$⊢\left(R\in \mathrm{Ring}\wedge {\mathrm{coe}}_1\left(A\right)\left(x-D\right)\in {\mathrm{Base}}_R\right)\to 1_R{\cdot }_R{\mathrm{coe}}_1\left(A\right)\left(x-D\right)={\mathrm{coe}}_1\left(A\right)\left(x-D\right)$$
49	37 47 48	syl2anc	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge D\le x\right)\to 1_R{\cdot }_R{\mathrm{coe}}_1\left(A\right)\left(x-D\right)={\mathrm{coe}}_1\left(A\right)\left(x-D\right)$$
50	49	ifeq1da	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to if\left(D\le x,1_R{\cdot }_R{\mathrm{coe}}_1\left(A\right)\left(x-D\right),\underset{\dot{}}{0}\right)=if\left(D\le x,{\mathrm{coe}}_1\left(A\right)\left(x-D\right),\underset{\dot{}}{0}\right)$$
51	50	mpteq2dva	$$⊢\phi \to \left(x\in {\mathbb{N}}_0⟼if\left(D\le x,1_R{\cdot }_R{\mathrm{coe}}_1\left(A\right)\left(x-D\right),\underset{\dot{}}{0}\right)\right)=\left(x\in {\mathbb{N}}_0⟼if\left(D\le x,{\mathrm{coe}}_1\left(A\right)\left(x-D\right),\underset{\dot{}}{0}\right)\right)$$
52	17 36 51	3eqtr3d	$$⊢\phi \to {\mathrm{coe}}_1\left(\left(D\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}A\right)=\left(x\in {\mathbb{N}}_0⟼if\left(D\le x,{\mathrm{coe}}_1\left(A\right)\left(x-D\right),\underset{\dot{}}{0}\right)\right)$$