Theorem coe1pwmulfv

Description: Function value of a right-multiplication by a variable power in the shifted domain. (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$$
	coe1pwmulfv.y	$$⊢\phi \to Y\in {\mathbb{N}}_0$$
Assertion	coe1pwmulfv	$$⊢\phi \to {\mathrm{coe}}_1\left(\left(D\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}A\right)\left(D+Y\right)={\mathrm{coe}}_1\left(A\right)\left(Y\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		coe1pwmulfv.y	$$⊢\phi \to Y\in {\mathbb{N}}_0$$
12	1 2 3 4 5 6 7 8 9 10	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)$$
13	12	fveq1d	$$⊢\phi \to {\mathrm{coe}}_1\left(\left(D\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}A\right)\left(D+Y\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)\left(D+Y\right)$$
14	10 11	nn0addcld	$$⊢\phi \to D+Y\in {\mathbb{N}}_0$$
15		breq2	$$⊢x=D+Y\to \left(D\le x\leftrightarrow D\le D+Y\right)$$
16		fvoveq1	$$⊢x=D+Y\to {\mathrm{coe}}_1\left(A\right)\left(x-D\right)={\mathrm{coe}}_1\left(A\right)\left(D+Y-D\right)$$
17	15 16	ifbieq1d	$$⊢x=D+Y\to if\left(D\le x,{\mathrm{coe}}_1\left(A\right)\left(x-D\right),\underset{\dot{}}{0}\right)=if\left(D\le D+Y,{\mathrm{coe}}_1\left(A\right)\left(D+Y-D\right),\underset{\dot{}}{0}\right)$$
18		eqid	$$⊢\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)=\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)$$
19		fvex	$$⊢{\mathrm{coe}}_1\left(A\right)\left(D+Y-D\right)\in \mathrm{V}$$
20	1	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
21	19 20	ifex	$$⊢if\left(D\le D+Y,{\mathrm{coe}}_1\left(A\right)\left(D+Y-D\right),\underset{\dot{}}{0}\right)\in \mathrm{V}$$
22	17 18 21	fvmpt	$$⊢D+Y\in {\mathbb{N}}_0\to \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)\left(D+Y\right)=if\left(D\le D+Y,{\mathrm{coe}}_1\left(A\right)\left(D+Y-D\right),\underset{\dot{}}{0}\right)$$
23	14 22	syl	$$⊢\phi \to \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)\left(D+Y\right)=if\left(D\le D+Y,{\mathrm{coe}}_1\left(A\right)\left(D+Y-D\right),\underset{\dot{}}{0}\right)$$
24	10	nn0red	$$⊢\phi \to D\in ℝ$$
25		nn0addge1	$$⊢\left(D\in ℝ\wedge Y\in {\mathbb{N}}_0\right)\to D\le D+Y$$
26	24 11 25	syl2anc	$$⊢\phi \to D\le D+Y$$
27	26	iftrued	$$⊢\phi \to if\left(D\le D+Y,{\mathrm{coe}}_1\left(A\right)\left(D+Y-D\right),\underset{\dot{}}{0}\right)={\mathrm{coe}}_1\left(A\right)\left(D+Y-D\right)$$
28	10	nn0cnd	$$⊢\phi \to D\in ℂ$$
29	11	nn0cnd	$$⊢\phi \to Y\in ℂ$$
30	28 29	pncan2d	$$⊢\phi \to D+Y-D=Y$$
31	30	fveq2d	$$⊢\phi \to {\mathrm{coe}}_1\left(A\right)\left(D+Y-D\right)={\mathrm{coe}}_1\left(A\right)\left(Y\right)$$
32	23 27 31	3eqtrd	$$⊢\phi \to \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)\left(D+Y\right)={\mathrm{coe}}_1\left(A\right)\left(Y\right)$$
33	13 32	eqtrd	$$⊢\phi \to {\mathrm{coe}}_1\left(\left(D\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}A\right)\left(D+Y\right)={\mathrm{coe}}_1\left(A\right)\left(Y\right)$$