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

Metamath Proof Explorer

Theorem vr1cl2

Description: The variable X is a member of the power series algebra R [ [ X ] ] . (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypotheses vr1val.1 
|- X = ( var1 ` R )
vr1cl2.2 
|- S = ( PwSer1 ` R )
vr1cl2.3 
|- B = ( Base ` S )
Assertion vr1cl2 
|- ( R e. Ring -> X e. B )

Proof

Step Hyp Ref Expression
1 vr1val.1 
 |-  X = ( var1 ` R )
2 vr1cl2.2 
 |-  S = ( PwSer1 ` R )
3 vr1cl2.3 
 |-  B = ( Base ` S )
4 1 vr1val 
 |-  X = ( ( 1o mVar R ) ` (/) )
5 eqid 
 |-  ( 1o mPwSer R ) = ( 1o mPwSer R )
6 eqid 
 |-  ( 1o mVar R ) = ( 1o mVar R )
7 eqid 
 |-  ( Base ` ( 1o mPwSer R ) ) = ( Base ` ( 1o mPwSer R ) )
8 1on 
 |-  1o e. On
9 8 a1i 
 |-  ( R e. Ring -> 1o e. On )
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 mvrcl2 
 |-  ( R e. Ring -> ( ( 1o mVar R ) ` (/) ) e. ( Base ` ( 1o mPwSer R ) ) )
14 2 psr1val 
 |-  S = ( ( 1o ordPwSer R ) ` (/) )
15 0ss 
 |-  (/) C_ ( 1o X. 1o )
16 15 a1i 
 |-  ( R e. Ring -> (/) C_ ( 1o X. 1o ) )
17 5 14 16 opsrbas 
 |-  ( R e. Ring -> ( Base ` ( 1o mPwSer R ) ) = ( Base ` S ) )
18 17 3 eqtr4di 
 |-  ( R e. Ring -> ( Base ` ( 1o mPwSer R ) ) = B )
19 13 18 eleqtrd 
 |-  ( R e. Ring -> ( ( 1o mVar R ) ` (/) ) e. B )
20 4 19 eqeltrid 
 |-  ( R e. Ring -> X e. B )