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	2 3	ply1bas	|- B = ( Base ` ( 1o mPoly R ) )
8		1onn	|- 1o e. _om
9	8	a1i	|- ( R e. Ring -> 1o e. _om )
10		id	|- ( R e. Ring -> R e. Ring )
11		0lt1o	|- (/) e. 1o
12	11	a1i	|- ( R e. Ring -> (/) e. 1o )
13	5 6 7 9 10 12	mvrcl	|- ( R e. Ring -> ( ( 1o mVar R ) ` (/) ) e. B )
14	4 13	eqeltrid	|- ( R e. Ring -> X e. B )