| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mpfconst.b |
|- B = ( Base ` S ) |
| 2 |
|
mpfconst.q |
|- Q = ran ( ( I evalSub S ) ` R ) |
| 3 |
|
mpfconst.i |
|- ( ph -> I e. V ) |
| 4 |
|
mpfconst.s |
|- ( ph -> S e. CRing ) |
| 5 |
|
mpfconst.r |
|- ( ph -> R e. ( SubRing ` S ) ) |
| 6 |
|
mpfconst.x |
|- ( ph -> X e. R ) |
| 7 |
|
eqid |
|- ( ( I evalSub S ) ` R ) = ( ( I evalSub S ) ` R ) |
| 8 |
|
eqid |
|- ( I mPoly ( S |`s R ) ) = ( I mPoly ( S |`s R ) ) |
| 9 |
|
eqid |
|- ( S |`s R ) = ( S |`s R ) |
| 10 |
|
eqid |
|- ( algSc ` ( I mPoly ( S |`s R ) ) ) = ( algSc ` ( I mPoly ( S |`s R ) ) ) |
| 11 |
7 8 9 1 10 3 4 5 6
|
evlssca |
|- ( ph -> ( ( ( I evalSub S ) ` R ) ` ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` X ) ) = ( ( B ^m I ) X. { X } ) ) |
| 12 |
|
eqid |
|- ( S ^s ( B ^m I ) ) = ( S ^s ( B ^m I ) ) |
| 13 |
7 8 9 12 1
|
evlsrhm |
|- ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S |`s R ) ) RingHom ( S ^s ( B ^m I ) ) ) ) |
| 14 |
3 4 5 13
|
syl3anc |
|- ( ph -> ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S |`s R ) ) RingHom ( S ^s ( B ^m I ) ) ) ) |
| 15 |
|
eqid |
|- ( Base ` ( I mPoly ( S |`s R ) ) ) = ( Base ` ( I mPoly ( S |`s R ) ) ) |
| 16 |
|
eqid |
|- ( Base ` ( S ^s ( B ^m I ) ) ) = ( Base ` ( S ^s ( B ^m I ) ) ) |
| 17 |
15 16
|
rhmf |
|- ( ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S |`s R ) ) RingHom ( S ^s ( B ^m I ) ) ) -> ( ( I evalSub S ) ` R ) : ( Base ` ( I mPoly ( S |`s R ) ) ) --> ( Base ` ( S ^s ( B ^m I ) ) ) ) |
| 18 |
|
ffn |
|- ( ( ( I evalSub S ) ` R ) : ( Base ` ( I mPoly ( S |`s R ) ) ) --> ( Base ` ( S ^s ( B ^m I ) ) ) -> ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S |`s R ) ) ) ) |
| 19 |
14 17 18
|
3syl |
|- ( ph -> ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S |`s R ) ) ) ) |
| 20 |
9
|
subrgring |
|- ( R e. ( SubRing ` S ) -> ( S |`s R ) e. Ring ) |
| 21 |
5 20
|
syl |
|- ( ph -> ( S |`s R ) e. Ring ) |
| 22 |
|
eqid |
|- ( Scalar ` ( I mPoly ( S |`s R ) ) ) = ( Scalar ` ( I mPoly ( S |`s R ) ) ) |
| 23 |
8
|
mplring |
|- ( ( I e. V /\ ( S |`s R ) e. Ring ) -> ( I mPoly ( S |`s R ) ) e. Ring ) |
| 24 |
8
|
mpllmod |
|- ( ( I e. V /\ ( S |`s R ) e. Ring ) -> ( I mPoly ( S |`s R ) ) e. LMod ) |
| 25 |
|
eqid |
|- ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) = ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) |
| 26 |
10 22 23 24 25 15
|
asclf |
|- ( ( I e. V /\ ( S |`s R ) e. Ring ) -> ( algSc ` ( I mPoly ( S |`s R ) ) ) : ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) --> ( Base ` ( I mPoly ( S |`s R ) ) ) ) |
| 27 |
3 21 26
|
syl2anc |
|- ( ph -> ( algSc ` ( I mPoly ( S |`s R ) ) ) : ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) --> ( Base ` ( I mPoly ( S |`s R ) ) ) ) |
| 28 |
1
|
subrgss |
|- ( R e. ( SubRing ` S ) -> R C_ B ) |
| 29 |
9 1
|
ressbas2 |
|- ( R C_ B -> R = ( Base ` ( S |`s R ) ) ) |
| 30 |
5 28 29
|
3syl |
|- ( ph -> R = ( Base ` ( S |`s R ) ) ) |
| 31 |
|
ovexd |
|- ( ph -> ( S |`s R ) e. _V ) |
| 32 |
8 3 31
|
mplsca |
|- ( ph -> ( S |`s R ) = ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) |
| 33 |
32
|
fveq2d |
|- ( ph -> ( Base ` ( S |`s R ) ) = ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) ) |
| 34 |
30 33
|
eqtrd |
|- ( ph -> R = ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) ) |
| 35 |
6 34
|
eleqtrd |
|- ( ph -> X e. ( Base ` ( Scalar ` ( I mPoly ( S |`s R ) ) ) ) ) |
| 36 |
27 35
|
ffvelcdmd |
|- ( ph -> ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` X ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) |
| 37 |
|
fnfvelrn |
|- ( ( ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S |`s R ) ) ) /\ ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` X ) e. ( Base ` ( I mPoly ( S |`s R ) ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` X ) ) e. ran ( ( I evalSub S ) ` R ) ) |
| 38 |
19 36 37
|
syl2anc |
|- ( ph -> ( ( ( I evalSub S ) ` R ) ` ( ( algSc ` ( I mPoly ( S |`s R ) ) ) ` X ) ) e. ran ( ( I evalSub S ) ` R ) ) |
| 39 |
11 38
|
eqeltrrd |
|- ( ph -> ( ( B ^m I ) X. { X } ) e. ran ( ( I evalSub S ) ` R ) ) |
| 40 |
39 2
|
eleqtrrdi |
|- ( ph -> ( ( B ^m I ) X. { X } ) e. Q ) |