Metamath Proof Explorer

Theorem evlmulval

Description: Polynomial evaluation builder for multiplication. (Contributed by SN, 18-Feb-2025)

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

Proof

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