Theorem coe1tmfv1

Description: Nonzero coefficient of a polynomial term. (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$$
Assertion	coe1tmfv1	$$⊢\left(R\in \mathrm{Ring}\wedge C\in K\wedge D\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(C\underset{\dot{}}{·}\left(D\underset{\dot{}}{\times }X\right)\right)\left(D\right)=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	1 2 3 4 5 6 7	coe1tm	$$⊢\left(R\in \mathrm{Ring}\wedge C\in K\wedge D\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(C\underset{\dot{}}{·}\left(D\underset{\dot{}}{\times }X\right)\right)=\left(x\in {\mathbb{N}}_0⟼if\left(x=D,C,\underset{\dot{}}{0}\right)\right)$$
9	8	fveq1d	$$⊢\left(R\in \mathrm{Ring}\wedge C\in K\wedge D\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(C\underset{\dot{}}{·}\left(D\underset{\dot{}}{\times }X\right)\right)\left(D\right)=\left(x\in {\mathbb{N}}_0⟼if\left(x=D,C,\underset{\dot{}}{0}\right)\right)\left(D\right)$$
10		eqid	$$⊢\left(x\in {\mathbb{N}}_0⟼if\left(x=D,C,\underset{\dot{}}{0}\right)\right)=\left(x\in {\mathbb{N}}_0⟼if\left(x=D,C,\underset{\dot{}}{0}\right)\right)$$
11		iftrue	$$⊢x=D\to if\left(x=D,C,\underset{\dot{}}{0}\right)=C$$
12		simp3	$$⊢\left(R\in \mathrm{Ring}\wedge C\in K\wedge D\in {\mathbb{N}}_0\right)\to D\in {\mathbb{N}}_0$$
13		simp2	$$⊢\left(R\in \mathrm{Ring}\wedge C\in K\wedge D\in {\mathbb{N}}_0\right)\to C\in K$$
14	10 11 12 13	fvmptd3	$$⊢\left(R\in \mathrm{Ring}\wedge C\in K\wedge D\in {\mathbb{N}}_0\right)\to \left(x\in {\mathbb{N}}_0⟼if\left(x=D,C,\underset{\dot{}}{0}\right)\right)\left(D\right)=C$$
15	9 14	eqtrd	$$⊢\left(R\in \mathrm{Ring}\wedge C\in K\wedge D\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(C\underset{\dot{}}{·}\left(D\underset{\dot{}}{\times }X\right)\right)\left(D\right)=C$$