| Step |
Hyp |
Ref |
Expression |
| 1 |
|
evlscafv.1 |
|- Q = ( I eval R ) |
| 2 |
|
evlscafv.2 |
|- W = ( I mPoly R ) |
| 3 |
|
evlscafv.3 |
|- B = ( Base ` R ) |
| 4 |
|
evlscafv.4 |
|- A = ( algSc ` W ) |
| 5 |
|
evlscafv.5 |
|- ( ph -> I e. V ) |
| 6 |
|
evlscafv.6 |
|- ( ph -> R e. CRing ) |
| 7 |
|
evlscafv.7 |
|- ( ph -> X e. B ) |
| 8 |
|
evlscafv.8 |
|- ( ph -> L : I --> B ) |
| 9 |
1 2 3 4 5 6 7
|
evlsca |
|- ( ph -> ( Q ` ( A ` X ) ) = ( ( B ^m I ) X. { X } ) ) |
| 10 |
9
|
fveq1d |
|- ( ph -> ( ( Q ` ( A ` X ) ) ` L ) = ( ( ( B ^m I ) X. { X } ) ` L ) ) |
| 11 |
3
|
fvexi |
|- B e. _V |
| 12 |
11
|
a1i |
|- ( ph -> B e. _V ) |
| 13 |
12 5 8
|
elmapdd |
|- ( ph -> L e. ( B ^m I ) ) |
| 14 |
|
fvconst2g |
|- ( ( X e. B /\ L e. ( B ^m I ) ) -> ( ( ( B ^m I ) X. { X } ) ` L ) = X ) |
| 15 |
7 13 14
|
syl2anc |
|- ( ph -> ( ( ( B ^m I ) X. { X } ) ` L ) = X ) |
| 16 |
10 15
|
eqtrd |
|- ( ph -> ( ( Q ` ( A ` X ) ) ` L ) = X ) |