Metamath Proof Explorer


Theorem uc1pn0

Description: Unitic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses uc1pn0.p 𝑃 = ( Poly1𝑅 )
uc1pn0.z 0 = ( 0g𝑃 )
uc1pn0.c 𝐶 = ( Unic1p𝑅 )
Assertion uc1pn0 ( 𝐹𝐶𝐹0 )

Proof

Step Hyp Ref Expression
1 uc1pn0.p 𝑃 = ( Poly1𝑅 )
2 uc1pn0.z 0 = ( 0g𝑃 )
3 uc1pn0.c 𝐶 = ( Unic1p𝑅 )
4 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
5 eqid ( deg1𝑅 ) = ( deg1𝑅 )
6 eqid ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
7 1 4 2 5 3 6 isuc1p ( 𝐹𝐶 ↔ ( 𝐹 ∈ ( Base ‘ 𝑃 ) ∧ 𝐹0 ∧ ( ( coe1𝐹 ) ‘ ( ( deg1𝑅 ) ‘ 𝐹 ) ) ∈ ( Unit ‘ 𝑅 ) ) )
8 7 simp2bi ( 𝐹𝐶𝐹0 )