MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vr1val Structured version   Unicode version

Theorem vr1val 17741
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.)
Hypothesis
Ref Expression
vr1val.1  |-  X  =  (var1 `  R )
Assertion
Ref Expression
vr1val  |-  X  =  ( ( 1o mVar  R
) `  (/) )

Proof of Theorem vr1val
Dummy variables  f  h  i  r  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vr1val.1 . . 3  |-  X  =  (var1 `  R )
2 oveq2 6184 . . . . 5  |-  ( r  =  R  ->  ( 1o mVar  r )  =  ( 1o mVar  R ) )
32fveq1d 5777 . . . 4  |-  ( r  =  R  ->  (
( 1o mVar  r ) `  (/) )  =  ( ( 1o mVar  R ) `
 (/) ) )
4 df-vr1 17730 . . . 4  |- var1  =  (
r  e.  _V  |->  ( ( 1o mVar  r ) `
 (/) ) )
5 fvex 5785 . . . 4  |-  ( ( 1o mVar  R ) `  (/) )  e.  _V
63, 4, 5fvmpt 5859 . . 3  |-  ( R  e.  _V  ->  (var1 `  R )  =  ( ( 1o mVar  R ) `
 (/) ) )
71, 6syl5eq 2502 . 2  |-  ( R  e.  _V  ->  X  =  ( ( 1o mVar  R ) `  (/) ) )
8 fvprc 5769 . . . 4  |-  ( -.  R  e.  _V  ->  (var1 `  R )  =  (/) )
9 0fv 5808 . . . 4  |-  ( (/) `  (/) )  =  (/)
108, 1, 93eqtr4g 2515 . . 3  |-  ( -.  R  e.  _V  ->  X  =  ( (/) `  (/) ) )
11 df-mvr 17516 . . . . . 6  |- 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 ) ) ) ) )
1211reldmmpt2 6287 . . . . 5  |-  Rel  dom mVar
1312ovprc2 6205 . . . 4  |-  ( -.  R  e.  _V  ->  ( 1o mVar  R )  =  (/) )
1413fveq1d 5777 . . 3  |-  ( -.  R  e.  _V  ->  ( ( 1o mVar  R ) `
 (/) )  =  (
(/) `  (/) ) )
1510, 14eqtr4d 2493 . 2  |-  ( -.  R  e.  _V  ->  X  =  ( ( 1o mVar  R ) `  (/) ) )
167, 15pm2.61i 164 1  |-  X  =  ( ( 1o mVar  R
) `  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1370    e. wcel 1757   {crab 2796   _Vcvv 3054   (/)c0 3721   ifcif 3875    |-> cmpt 4434   `'ccnv 4923   "cima 4927   ` cfv 5502  (class class class)co 6176   1oc1o 6999    ^m cmap 7300   Fincfn 7396   0cc0 9369   1c1 9370   NNcn 10409   NN0cn0 10666   0gc0g 14466   1rcur 16694   mVar cmvr 17511  var1cv1 17725
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-sep 4497  ax-nul 4505  ax-pow 4554  ax-pr 4615
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-rab 2801  df-v 3056  df-sbc 3271  df-dif 3415  df-un 3417  df-in 3419  df-ss 3426  df-nul 3722  df-if 3876  df-sn 3962  df-pr 3964  df-op 3968  df-uni 4176  df-br 4377  df-opab 4435  df-mpt 4436  df-id 4720  df-xp 4930  df-rel 4931  df-cnv 4932  df-co 4933  df-dm 4934  df-iota 5465  df-fun 5504  df-fv 5510  df-ov 6179  df-oprab 6180  df-mpt2 6181  df-mvr 17516  df-vr1 17730
This theorem is referenced by:  vr1cl2  17742  vr1cl  17764  subrgvr1  17808  subrgvr1cl  17809  coe1tm  17820  ply1coe  17841  ply1coeOLD  17842  evl1var  17865  evls1var  17867
  Copyright terms: Public domain W3C validator