mon1pldg

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

Step	Hyp	Ref	Expression
1		mon1pldg.d	$⊢ D = \deg_{1} (R)$
2		mon1pldg.o	$⊢ \underset{˙}{1} = 1_{R}$
3		mon1pldg.m	$⊢ M = {Monic}_{1p} (R)$
4		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
5		eqid	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{{Poly}_{1} (R)}$
6		eqid	$⊢ 0_{{Poly}_{1} (R)} = 0_{{Poly}_{1} (R)}$
7	4 5 6 1 3 2	ismon1p	$⊢ F \in M \leftrightarrow (F \in {Base}_{{Poly}_{1} (R)} \land F \neq 0_{{Poly}_{1} (R)} \land {coe}_{1} (F) (D (F)) = \underset{˙}{1})$
8	7	simp3bi	$⊢ F \in M \to {coe}_{1} (F) (D (F)) = \underset{˙}{1}$

Metamath Proof Explorer