| Step |
Hyp |
Ref |
Expression |
| 1 |
|
evlsaddval.q |
|- Q = ( ( I evalSub S ) ` R ) |
| 2 |
|
evlsaddval.p |
|- P = ( I mPoly U ) |
| 3 |
|
evlsaddval.u |
|- U = ( S |`s R ) |
| 4 |
|
evlsaddval.k |
|- K = ( Base ` S ) |
| 5 |
|
evlsaddval.b |
|- B = ( Base ` P ) |
| 6 |
|
evlsaddval.i |
|- ( ph -> I e. Z ) |
| 7 |
|
evlsaddval.s |
|- ( ph -> S e. CRing ) |
| 8 |
|
evlsaddval.r |
|- ( ph -> R e. ( SubRing ` S ) ) |
| 9 |
|
evlsaddval.a |
|- ( ph -> A e. ( K ^m I ) ) |
| 10 |
|
evlsaddval.m |
|- ( ph -> ( M e. B /\ ( ( Q ` M ) ` A ) = V ) ) |
| 11 |
|
evlsaddval.n |
|- ( ph -> ( N e. B /\ ( ( Q ` N ) ` A ) = W ) ) |
| 12 |
|
evlsmulval.g |
|- .xb = ( .r ` P ) |
| 13 |
|
evlsmulval.f |
|- .x. = ( .r ` S ) |
| 14 |
|
eqid |
|- ( S ^s ( K ^m I ) ) = ( S ^s ( K ^m I ) ) |
| 15 |
1 2 3 14 4
|
evlsrhm |
|- ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( P RingHom ( S ^s ( K ^m I ) ) ) ) |
| 16 |
6 7 8 15
|
syl3anc |
|- ( ph -> Q e. ( P RingHom ( S ^s ( K ^m I ) ) ) ) |
| 17 |
|
rhmrcl1 |
|- ( Q e. ( P RingHom ( S ^s ( K ^m I ) ) ) -> P e. Ring ) |
| 18 |
16 17
|
syl |
|- ( ph -> P e. Ring ) |
| 19 |
10
|
simpld |
|- ( ph -> M e. B ) |
| 20 |
11
|
simpld |
|- ( ph -> N e. B ) |
| 21 |
5 12
|
ringcl |
|- ( ( P e. Ring /\ M e. B /\ N e. B ) -> ( M .xb N ) e. B ) |
| 22 |
18 19 20 21
|
syl3anc |
|- ( ph -> ( M .xb N ) e. B ) |
| 23 |
|
eqid |
|- ( .r ` ( S ^s ( K ^m I ) ) ) = ( .r ` ( S ^s ( K ^m I ) ) ) |
| 24 |
5 12 23
|
rhmmul |
|- ( ( Q e. ( P RingHom ( S ^s ( K ^m I ) ) ) /\ M e. B /\ N e. B ) -> ( Q ` ( M .xb N ) ) = ( ( Q ` M ) ( .r ` ( S ^s ( K ^m I ) ) ) ( Q ` N ) ) ) |
| 25 |
16 19 20 24
|
syl3anc |
|- ( ph -> ( Q ` ( M .xb N ) ) = ( ( Q ` M ) ( .r ` ( S ^s ( K ^m I ) ) ) ( Q ` N ) ) ) |
| 26 |
|
eqid |
|- ( Base ` ( S ^s ( K ^m I ) ) ) = ( Base ` ( S ^s ( K ^m I ) ) ) |
| 27 |
|
ovexd |
|- ( ph -> ( K ^m I ) e. _V ) |
| 28 |
5 26
|
rhmf |
|- ( Q e. ( P RingHom ( S ^s ( K ^m I ) ) ) -> Q : B --> ( Base ` ( S ^s ( K ^m I ) ) ) ) |
| 29 |
16 28
|
syl |
|- ( ph -> Q : B --> ( Base ` ( S ^s ( K ^m I ) ) ) ) |
| 30 |
29 19
|
ffvelcdmd |
|- ( ph -> ( Q ` M ) e. ( Base ` ( S ^s ( K ^m I ) ) ) ) |
| 31 |
29 20
|
ffvelcdmd |
|- ( ph -> ( Q ` N ) e. ( Base ` ( S ^s ( K ^m I ) ) ) ) |
| 32 |
14 26 7 27 30 31 13 23
|
pwsmulrval |
|- ( ph -> ( ( Q ` M ) ( .r ` ( S ^s ( K ^m I ) ) ) ( Q ` N ) ) = ( ( Q ` M ) oF .x. ( Q ` N ) ) ) |
| 33 |
25 32
|
eqtrd |
|- ( ph -> ( Q ` ( M .xb N ) ) = ( ( Q ` M ) oF .x. ( Q ` N ) ) ) |
| 34 |
33
|
fveq1d |
|- ( ph -> ( ( Q ` ( M .xb N ) ) ` A ) = ( ( ( Q ` M ) oF .x. ( Q ` N ) ) ` A ) ) |
| 35 |
14 4 26 7 27 30
|
pwselbas |
|- ( ph -> ( Q ` M ) : ( K ^m I ) --> K ) |
| 36 |
35
|
ffnd |
|- ( ph -> ( Q ` M ) Fn ( K ^m I ) ) |
| 37 |
14 4 26 7 27 31
|
pwselbas |
|- ( ph -> ( Q ` N ) : ( K ^m I ) --> K ) |
| 38 |
37
|
ffnd |
|- ( ph -> ( Q ` N ) Fn ( K ^m I ) ) |
| 39 |
|
fnfvof |
|- ( ( ( ( Q ` M ) Fn ( K ^m I ) /\ ( Q ` N ) Fn ( K ^m I ) ) /\ ( ( K ^m I ) e. _V /\ A e. ( K ^m I ) ) ) -> ( ( ( Q ` M ) oF .x. ( Q ` N ) ) ` A ) = ( ( ( Q ` M ) ` A ) .x. ( ( Q ` N ) ` A ) ) ) |
| 40 |
36 38 27 9 39
|
syl22anc |
|- ( ph -> ( ( ( Q ` M ) oF .x. ( Q ` N ) ) ` A ) = ( ( ( Q ` M ) ` A ) .x. ( ( Q ` N ) ` A ) ) ) |
| 41 |
10
|
simprd |
|- ( ph -> ( ( Q ` M ) ` A ) = V ) |
| 42 |
11
|
simprd |
|- ( ph -> ( ( Q ` N ) ` A ) = W ) |
| 43 |
41 42
|
oveq12d |
|- ( ph -> ( ( ( Q ` M ) ` A ) .x. ( ( Q ` N ) ` A ) ) = ( V .x. W ) ) |
| 44 |
34 40 43
|
3eqtrd |
|- ( ph -> ( ( Q ` ( M .xb N ) ) ` A ) = ( V .x. W ) ) |
| 45 |
22 44
|
jca |
|- ( ph -> ( ( M .xb N ) e. B /\ ( ( Q ` ( M .xb N ) ) ` A ) = ( V .x. W ) ) ) |