Step |
Hyp |
Ref |
Expression |
1 |
|
vr1cl.x |
|- X = ( var1 ` R ) |
2 |
|
vr1cl.p |
|- P = ( Poly1 ` R ) |
3 |
|
vr1cl.b |
|- B = ( Base ` P ) |
4 |
1
|
vr1val |
|- X = ( ( 1o mVar R ) ` (/) ) |
5 |
|
eqid |
|- ( 1o mPoly R ) = ( 1o mPoly R ) |
6 |
|
eqid |
|- ( 1o mVar R ) = ( 1o mVar R ) |
7 |
2 3
|
ply1bas |
|- B = ( Base ` ( 1o mPoly R ) ) |
8 |
|
1onn |
|- 1o e. _om |
9 |
8
|
a1i |
|- ( R e. Ring -> 1o e. _om ) |
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
|
mvrcl |
|- ( R e. Ring -> ( ( 1o mVar R ) ` (/) ) e. B ) |
14 |
4 13
|
eqeltrid |
|- ( R e. Ring -> X e. B ) |