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	2	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
25	4	ringmgp	$$⊢P\in \mathrm{Ring}\to N\in \mathrm{Mnd}$$
26	8 24 25	3syl	$$⊢\phi \to N\in \mathrm{Mnd}$$
27	3 2 6	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in B$$
28	8 27	syl	$$⊢\phi \to X\in B$$
29	4 6	mgpbas	$$⊢B={\mathrm{Base}}_N$$
30	29 5	mulgnn0cl	$$⊢\left(N\in \mathrm{Mnd}\wedge D\in {\mathbb{N}}_0\wedge X\in B\right)\to D\underset{\dot{}}{\times }X\in B$$
31	26 10 28 30	syl3anc	$$⊢\phi \to D\underset{\dot{}}{\times }X\in B$$
32		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
33		eqid	$$⊢1_{\mathrm{Scalar}\left(P\right)}=1_{\mathrm{Scalar}\left(P\right)}$$
34	6 32 12 33	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$$
35	23 31 34	syl2anc	$$⊢\phi \to 1_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\left(D\underset{\dot{}}{\times }X\right)=D\underset{\dot{}}{\times }X$$
36	21 35	eqtrd	$$⊢\phi \to 1_R{\cdot }_P\left(D\underset{\dot{}}{\times }X\right)=D\underset{\dot{}}{\times }X$$
37	36	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)$$
38	8	ad2antrr	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge D\le x\right)\to R\in \mathrm{Ring}$$
39		eqid	$$⊢{\mathrm{coe}}_1\left(A\right)={\mathrm{coe}}_1\left(A\right)$$
40	39 6 2 11	coe1f	$$⊢A\in B\to {\mathrm{coe}}_1\left(A\right):{\mathbb{N}}_0⟶{\mathrm{Base}}_R$$
41	9 40	syl	$$⊢\phi \to {\mathrm{coe}}_1\left(A\right):{\mathbb{N}}_0⟶{\mathrm{Base}}_R$$
42	41	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$$
43	10	ad2antrr	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge D\le x\right)\to D\in {\mathbb{N}}_0$$
44		simplr	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge D\le x\right)\to x\in {\mathbb{N}}_0$$
45		simpr	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge D\le x\right)\to D\le x$$
46		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$$
47	43 44 45 46	syl3anc	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge D\le x\right)\to x-D\in {\mathbb{N}}_0$$
48	42 47	ffvelrnd	$$⊢\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$$
49	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)$$
50	38 48 49	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)$$
51	50	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)$$
52	51	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)$$
53	17 37 52	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)$$