Theorem uc1pn0

Description: Unitic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	uc1pn0.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	uc1pn0.z	$$⊢\underset{\dot{}}{0}=0_P$$
	uc1pn0.c	$$⊢C={Unic}_{\mathrm{1p}}\left(R\right)$$
Assertion	uc1pn0	$$⊢F\in C\to F\ne \underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		uc1pn0.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		uc1pn0.z	$$⊢\underset{\dot{}}{0}=0_P$$
3		uc1pn0.c	$$⊢C={Unic}_{\mathrm{1p}}\left(R\right)$$
4		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
5		eqid	$$⊢{\mathrm{deg}}_1\left(R\right)={\mathrm{deg}}_1\left(R\right)$$
6		eqid	$$⊢\mathrm{Unit}\left(R\right)=\mathrm{Unit}\left(R\right)$$
7	1 4 2 5 3 6	isuc1p	$$⊢F\in C\leftrightarrow \left(F\in {\mathrm{Base}}_P\wedge F\ne \underset{\dot{}}{0}\wedge {\mathrm{coe}}_1\left(F\right)\left({\mathrm{deg}}_1\left(R\right)\left(F\right)\right)\in \mathrm{Unit}\left(R\right)\right)$$
8	7	simp2bi	$$⊢F\in C\to F\ne \underset{\dot{}}{0}$$