| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ply1vscl.p |
|- P = ( Poly1 ` R ) |
| 2 |
|
ply1vscl.b |
|- B = ( Base ` P ) |
| 3 |
|
ply1vscl.k |
|- K = ( Base ` R ) |
| 4 |
|
ply1vscl.s |
|- .x. = ( .s ` P ) |
| 5 |
|
ply1vscl.r |
|- ( ph -> R e. Ring ) |
| 6 |
|
ply1vscl.c |
|- ( ph -> C e. K ) |
| 7 |
|
ply1vscl.x |
|- ( ph -> X e. B ) |
| 8 |
1 2
|
ply1bas |
|- B = ( Base ` ( 1o mPoly R ) ) |
| 9 |
|
eqid |
|- ( Scalar ` ( 1o mPoly R ) ) = ( Scalar ` ( 1o mPoly R ) ) |
| 10 |
|
eqid |
|- ( 1o mPoly R ) = ( 1o mPoly R ) |
| 11 |
1 10 4
|
ply1vsca |
|- .x. = ( .s ` ( 1o mPoly R ) ) |
| 12 |
|
eqid |
|- ( Base ` ( Scalar ` ( 1o mPoly R ) ) ) = ( Base ` ( Scalar ` ( 1o mPoly R ) ) ) |
| 13 |
|
1oex |
|- 1o e. _V |
| 14 |
13
|
a1i |
|- ( ph -> 1o e. _V ) |
| 15 |
10 14 5
|
mpllmodd |
|- ( ph -> ( 1o mPoly R ) e. LMod ) |
| 16 |
10 14 5
|
mplsca |
|- ( ph -> R = ( Scalar ` ( 1o mPoly R ) ) ) |
| 17 |
16
|
fveq2d |
|- ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` ( 1o mPoly R ) ) ) ) |
| 18 |
3 17
|
eqtrid |
|- ( ph -> K = ( Base ` ( Scalar ` ( 1o mPoly R ) ) ) ) |
| 19 |
6 18
|
eleqtrd |
|- ( ph -> C e. ( Base ` ( Scalar ` ( 1o mPoly R ) ) ) ) |
| 20 |
8 9 11 12 15 19 7
|
lmodvscld |
|- ( ph -> ( C .x. X ) e. B ) |