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	syl5eq	|- ( 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 ) ` (/) )