Theorem ismon1p

Description: Being a monic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	uc1pval.p	|- P = ( Poly1 ` R )
	uc1pval.b	|- B = ( Base ` P )
	uc1pval.z	|- .0. = ( 0g ` P )
	uc1pval.d	|- D = ( deg1 ` R )
	mon1pval.m	|- M = ( Monic1p ` R )
	mon1pval.o	|- .1. = ( 1r ` R )
Assertion	ismon1p	|- ( F e. M <-> ( F e. B /\ F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) = .1. ) )

Proof

Step	Hyp	Ref	Expression
1		uc1pval.p	|- P = ( Poly1 ` R )
2		uc1pval.b	|- B = ( Base ` P )
3		uc1pval.z	|- .0. = ( 0g ` P )
4		uc1pval.d	|- D = ( deg1 ` R )
5		mon1pval.m	|- M = ( Monic1p ` R )
6		mon1pval.o	|- .1. = ( 1r ` R )
7		neeq1	|- ( f = F -> ( f =/= .0. <-> F =/= .0. ) )
8		fveq2	|- ( f = F -> ( coe1 ` f ) = ( coe1 ` F ) )
9		fveq2	|- ( f = F -> ( D ` f ) = ( D ` F ) )
10	8 9	fveq12d	|- ( f = F -> ( ( coe1 ` f ) ` ( D ` f ) ) = ( ( coe1 ` F ) ` ( D ` F ) ) )
11	10	eqeq1d	|- ( f = F -> ( ( ( coe1 ` f ) ` ( D ` f ) ) = .1. <-> ( ( coe1 ` F ) ` ( D ` F ) ) = .1. ) )
12	7 11	anbi12d	|- ( f = F -> ( ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) = .1. ) <-> ( F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) = .1. ) ) )
13	1 2 3 4 5 6	mon1pval	|- M = { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) = .1. ) }
14	12 13	elrab2	|- ( F e. M <-> ( F e. B /\ ( F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) = .1. ) ) )
15		3anass	|- ( ( F e. B /\ F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) = .1. ) <-> ( F e. B /\ ( F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) = .1. ) ) )
16	14 15	bitr4i	|- ( F e. M <-> ( F e. B /\ F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) = .1. ) )