| Step |
Hyp |
Ref |
Expression |
| 1 |
|
evlsscaval.q |
|- Q = ( ( I evalSub S ) ` R ) |
| 2 |
|
evlsscaval.p |
|- P = ( I mPoly U ) |
| 3 |
|
evlsscaval.u |
|- U = ( S |`s R ) |
| 4 |
|
evlsscaval.k |
|- K = ( Base ` S ) |
| 5 |
|
evlsscaval.b |
|- B = ( Base ` P ) |
| 6 |
|
evlsscaval.a |
|- A = ( algSc ` P ) |
| 7 |
|
evlsscaval.i |
|- ( ph -> I e. V ) |
| 8 |
|
evlsscaval.s |
|- ( ph -> S e. CRing ) |
| 9 |
|
evlsscaval.r |
|- ( ph -> R e. ( SubRing ` S ) ) |
| 10 |
|
evlsscaval.x |
|- ( ph -> X e. R ) |
| 11 |
|
evlsscaval.l |
|- ( ph -> L e. ( K ^m I ) ) |
| 12 |
|
eqid |
|- ( Base ` U ) = ( Base ` U ) |
| 13 |
3
|
subrgring |
|- ( R e. ( SubRing ` S ) -> U e. Ring ) |
| 14 |
9 13
|
syl |
|- ( ph -> U e. Ring ) |
| 15 |
2 5 12 6 7 14
|
mplasclf |
|- ( ph -> A : ( Base ` U ) --> B ) |
| 16 |
3
|
subrgbas |
|- ( R e. ( SubRing ` S ) -> R = ( Base ` U ) ) |
| 17 |
9 16
|
syl |
|- ( ph -> R = ( Base ` U ) ) |
| 18 |
10 17
|
eleqtrd |
|- ( ph -> X e. ( Base ` U ) ) |
| 19 |
15 18
|
ffvelcdmd |
|- ( ph -> ( A ` X ) e. B ) |
| 20 |
1 2 3 4 6 7 8 9 10
|
evlssca |
|- ( ph -> ( Q ` ( A ` X ) ) = ( ( K ^m I ) X. { X } ) ) |
| 21 |
20
|
fveq1d |
|- ( ph -> ( ( Q ` ( A ` X ) ) ` L ) = ( ( ( K ^m I ) X. { X } ) ` L ) ) |
| 22 |
|
fvconst2g |
|- ( ( X e. R /\ L e. ( K ^m I ) ) -> ( ( ( K ^m I ) X. { X } ) ` L ) = X ) |
| 23 |
10 11 22
|
syl2anc |
|- ( ph -> ( ( ( K ^m I ) X. { X } ) ` L ) = X ) |
| 24 |
21 23
|
eqtrd |
|- ( ph -> ( ( Q ` ( A ` X ) ) ` L ) = X ) |
| 25 |
19 24
|
jca |
|- ( ph -> ( ( A ` X ) e. B /\ ( ( Q ` ( A ` X ) ) ` L ) = X ) ) |