Description: Define the base element of a univariate power series (the X element of the set R [ X ] of polynomials and also the X in the set R [ [ X ] ] of power series). (Contributed by Mario Carneiro, 8-Feb-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-vr1 | |- var1 = ( r e. _V |-> ( ( 1o mVar r ) ` (/) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cv1 | |- var1 |
|
| 1 | vr | |- r |
|
| 2 | cvv | |- _V |
|
| 3 | c1o | |- 1o |
|
| 4 | cmvr | |- mVar |
|
| 5 | 1 | cv | |- r |
| 6 | 3 5 4 | co | |- ( 1o mVar r ) |
| 7 | c0 | |- (/) |
|
| 8 | 7 6 | cfv | |- ( ( 1o mVar r ) ` (/) ) |
| 9 | 1 2 8 | cmpt | |- ( r e. _V |-> ( ( 1o mVar r ) ` (/) ) ) |
| 10 | 0 9 | wceq | |- var1 = ( r e. _V |-> ( ( 1o mVar r ) ` (/) ) ) |