Theorem coe1tmmul2fv

Description: Function value of a right-multiplication by a term in the shifted domain. (Contributed by Stefan O'Rear, 27-Mar-2015)

	Ref	Expression
Hypotheses	coe1tm.z	$$⊢\underset{\dot{}}{0}=0_R$$
	coe1tm.k	$$⊢K={\mathrm{Base}}_R$$
	coe1tm.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	coe1tm.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	coe1tm.m	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
	coe1tm.n	$$⊢N={\mathrm{mulGrp}}_P$$
	coe1tm.e	$$⊢\underset{\dot{}}{\times }={\cdot }_N$$
	coe1tmmul.b	$$⊢B={\mathrm{Base}}_P$$
	coe1tmmul.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_P$$
	coe1tmmul.u	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
	coe1tmmul.a	$$⊢\phi \to A\in B$$
	coe1tmmul.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	coe1tmmul.c	$$⊢\phi \to C\in K$$
	coe1tmmul.d	$$⊢\phi \to D\in {\mathbb{N}}_0$$
	coe1tmmul2fv.y	$$⊢\phi \to Y\in {\mathbb{N}}_0$$
Assertion	coe1tmmul2fv	$$⊢\phi \to {\mathrm{coe}}_1\left(A\underset{\dot{}}{\bullet }\left(C\underset{\dot{}}{·}\left(D\underset{\dot{}}{\times }X\right)\right)\right)\left(D+Y\right)={\mathrm{coe}}_1\left(A\right)\left(Y\right)\underset{\dot{}}{\times }C$$

Proof

Step	Hyp	Ref	Expression
1		coe1tm.z	$$⊢\underset{\dot{}}{0}=0_R$$
2		coe1tm.k	$$⊢K={\mathrm{Base}}_R$$
3		coe1tm.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
4		coe1tm.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
5		coe1tm.m	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
6		coe1tm.n	$$⊢N={\mathrm{mulGrp}}_P$$
7		coe1tm.e	$$⊢\underset{\dot{}}{\times }={\cdot }_N$$
8		coe1tmmul.b	$$⊢B={\mathrm{Base}}_P$$
9		coe1tmmul.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_P$$
10		coe1tmmul.u	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
11		coe1tmmul.a	$$⊢\phi \to A\in B$$
12		coe1tmmul.r	$$⊢\phi \to R\in \mathrm{Ring}$$
13		coe1tmmul.c	$$⊢\phi \to C\in K$$
14		coe1tmmul.d	$$⊢\phi \to D\in {\mathbb{N}}_0$$
15		coe1tmmul2fv.y	$$⊢\phi \to Y\in {\mathbb{N}}_0$$
16	1 2 3 4 5 6 7 8 9 10 11 12 13 14	coe1tmmul2	$$⊢\phi \to {\mathrm{coe}}_1\left(A\underset{\dot{}}{\bullet }\left(C\underset{\dot{}}{·}\left(D\underset{\dot{}}{\times }X\right)\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{}}{\times }C,\underset{\dot{}}{0}\right)\right)$$
17	16	fveq1d	$$⊢\phi \to {\mathrm{coe}}_1\left(A\underset{\dot{}}{\bullet }\left(C\underset{\dot{}}{·}\left(D\underset{\dot{}}{\times }X\right)\right)\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{}}{\times }C,\underset{\dot{}}{0}\right)\right)\left(D+Y\right)$$
18	14 15	nn0addcld	$$⊢\phi \to D+Y\in {\mathbb{N}}_0$$
19		breq2	$$⊢x=D+Y\to \left(D\le x\leftrightarrow D\le D+Y\right)$$
20		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)$$
21	20	oveq1d	$$⊢x=D+Y\to {\mathrm{coe}}_1\left(A\right)\left(x-D\right)\underset{\dot{}}{\times }C={\mathrm{coe}}_1\left(A\right)\left(D+Y-D\right)\underset{\dot{}}{\times }C$$
22	19 21	ifbieq1d	$$⊢x=D+Y\to if\left(D\le x,{\mathrm{coe}}_1\left(A\right)\left(x-D\right)\underset{\dot{}}{\times }C,\underset{\dot{}}{0}\right)=if\left(D\le D+Y,{\mathrm{coe}}_1\left(A\right)\left(D+Y-D\right)\underset{\dot{}}{\times }C,\underset{\dot{}}{0}\right)$$
23		eqid	$$⊢\left(x\in {\mathbb{N}}_0⟼if\left(D\le x,{\mathrm{coe}}_1\left(A\right)\left(x-D\right)\underset{\dot{}}{\times }C,\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{}}{\times }C,\underset{\dot{}}{0}\right)\right)$$
24		ovex	$$⊢{\mathrm{coe}}_1\left(A\right)\left(D+Y-D\right)\underset{\dot{}}{\times }C\in \mathrm{V}$$
25	1	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
26	24 25	ifex	$$⊢if\left(D\le D+Y,{\mathrm{coe}}_1\left(A\right)\left(D+Y-D\right)\underset{\dot{}}{\times }C,\underset{\dot{}}{0}\right)\in \mathrm{V}$$
27	22 23 26	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{}}{\times }C,\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{}}{\times }C,\underset{\dot{}}{0}\right)$$
28	18 27	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{}}{\times }C,\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{}}{\times }C,\underset{\dot{}}{0}\right)$$
29	14	nn0red	$$⊢\phi \to D\in ℝ$$
30		nn0addge1	$$⊢\left(D\in ℝ\wedge Y\in {\mathbb{N}}_0\right)\to D\le D+Y$$
31	29 15 30	syl2anc	$$⊢\phi \to D\le D+Y$$
32	31	iftrued	$$⊢\phi \to if\left(D\le D+Y,{\mathrm{coe}}_1\left(A\right)\left(D+Y-D\right)\underset{\dot{}}{\times }C,\underset{\dot{}}{0}\right)={\mathrm{coe}}_1\left(A\right)\left(D+Y-D\right)\underset{\dot{}}{\times }C$$
33	14	nn0cnd	$$⊢\phi \to D\in ℂ$$
34	15	nn0cnd	$$⊢\phi \to Y\in ℂ$$
35	33 34	pncan2d	$$⊢\phi \to D+Y-D=Y$$
36	35	fveq2d	$$⊢\phi \to {\mathrm{coe}}_1\left(A\right)\left(D+Y-D\right)={\mathrm{coe}}_1\left(A\right)\left(Y\right)$$
37	36	oveq1d	$$⊢\phi \to {\mathrm{coe}}_1\left(A\right)\left(D+Y-D\right)\underset{\dot{}}{\times }C={\mathrm{coe}}_1\left(A\right)\left(Y\right)\underset{\dot{}}{\times }C$$
38	28 32 37	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{}}{\times }C,\underset{\dot{}}{0}\right)\right)\left(D+Y\right)={\mathrm{coe}}_1\left(A\right)\left(Y\right)\underset{\dot{}}{\times }C$$
39	17 38	eqtrd	$$⊢\phi \to {\mathrm{coe}}_1\left(A\underset{\dot{}}{\bullet }\left(C\underset{\dot{}}{·}\left(D\underset{\dot{}}{\times }X\right)\right)\right)\left(D+Y\right)={\mathrm{coe}}_1\left(A\right)\left(Y\right)\underset{\dot{}}{\times }C$$