This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )