Theorem evls1fvf

Description: The subring evaluation function for a univariate polynomial as a function, with domain and codomain. (Contributed by Thierry Arnoux, 22-Mar-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 ) )
	evls1fvf.b	|- B = ( Base ` R )
	evls1fvf.q	|- ( ph -> Q e. U )
Assertion	evls1fvf	|- ( ph -> ( O ` Q ) : B --> B )

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		evls1fvf.b	|- B = ( Base ` R )
7		evls1fvf.q	|- ( ph -> Q e. U )
8		eqid	|- ( R ^s B ) = ( R ^s B )
9		eqid	|- ( Base ` ( R ^s B ) ) = ( Base ` ( R ^s B ) )
10	6	fvexi	|- B e. _V
11	10	a1i	|- ( ph -> B e. _V )
12		eqid	|- ( R |`s S ) = ( R |`s S )
13	1 6 8 12 2	evls1rhm	|- ( ( R e. CRing /\ S e. ( SubRing ` R ) ) -> O e. ( P RingHom ( R ^s B ) ) )
14	4 5 13	syl2anc	|- ( ph -> O e. ( P RingHom ( R ^s B ) ) )
15	3 9	rhmf	|- ( O e. ( P RingHom ( R ^s B ) ) -> O : U --> ( Base ` ( R ^s B ) ) )
16	14 15	syl	|- ( ph -> O : U --> ( Base ` ( R ^s B ) ) )
17	16 7	ffvelcdmd	|- ( ph -> ( O ` Q ) e. ( Base ` ( R ^s B ) ) )
18	8 6 9 4 11 17	pwselbas	|- ( ph -> ( O ` Q ) : B --> B )