Theorem mncn0

Description: A monic polynomial is not zero. (Contributed by Stefan O'Rear, 5-Dec-2014)

	Ref	Expression
Assertion	mncn0	$$⊢P\in \mathrm{Monic}\left(S\right)\to P\ne 0_{𝑝}$$

Proof

Step	Hyp	Ref	Expression
1		mnccoe	$$⊢P\in \mathrm{Monic}\left(S\right)\to \mathrm{coeff}\left(P\right)\left(\mathrm{deg}\left(P\right)\right)=1$$
2		coe0	$$⊢\mathrm{coeff}\left(0_{𝑝}\right)={\mathbb{N}}_0\times \left\{0\right\}$$
3	2	fveq1i	$$⊢\mathrm{coeff}\left(0_{𝑝}\right)\left(\mathrm{deg}\left(0_{𝑝}\right)\right)=\left({\mathbb{N}}_0\times \left\{0\right\}\right)\left(\mathrm{deg}\left(0_{𝑝}\right)\right)$$
4		dgr0	$$⊢\mathrm{deg}\left(0_{𝑝}\right)=0$$
5		0nn0	$$⊢0\in {\mathbb{N}}_0$$
6	4 5	eqeltri	$$⊢\mathrm{deg}\left(0_{𝑝}\right)\in {\mathbb{N}}_0$$
7		c0ex	$$⊢0\in \mathrm{V}$$
8	7	fvconst2	$$⊢\mathrm{deg}\left(0_{𝑝}\right)\in {\mathbb{N}}_0\to \left({\mathbb{N}}_0\times \left\{0\right\}\right)\left(\mathrm{deg}\left(0_{𝑝}\right)\right)=0$$
9	6 8	ax-mp	$$⊢\left({\mathbb{N}}_0\times \left\{0\right\}\right)\left(\mathrm{deg}\left(0_{𝑝}\right)\right)=0$$
10	3 9	eqtri	$$⊢\mathrm{coeff}\left(0_{𝑝}\right)\left(\mathrm{deg}\left(0_{𝑝}\right)\right)=0$$
11		0ne1	$$⊢0\ne 1$$
12	10 11	eqnetri	$$⊢\mathrm{coeff}\left(0_{𝑝}\right)\left(\mathrm{deg}\left(0_{𝑝}\right)\right)\ne 1$$
13		fveq2	$$⊢P=0_{𝑝}\to \mathrm{coeff}\left(P\right)=\mathrm{coeff}\left(0_{𝑝}\right)$$
14		fveq2	$$⊢P=0_{𝑝}\to \mathrm{deg}\left(P\right)=\mathrm{deg}\left(0_{𝑝}\right)$$
15	13 14	fveq12d	$$⊢P=0_{𝑝}\to \mathrm{coeff}\left(P\right)\left(\mathrm{deg}\left(P\right)\right)=\mathrm{coeff}\left(0_{𝑝}\right)\left(\mathrm{deg}\left(0_{𝑝}\right)\right)$$
16	15	neeq1d	$$⊢P=0_{𝑝}\to \left(\mathrm{coeff}\left(P\right)\left(\mathrm{deg}\left(P\right)\right)\ne 1\leftrightarrow \mathrm{coeff}\left(0_{𝑝}\right)\left(\mathrm{deg}\left(0_{𝑝}\right)\right)\ne 1\right)$$
17	12 16	mpbiri	$$⊢P=0_{𝑝}\to \mathrm{coeff}\left(P\right)\left(\mathrm{deg}\left(P\right)\right)\ne 1$$
18	17	necon2i	$$⊢\mathrm{coeff}\left(P\right)\left(\mathrm{deg}\left(P\right)\right)=1\to P\ne 0_{𝑝}$$
19	1 18	syl	$$⊢P\in \mathrm{Monic}\left(S\right)\to P\ne 0_{𝑝}$$