Theorem coe1tmfv2

Description: Zero 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$$
	coe1tmfv2.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	coe1tmfv2.c	$$⊢\phi \to C\in K$$
	coe1tmfv2.d	$$⊢\phi \to D\in {\mathbb{N}}_0$$
	coe1tmfv2.f	$$⊢\phi \to F\in {\mathbb{N}}_0$$
	coe1tmfv2.q	$$⊢\phi \to D\ne F$$
Assertion	coe1tmfv2	$$⊢\phi \to {\mathrm{coe}}_1\left(C\underset{\dot{}}{·}\left(D\underset{\dot{}}{\times }X\right)\right)\left(F\right)=\underset{\dot{}}{0}$$

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		coe1tmfv2.r	$$⊢\phi \to R\in \mathrm{Ring}$$
9		coe1tmfv2.c	$$⊢\phi \to C\in K$$
10		coe1tmfv2.d	$$⊢\phi \to D\in {\mathbb{N}}_0$$
11		coe1tmfv2.f	$$⊢\phi \to F\in {\mathbb{N}}_0$$
12		coe1tmfv2.q	$$⊢\phi \to D\ne F$$
13	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)$$
14	8 9 10 13	syl3anc	$$⊢\phi \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)$$
15	14	fveq1d	$$⊢\phi \to {\mathrm{coe}}_1\left(C\underset{\dot{}}{·}\left(D\underset{\dot{}}{\times }X\right)\right)\left(F\right)=\left(x\in {\mathbb{N}}_0⟼if\left(x=D,C,\underset{\dot{}}{0}\right)\right)\left(F\right)$$
16		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)$$
17		eqeq1	$$⊢x=F\to \left(x=D\leftrightarrow F=D\right)$$
18	17	ifbid	$$⊢x=F\to if\left(x=D,C,\underset{\dot{}}{0}\right)=if\left(F=D,C,\underset{\dot{}}{0}\right)$$
19	2 1	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in K$$
20	8 19	syl	$$⊢\phi \to \underset{\dot{}}{0}\in K$$
21	9 20	ifcld	$$⊢\phi \to if\left(F=D,C,\underset{\dot{}}{0}\right)\in K$$
22	16 18 11 21	fvmptd3	$$⊢\phi \to \left(x\in {\mathbb{N}}_0⟼if\left(x=D,C,\underset{\dot{}}{0}\right)\right)\left(F\right)=if\left(F=D,C,\underset{\dot{}}{0}\right)$$
23	12	necomd	$$⊢\phi \to F\ne D$$
24	23	neneqd	$$⊢\phi \to \neg F=D$$
25	24	iffalsed	$$⊢\phi \to if\left(F=D,C,\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
26	15 22 25	3eqtrd	$$⊢\phi \to {\mathrm{coe}}_1\left(C\underset{\dot{}}{·}\left(D\underset{\dot{}}{\times }X\right)\right)\left(F\right)=\underset{\dot{}}{0}$$