Theorem mon1pldg

Description: Unitic polynomials have one leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	mon1pldg.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	mon1pldg.o	$$⊢\underset{\dot{}}{1}=1_R$$
	mon1pldg.m	$$⊢M={Monic}_{\mathrm{1p}}\left(R\right)$$
Assertion	mon1pldg	$$⊢F\in M\to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)=\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		mon1pldg.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
2		mon1pldg.o	$$⊢\underset{\dot{}}{1}=1_R$$
3		mon1pldg.m	$$⊢M={Monic}_{\mathrm{1p}}\left(R\right)$$
4		eqid	$$⊢{\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(R\right)$$
5		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
6		eqid	$$⊢0_{{\mathrm{Poly}}_1\left(R\right)}=0_{{\mathrm{Poly}}_1\left(R\right)}$$
7	4 5 6 1 3 2	ismon1p	$$⊢F\in M\leftrightarrow \left(F\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\wedge F\ne 0_{{\mathrm{Poly}}_1\left(R\right)}\wedge {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)=\underset{\dot{}}{1}\right)$$
8	7	simp3bi	$$⊢F\in M\to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)=\underset{\dot{}}{1}$$