Theorem uc1pldg

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

	Ref	Expression
Hypotheses	uc1pldg.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	uc1pldg.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	uc1pldg.c	⊢ 𝐶 = ( Unic1p ‘ 𝑅 )
Assertion	uc1pldg	⊢ ( 𝐹 ∈ 𝐶 → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		uc1pldg.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		uc1pldg.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
3		uc1pldg.c	⊢ 𝐶 = ( Unic1p ‘ 𝑅 )
4		eqid	⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
5		eqid	⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
6		eqid	⊢ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) = ( 0g ‘ ( Poly1 ‘ 𝑅 ) )
7	4 5 6 1 3 2	isuc1p	⊢ ( 𝐹 ∈ 𝐶 ↔ ( 𝐹 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ 𝐹 ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) ∧ ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝑈 ) )
8	7	simp3bi	⊢ ( 𝐹 ∈ 𝐶 → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝑈 )