Metamath Proof Explorer


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𝐹 ) ‘ ( 𝐷𝐹 ) ) ∈ 𝑈 )