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

Metamath Proof Explorer

Theorem vr1val

Description: The value of the generator of the power series algebra (the X in R [ [ X ] ] ). Since all univariate polynomial rings over a fixed base ring R are isomorphic, we don't bother to pass this in as a parameter; internally we are actually using the empty set as this generator and 1o = { (/) } is the index set (but for most purposes this choice should not be visible anyway). (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypothesis vr1val.1 
|- X = ( var1 ` R )
Assertion vr1val 
|- X = ( ( 1o mVar R ) ` (/) )

Proof

Step Hyp Ref Expression
1 vr1val.1 
 |-  X = ( var1 ` R )
2 oveq2 
 |-  ( r = R -> ( 1o mVar r ) = ( 1o mVar R ) )
3 2 fveq1d 
 |-  ( r = R -> ( ( 1o mVar r ) ` (/) ) = ( ( 1o mVar R ) ` (/) ) )
4 df-vr1 
 |-  var1 = ( r e. _V |-> ( ( 1o mVar r ) ` (/) ) )
5 fvex 
 |-  ( ( 1o mVar R ) ` (/) ) e. _V
6 3 4 5 fvmpt 
 |-  ( R e. _V -> ( var1 ` R ) = ( ( 1o mVar R ) ` (/) ) )
7 1 6 eqtrid 
 |-  ( R e. _V -> X = ( ( 1o mVar R ) ` (/) ) )
8 fvprc 
 |-  ( -. R e. _V -> ( var1 ` R ) = (/) )
9 0fv 
 |-  ( (/) ` (/) ) = (/)
10 8 1 9 3eqtr4g 
 |-  ( -. R e. _V -> X = ( (/) ` (/) ) )
11 df-mvr 
 |-  mVar = ( i e. _V , r e. _V |-> ( x e. i |-> ( f e. { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. i |-> if ( y = x , 1 , 0 ) ) , ( 1r ` r ) , ( 0g ` r ) ) ) ) )
12 11 reldmmpo 
 |-  Rel dom mVar
13 12 ovprc2 
 |-  ( -. R e. _V -> ( 1o mVar R ) = (/) )
14 13 fveq1d 
 |-  ( -. R e. _V -> ( ( 1o mVar R ) ` (/) ) = ( (/) ` (/) ) )
15 10 14 eqtr4d 
 |-  ( -. R e. _V -> X = ( ( 1o mVar R ) ` (/) ) )
16 7 15 pm2.61i 
 |-  X = ( ( 1o mVar R ) ` (/) )