| Step |
Hyp |
Ref |
Expression |
| 1 |
|
evls1maprhm.q |
|- O = ( R evalSub1 S ) |
| 2 |
|
evls1maprhm.p |
|- P = ( Poly1 ` ( R |`s S ) ) |
| 3 |
|
evls1maprhm.b |
|- B = ( Base ` R ) |
| 4 |
|
evls1maprhm.u |
|- U = ( Base ` P ) |
| 5 |
|
evls1maprhm.r |
|- ( ph -> R e. CRing ) |
| 6 |
|
evls1maprhm.s |
|- ( ph -> S e. ( SubRing ` R ) ) |
| 7 |
|
evls1fvcl.1 |
|- ( ph -> Y e. B ) |
| 8 |
|
evls1fvcl.2 |
|- ( ph -> M e. U ) |
| 9 |
|
eqid |
|- ( R |`s S ) = ( R |`s S ) |
| 10 |
|
eqid |
|- ( eval1 ` R ) = ( eval1 ` R ) |
| 11 |
1 3 2 9 4 10 5 6
|
ressply1evl |
|- ( ph -> O = ( ( eval1 ` R ) |` U ) ) |
| 12 |
11
|
fveq1d |
|- ( ph -> ( O ` M ) = ( ( ( eval1 ` R ) |` U ) ` M ) ) |
| 13 |
8
|
fvresd |
|- ( ph -> ( ( ( eval1 ` R ) |` U ) ` M ) = ( ( eval1 ` R ) ` M ) ) |
| 14 |
12 13
|
eqtrd |
|- ( ph -> ( O ` M ) = ( ( eval1 ` R ) ` M ) ) |
| 15 |
14
|
fveq1d |
|- ( ph -> ( ( O ` M ) ` Y ) = ( ( ( eval1 ` R ) ` M ) ` Y ) ) |
| 16 |
|
eqid |
|- ( Poly1 ` R ) = ( Poly1 ` R ) |
| 17 |
|
eqid |
|- ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) ) |
| 18 |
|
eqid |
|- ( ( Poly1 ` R ) |`s U ) = ( ( Poly1 ` R ) |`s U ) |
| 19 |
16 9 2 4 6 18
|
ressply1bas |
|- ( ph -> U = ( Base ` ( ( Poly1 ` R ) |`s U ) ) ) |
| 20 |
18 17
|
ressbasss |
|- ( Base ` ( ( Poly1 ` R ) |`s U ) ) C_ ( Base ` ( Poly1 ` R ) ) |
| 21 |
19 20
|
eqsstrdi |
|- ( ph -> U C_ ( Base ` ( Poly1 ` R ) ) ) |
| 22 |
21 8
|
sseldd |
|- ( ph -> M e. ( Base ` ( Poly1 ` R ) ) ) |
| 23 |
10 16 3 17 5 7 22
|
fveval1fvcl |
|- ( ph -> ( ( ( eval1 ` R ) ` M ) ` Y ) e. B ) |
| 24 |
15 23
|
eqeltrd |
|- ( ph -> ( ( O ` M ) ` Y ) e. B ) |