uc1pldg

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

Step	Hyp	Ref	Expression
1		uc1pldg.d	$⊢ D = \deg_{1} (R)$
2		uc1pldg.u	$⊢ U = Unit (R)$
3		uc1pldg.c	$⊢ C = {Unic}_{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	isuc1p	$⊢ F \in C \leftrightarrow (F \in {Base}_{{Poly}_{1} (R)} \land F \neq 0_{{Poly}_{1} (R)} \land {coe}_{1} (F) (D (F)) \in U)$
8	7	simp3bi	$⊢ F \in C \to {coe}_{1} (F) (D (F)) \in U$

Metamath Proof Explorer