Theorem evls1fn

Description: Functionality of the subring polynomial evaluation. (Contributed by Thierry Arnoux, 9-Feb-2025)

	Ref	Expression
Hypotheses	evls1fn.o	|- O = ( R evalSub1 S )
	evls1fn.p	|- P = ( Poly1 ` ( R |`s S ) )
	evls1fn.u	|- U = ( Base ` P )
	evls1fn.1	|- ( ph -> R e. CRing )
	evls1fn.2	|- ( ph -> S e. ( SubRing ` R ) )
Assertion	evls1fn	|- ( ph -> O Fn U )

Proof

Step	Hyp	Ref	Expression
1		evls1fn.o	|- O = ( R evalSub1 S )
2		evls1fn.p	|- P = ( Poly1 ` ( R |`s S ) )
3		evls1fn.u	|- U = ( Base ` P )
4		evls1fn.1	|- ( ph -> R e. CRing )
5		evls1fn.2	|- ( ph -> S e. ( SubRing ` R ) )
6		eqid	|- ( Base ` R ) = ( Base ` R )
7		eqid	|- ( R ^s ( Base ` R ) ) = ( R ^s ( Base ` R ) )
8		eqid	|- ( R |`s S ) = ( R |`s S )
9	1 6 7 8 2	evls1rhm	|- ( ( R e. CRing /\ S e. ( SubRing ` R ) ) -> O e. ( P RingHom ( R ^s ( Base ` R ) ) ) )
10	4 5 9	syl2anc	|- ( ph -> O e. ( P RingHom ( R ^s ( Base ` R ) ) ) )
11		eqid	|- ( Base ` ( R ^s ( Base ` R ) ) ) = ( Base ` ( R ^s ( Base ` R ) ) )
12	3 11	rhmf	|- ( O e. ( P RingHom ( R ^s ( Base ` R ) ) ) -> O : U --> ( Base ` ( R ^s ( Base ` R ) ) ) )
13	10 12	syl	|- ( ph -> O : U --> ( Base ` ( R ^s ( Base ` R ) ) ) )
14	13	ffnd	|- ( ph -> O Fn U )