Theorem mon1pcl

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

	Ref	Expression
Hypotheses	uc1pcl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	uc1pcl.b	$$⊢B={\mathrm{Base}}_P$$
	mon1pcl.m	$$⊢M={Monic}_{\mathrm{1p}}\left(R\right)$$
Assertion	mon1pcl	$$⊢F\in M\to F\in B$$

Proof

Step	Hyp	Ref	Expression
1		uc1pcl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		uc1pcl.b	$$⊢B={\mathrm{Base}}_P$$
3		mon1pcl.m	$$⊢M={Monic}_{\mathrm{1p}}\left(R\right)$$
4		eqid	$$⊢0_P=0_P$$
5		eqid	$$⊢{\mathrm{deg}}_1\left(R\right)={\mathrm{deg}}_1\left(R\right)$$
6		eqid	$$⊢1_R=1_R$$
7	1 2 4 5 3 6	ismon1p	$$⊢F\in M\leftrightarrow \left(F\in B\wedge F\ne 0_P\wedge {\mathrm{coe}}_1\left(F\right)\left({\mathrm{deg}}_1\left(R\right)\left(F\right)\right)=1_R\right)$$
8	7	simp1bi	$$⊢F\in M\to F\in B$$