This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem evlvvval

Description: Give a formula for the evaluation of a polynomial given assignments from variables to values. (Contributed by SN, 5-Mar-2025)

Ref Expression
Hypotheses evlvvval.q 
|- Q = ( I eval R )
evlvvval.p 
|- P = ( I mPoly R )
evlvvval.b 
|- B = ( Base ` P )
evlvvval.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
evlvvval.k 
|- K = ( Base ` R )
evlvvval.m 
|- M = ( mulGrp ` R )
evlvvval.w 
|- .^ = ( .g ` M )
evlvvval.x 
|- .x. = ( .r ` R )
evlvvval.i 
|- ( ph -> I e. V )
evlvvval.r 
|- ( ph -> R e. CRing )
evlvvval.f 
|- ( ph -> F e. B )
evlvvval.a 
|- ( ph -> A e. ( K ^m I ) )
Assertion evlvvval 
|- ( ph -> ( ( Q ` F ) ` A ) = ( R gsum ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 evlvvval.q 
 |-  Q = ( I eval R )
2 evlvvval.p 
 |-  P = ( I mPoly R )
3 evlvvval.b 
 |-  B = ( Base ` P )
4 evlvvval.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
5 evlvvval.k 
 |-  K = ( Base ` R )
6 evlvvval.m 
 |-  M = ( mulGrp ` R )
7 evlvvval.w 
 |-  .^ = ( .g ` M )
8 evlvvval.x 
 |-  .x. = ( .r ` R )
9 evlvvval.i 
 |-  ( ph -> I e. V )
10 evlvvval.r 
 |-  ( ph -> R e. CRing )
11 evlvvval.f 
 |-  ( ph -> F e. B )
12 evlvvval.a 
 |-  ( ph -> A e. ( K ^m I ) )
13 eqid 
 |-  ( ( I evalSub R ) ` ( Base ` R ) ) = ( ( I evalSub R ) ` ( Base ` R ) )
14 eqid 
 |-  ( I mPoly ( R |`s ( Base ` R ) ) ) = ( I mPoly ( R |`s ( Base ` R ) ) )
15 eqid 
 |-  ( R |`s ( Base ` R ) ) = ( R |`s ( Base ` R ) )
16 eqid 
 |-  ( Base ` ( I mPoly ( R |`s ( Base ` R ) ) ) ) = ( Base ` ( I mPoly ( R |`s ( Base ` R ) ) ) )
17 10 crngringd 
 |-  ( ph -> R e. Ring )
18 eqid 
 |-  ( Base ` R ) = ( Base ` R )
19 18 subrgid 
 |-  ( R e. Ring -> ( Base ` R ) e. ( SubRing ` R ) )
20 17 19 syl 
 |-  ( ph -> ( Base ` R ) e. ( SubRing ` R ) )
21 18 ressid 
 |-  ( R e. CRing -> ( R |`s ( Base ` R ) ) = R )
22 10 21 syl 
 |-  ( ph -> ( R |`s ( Base ` R ) ) = R )
23 22 oveq2d 
 |-  ( ph -> ( I mPoly ( R |`s ( Base ` R ) ) ) = ( I mPoly R ) )
24 23 2 eqtr4di 
 |-  ( ph -> ( I mPoly ( R |`s ( Base ` R ) ) ) = P )
25 24 fveq2d 
 |-  ( ph -> ( Base ` ( I mPoly ( R |`s ( Base ` R ) ) ) ) = ( Base ` P ) )
26 25 3 eqtr4di 
 |-  ( ph -> ( Base ` ( I mPoly ( R |`s ( Base ` R ) ) ) ) = B )
27 11 26 eleqtrrd 
 |-  ( ph -> F e. ( Base ` ( I mPoly ( R |`s ( Base ` R ) ) ) ) )
28 13 1 14 15 16 9 10 20 27 evlsevl 
 |-  ( ph -> ( ( ( I evalSub R ) ` ( Base ` R ) ) ` F ) = ( Q ` F ) )
29 28 fveq1d 
 |-  ( ph -> ( ( ( ( I evalSub R ) ` ( Base ` R ) ) ` F ) ` A ) = ( ( Q ` F ) ` A ) )
30 13 14 16 15 4 5 6 7 8 9 10 20 27 12 evlsvvval 
 |-  ( ph -> ( ( ( ( I evalSub R ) ` ( Base ` R ) ) ` F ) ` A ) = ( R gsum ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) )
31 29 30 eqtr3d 
 |-  ( ph -> ( ( Q ` F ) ` A ) = ( R gsum ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) )