Metamath Proof Explorer


Theorem mncply

Description: A monic polynomial is a polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014)

Ref Expression
Assertion mncply ( 𝑃 ∈ ( Monic ‘ 𝑆 ) → 𝑃 ∈ ( Poly ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 elmnc ( 𝑃 ∈ ( Monic ‘ 𝑆 ) ↔ ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) = 1 ) )
2 1 simplbi ( 𝑃 ∈ ( Monic ‘ 𝑆 ) → 𝑃 ∈ ( Poly ‘ 𝑆 ) )