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

Metamath Proof Explorer

Theorem evlcl

Description: A polynomial over the ring R evaluates to an element in R . (Contributed by SN, 12-Mar-2025)

Ref Expression
Hypotheses evlcl.q 
|- Q = ( I eval R )
evlcl.p 
|- P = ( I mPoly R )
evlcl.b 
|- B = ( Base ` P )
evlcl.k 
|- K = ( Base ` R )
evlcl.i 
|- ( ph -> I e. V )
evlcl.r 
|- ( ph -> R e. CRing )
evlcl.f 
|- ( ph -> F e. B )
evlcl.a 
|- ( ph -> A e. ( K ^m I ) )
Assertion evlcl 
|- ( ph -> ( ( Q ` F ) ` A ) e. K )

Proof

Step Hyp Ref Expression
1 evlcl.q 
 |-  Q = ( I eval R )
2 evlcl.p 
 |-  P = ( I mPoly R )
3 evlcl.b 
 |-  B = ( Base ` P )
4 evlcl.k 
 |-  K = ( Base ` R )
5 evlcl.i 
 |-  ( ph -> I e. V )
6 evlcl.r 
 |-  ( ph -> R e. CRing )
7 evlcl.f 
 |-  ( ph -> F e. B )
8 evlcl.a 
 |-  ( ph -> A e. ( K ^m I ) )
9 eqid 
 |-  ( R ^s ( K ^m I ) ) = ( R ^s ( K ^m I ) )
10 eqid 
 |-  ( Base ` ( R ^s ( K ^m I ) ) ) = ( Base ` ( R ^s ( K ^m I ) ) )
11 ovexd 
 |-  ( ph -> ( K ^m I ) e. _V )
12 1 4 2 9 evlrhm 
 |-  ( ( I e. V /\ R e. CRing ) -> Q e. ( P RingHom ( R ^s ( K ^m I ) ) ) )
13 5 6 12 syl2anc 
 |-  ( ph -> Q e. ( P RingHom ( R ^s ( K ^m I ) ) ) )
14 3 10 rhmf 
 |-  ( Q e. ( P RingHom ( R ^s ( K ^m I ) ) ) -> Q : B --> ( Base ` ( R ^s ( K ^m I ) ) ) )
15 13 14 syl 
 |-  ( ph -> Q : B --> ( Base ` ( R ^s ( K ^m I ) ) ) )
16 15 7 ffvelcdmd 
 |-  ( ph -> ( Q ` F ) e. ( Base ` ( R ^s ( K ^m I ) ) ) )
17 9 4 10 6 11 16 pwselbas 
 |-  ( ph -> ( Q ` F ) : ( K ^m I ) --> K )
18 17 8 ffvelcdmd 
 |-  ( ph -> ( ( Q ` F ) ` A ) e. K )