Metamath Proof Explorer

Theorem evlsmulval

Description: Polynomial evaluation builder for multiplication. (Contributed by SN, 27-Jul-2024)

Ref Expression
Hypotheses evlsaddval.q 
|- Q = ( ( I evalSub S ) ` R )
evlsaddval.p 
|- P = ( I mPoly U )
evlsaddval.u 
|- U = ( S |`s R )
evlsaddval.k 
|- K = ( Base ` S )
evlsaddval.b 
|- B = ( Base ` P )
evlsaddval.i 
|- ( ph -> I e. Z )
evlsaddval.s 
|- ( ph -> S e. CRing )
evlsaddval.r 
|- ( ph -> R e. ( SubRing ` S ) )
evlsaddval.a 
|- ( ph -> A e. ( K ^m I ) )
evlsaddval.m 
|- ( ph -> ( M e. B /\ ( ( Q ` M ) ` A ) = V ) )
evlsaddval.n 
|- ( ph -> ( N e. B /\ ( ( Q ` N ) ` A ) = W ) )
evlsmulval.g 
|- .xb = ( .r ` P )
evlsmulval.f 
|- .x. = ( .r ` S )
Assertion evlsmulval 
|- ( ph -> ( ( M .xb N ) e. B /\ ( ( Q ` ( M .xb N ) ) ` A ) = ( V .x. W ) ) )

Proof

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 ffvelrnd 
 |-  ( ph -> ( Q ` M ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
31 29 20 ffvelrnd 
 |-  ( 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 ) ) )