Metamath Proof Explorer

Theorem evlsval3

Description: Give a formula for the polynomial evaluation homomorphism. (Contributed by SN, 26-Jul-2024)

Ref Expression
Hypotheses evlsval3.q 
|- Q = ( ( I evalSub S ) ` R )
evlsval3.p 
|- P = ( I mPoly U )
evlsval3.b 
|- B = ( Base ` P )
evlsval3.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
evlsval3.k 
|- K = ( Base ` S )
evlsval3.u 
|- U = ( S |`s R )
evlsval3.t 
|- T = ( S ^s ( K ^m I ) )
evlsval3.m 
|- M = ( mulGrp ` T )
evlsval3.w 
|- .^ = ( .g ` M )
evlsval3.x 
|- .x. = ( .r ` T )
evlsval3.e 
|- E = ( p e. B |-> ( T gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( M gsum ( b oF .^ G ) ) ) ) ) )
evlsval3.f 
|- F = ( x e. R |-> ( ( K ^m I ) X. { x } ) )
evlsval3.g 
|- G = ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) )
evlsval3.i 
|- ( ph -> I e. V )
evlsval3.s 
|- ( ph -> S e. CRing )
evlsval3.r 
|- ( ph -> R e. ( SubRing ` S ) )
Assertion evlsval3 
|- ( ph -> Q = E )

Proof

Step Hyp Ref Expression
1 evlsval3.q 
 |-  Q = ( ( I evalSub S ) ` R )
2 evlsval3.p 
 |-  P = ( I mPoly U )
3 evlsval3.b 
 |-  B = ( Base ` P )
4 evlsval3.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
5 evlsval3.k 
 |-  K = ( Base ` S )
6 evlsval3.u 
 |-  U = ( S |`s R )
7 evlsval3.t 
 |-  T = ( S ^s ( K ^m I ) )
8 evlsval3.m 
 |-  M = ( mulGrp ` T )
9 evlsval3.w 
 |-  .^ = ( .g ` M )
10 evlsval3.x 
 |-  .x. = ( .r ` T )
11 evlsval3.e 
 |-  E = ( p e. B |-> ( T gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( M gsum ( b oF .^ G ) ) ) ) ) )
12 evlsval3.f 
 |-  F = ( x e. R |-> ( ( K ^m I ) X. { x } ) )
13 evlsval3.g 
 |-  G = ( x e. I |-> ( a e. ( K ^m I ) |-> ( a ` x ) ) )
14 evlsval3.i 
 |-  ( ph -> I e. V )
15 evlsval3.s 
 |-  ( ph -> S e. CRing )
16 evlsval3.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
17 eqid 
 |-  ( I mVar U ) = ( I mVar U )
18 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
19 1 2 17 6 7 5 18 12 13 evlsval 
 |-  ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q = ( iota_ f e. ( P RingHom T ) ( ( f o. ( algSc ` P ) ) = F /\ ( f o. ( I mVar U ) ) = G ) ) )
20 14 15 16 19 syl3anc 
 |-  ( ph -> Q = ( iota_ f e. ( P RingHom T ) ( ( f o. ( algSc ` P ) ) = F /\ ( f o. ( I mVar U ) ) = G ) ) )
21 eqid 
 |-  ( Base ` T ) = ( Base ` T )
22 6 subrgcrng 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> U e. CRing )
23 15 16 22 syl2anc 
 |-  ( ph -> U e. CRing )
24 ovexd 
 |-  ( ph -> ( K ^m I ) e. _V )
25 7 pwscrng 
 |-  ( ( S e. CRing /\ ( K ^m I ) e. _V ) -> T e. CRing )
26 15 24 25 syl2anc 
 |-  ( ph -> T e. CRing )
27 5 subrgss 
 |-  ( R e. ( SubRing ` S ) -> R C_ K )
28 16 27 syl 
 |-  ( ph -> R C_ K )
29 28 resmptd 
 |-  ( ph -> ( ( x e. K |-> ( ( K ^m I ) X. { x } ) ) |` R ) = ( x e. R |-> ( ( K ^m I ) X. { x } ) ) )
30 12 29 eqtr4id 
 |-  ( ph -> F = ( ( x e. K |-> ( ( K ^m I ) X. { x } ) ) |` R ) )
31 15 crngringd 
 |-  ( ph -> S e. Ring )
32 eqid 
 |-  ( x e. K |-> ( ( K ^m I ) X. { x } ) ) = ( x e. K |-> ( ( K ^m I ) X. { x } ) )
33 7 5 32 pwsdiagrhm 
 |-  ( ( S e. Ring /\ ( K ^m I ) e. _V ) -> ( x e. K |-> ( ( K ^m I ) X. { x } ) ) e. ( S RingHom T ) )
34 31 24 33 syl2anc 
 |-  ( ph -> ( x e. K |-> ( ( K ^m I ) X. { x } ) ) e. ( S RingHom T ) )
35 6 resrhm 
 |-  ( ( ( x e. K |-> ( ( K ^m I ) X. { x } ) ) e. ( S RingHom T ) /\ R e. ( SubRing ` S ) ) -> ( ( x e. K |-> ( ( K ^m I ) X. { x } ) ) |` R ) e. ( U RingHom T ) )
36 34 16 35 syl2anc 
 |-  ( ph -> ( ( x e. K |-> ( ( K ^m I ) X. { x } ) ) |` R ) e. ( U RingHom T ) )
37 30 36 eqeltrd 
 |-  ( ph -> F e. ( U RingHom T ) )
38 5 fvexi 
 |-  K e. _V
39 elmapg 
 |-  ( ( K e. _V /\ I e. V ) -> ( a e. ( K ^m I ) <-> a : I --> K ) )
40 38 14 39 sylancr 
 |-  ( ph -> ( a e. ( K ^m I ) <-> a : I --> K ) )
41 40 biimpa 
 |-  ( ( ph /\ a e. ( K ^m I ) ) -> a : I --> K )
42 41 adantlr 
 |-  ( ( ( ph /\ x e. I ) /\ a e. ( K ^m I ) ) -> a : I --> K )
43 simplr 
 |-  ( ( ( ph /\ x e. I ) /\ a e. ( K ^m I ) ) -> x e. I )
44 42 43 ffvelrnd 
 |-  ( ( ( ph /\ x e. I ) /\ a e. ( K ^m I ) ) -> ( a ` x ) e. K )
45 44 fmpttd 
 |-  ( ( ph /\ x e. I ) -> ( a e. ( K ^m I ) |-> ( a ` x ) ) : ( K ^m I ) --> K )
46 ovexd 
 |-  ( ( ph /\ x e. I ) -> ( K ^m I ) e. _V )
47 7 5 21 pwselbasb 
 |-  ( ( S e. CRing /\ ( K ^m I ) e. _V ) -> ( ( a e. ( K ^m I ) |-> ( a ` x ) ) e. ( Base ` T ) <-> ( a e. ( K ^m I ) |-> ( a ` x ) ) : ( K ^m I ) --> K ) )
48 15 46 47 syl2an2r 
 |-  ( ( ph /\ x e. I ) -> ( ( a e. ( K ^m I ) |-> ( a ` x ) ) e. ( Base ` T ) <-> ( a e. ( K ^m I ) |-> ( a ` x ) ) : ( K ^m I ) --> K ) )
49 45 48 mpbird 
 |-  ( ( ph /\ x e. I ) -> ( a e. ( K ^m I ) |-> ( a ` x ) ) e. ( Base ` T ) )
50 49 13 fmptd 
 |-  ( ph -> G : I --> ( Base ` T ) )
51 2 3 21 4 8 9 10 17 11 14 23 26 37 50 18 evlslem1 
 |-  ( ph -> ( E e. ( P RingHom T ) /\ ( E o. ( algSc ` P ) ) = F /\ ( E o. ( I mVar U ) ) = G ) )
52 51 simp2d 
 |-  ( ph -> ( E o. ( algSc ` P ) ) = F )
53 51 simp3d 
 |-  ( ph -> ( E o. ( I mVar U ) ) = G )
54 51 simp1d 
 |-  ( ph -> E e. ( P RingHom T ) )
55 2 21 18 17 14 23 26 37 50 evlseu 
 |-  ( ph -> E! f e. ( P RingHom T ) ( ( f o. ( algSc ` P ) ) = F /\ ( f o. ( I mVar U ) ) = G ) )
56 coeq1 
 |-  ( f = E -> ( f o. ( algSc ` P ) ) = ( E o. ( algSc ` P ) ) )
57 56 eqeq1d 
 |-  ( f = E -> ( ( f o. ( algSc ` P ) ) = F <-> ( E o. ( algSc ` P ) ) = F ) )
58 coeq1 
 |-  ( f = E -> ( f o. ( I mVar U ) ) = ( E o. ( I mVar U ) ) )
59 58 eqeq1d 
 |-  ( f = E -> ( ( f o. ( I mVar U ) ) = G <-> ( E o. ( I mVar U ) ) = G ) )
60 57 59 anbi12d 
 |-  ( f = E -> ( ( ( f o. ( algSc ` P ) ) = F /\ ( f o. ( I mVar U ) ) = G ) <-> ( ( E o. ( algSc ` P ) ) = F /\ ( E o. ( I mVar U ) ) = G ) ) )
61 60 riota2 
 |-  ( ( E e. ( P RingHom T ) /\ E! f e. ( P RingHom T ) ( ( f o. ( algSc ` P ) ) = F /\ ( f o. ( I mVar U ) ) = G ) ) -> ( ( ( E o. ( algSc ` P ) ) = F /\ ( E o. ( I mVar U ) ) = G ) <-> ( iota_ f e. ( P RingHom T ) ( ( f o. ( algSc ` P ) ) = F /\ ( f o. ( I mVar U ) ) = G ) ) = E ) )
62 54 55 61 syl2anc 
 |-  ( ph -> ( ( ( E o. ( algSc ` P ) ) = F /\ ( E o. ( I mVar U ) ) = G ) <-> ( iota_ f e. ( P RingHom T ) ( ( f o. ( algSc ` P ) ) = F /\ ( f o. ( I mVar U ) ) = G ) ) = E ) )
63 52 53 62 mpbi2and 
 |-  ( ph -> ( iota_ f e. ( P RingHom T ) ( ( f o. ( algSc ` P ) ) = F /\ ( f o. ( I mVar U ) ) = G ) ) = E )
64 20 63 eqtrd 
 |-  ( ph -> Q = E )