Theorem evlscl

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

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

Proof

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