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 )