Theorem vr1cl

Description: The generator of a univariate polynomial algebra is contained in the base set. (Contributed by Stefan O'Rear, 19-Mar-2015)

	Ref	Expression
Hypotheses	vr1cl.x	|- X = ( var1 ` R )
	vr1cl.p	|- P = ( Poly1 ` R )
	vr1cl.b	|- B = ( Base ` P )
Assertion	vr1cl	|- ( R e. Ring -> X e. B )

Proof

Step	Hyp	Ref	Expression
1		vr1cl.x	|- X = ( var1 ` R )
2		vr1cl.p	|- P = ( Poly1 ` R )
3		vr1cl.b	|- B = ( Base ` P )
4	1	vr1val	|- X = ( ( 1o mVar R ) ` (/) )
5		eqid	|- ( 1o mPoly R ) = ( 1o mPoly R )
6		eqid	|- ( 1o mVar R ) = ( 1o mVar R )
7		eqid	|- ( PwSer1 ` R ) = ( PwSer1 ` R )
8	2 7 3	ply1bas	|- B = ( Base ` ( 1o mPoly R ) )
9		1onn	|- 1o e. _om
10	9	a1i	|- ( R e. Ring -> 1o e. _om )
11		id	|- ( R e. Ring -> R e. Ring )
12		0lt1o	|- (/) e. 1o
13	12	a1i	|- ( R e. Ring -> (/) e. 1o )
14	5 6 8 10 11 13	mvrcl	|- ( R e. Ring -> ( ( 1o mVar R ) ` (/) ) e. B )
15	4 14	eqeltrid	|- ( R e. Ring -> X e. B )