Theorem mon1pn0

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

	Ref	Expression
Hypotheses	uc1pn0.p	|- P = ( Poly1 ` R )
	uc1pn0.z	|- .0. = ( 0g ` P )
	mon1pn0.m	|- M = ( Monic1p ` R )
Assertion	mon1pn0	|- ( F e. M -> F =/= .0. )

Proof

Step	Hyp	Ref	Expression
1		uc1pn0.p	|- P = ( Poly1 ` R )
2		uc1pn0.z	|- .0. = ( 0g ` P )
3		mon1pn0.m	|- M = ( Monic1p ` R )
4		eqid	|- ( Base ` P ) = ( Base ` P )
5		eqid	|- ( deg1 ` R ) = ( deg1 ` R )
6		eqid	|- ( 1r ` R ) = ( 1r ` R )
7	1 4 2 5 3 6	ismon1p	|- ( F e. M <-> ( F e. ( Base ` P ) /\ F =/= .0. /\ ( ( coe1 ` F ) ` ( ( deg1 ` R ) ` F ) ) = ( 1r ` R ) ) )
8	7	simp2bi	|- ( F e. M -> F =/= .0. )