Theorem isuc1p

Description: Being a unitic 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 )
	uc1pval.c	|- C = ( Unic1p ` R )
	uc1pval.u	|- U = ( Unit ` R )
Assertion	isuc1p	|- ( F e. C <-> ( F e. B /\ F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) e. U ) )

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		uc1pval.c	|- C = ( Unic1p ` R )
6		uc1pval.u	|- U = ( Unit ` 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	eleq1d	|- ( f = F -> ( ( ( coe1 ` f ) ` ( D ` f ) ) e. U <-> ( ( coe1 ` F ) ` ( D ` F ) ) e. U ) )
12	7 11	anbi12d	|- ( f = F -> ( ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) <-> ( F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) e. U ) ) )
13	1 2 3 4 5 6	uc1pval	|- C = { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) }
14	12 13	elrab2	|- ( F e. C <-> ( F e. B /\ ( F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) e. U ) ) )
15		3anass	|- ( ( F e. B /\ F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) e. U ) <-> ( F e. B /\ ( F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) e. U ) ) )
16	14 15	bitr4i	|- ( F e. C <-> ( F e. B /\ F =/= .0. /\ ( ( coe1 ` F ) ` ( D ` F ) ) e. U ) )