Theorem uc1pcl

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

	Ref	Expression
Hypotheses	uc1pcl.p	|- P = ( Poly1 ` R )
	uc1pcl.b	|- B = ( Base ` P )
	uc1pcl.c	|- C = ( Unic1p ` R )
Assertion	uc1pcl	|- ( F e. C -> F e. B )

Proof

Step	Hyp	Ref	Expression
1		uc1pcl.p	|- P = ( Poly1 ` R )
2		uc1pcl.b	|- B = ( Base ` P )
3		uc1pcl.c	|- C = ( Unic1p ` R )
4		eqid	|- ( 0g ` P ) = ( 0g ` P )
5		eqid	|- ( deg1 ` R ) = ( deg1 ` R )
6		eqid	|- ( Unit ` R ) = ( Unit ` R )
7	1 2 4 5 3 6	isuc1p	|- ( F e. C <-> ( F e. B /\ F =/= ( 0g ` P ) /\ ( ( coe1 ` F ) ` ( ( deg1 ` R ) ` F ) ) e. ( Unit ` R ) ) )
8	7	simp1bi	|- ( F e. C -> F e. B )