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	⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
	evls1fn.p	⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
	evls1fn.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
	evls1fn.1	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	evls1fn.2	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
	evls1fvf.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	evls1fvf.q	⊢ ( 𝜑 → 𝑄 ∈ 𝑈 )
Assertion	evls1fvf	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑄 ) : 𝐵 ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		evls1fn.o	⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
2		evls1fn.p	⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
3		evls1fn.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
4		evls1fn.1	⊢ ( 𝜑 → 𝑅 ∈ CRing )
5		evls1fn.2	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
6		evls1fvf.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
7		evls1fvf.q	⊢ ( 𝜑 → 𝑄 ∈ 𝑈 )
8		eqid	⊢ ( 𝑅 ↑s 𝐵 ) = ( 𝑅 ↑s 𝐵 )
9		eqid	⊢ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) = ( Base ‘ ( 𝑅 ↑s 𝐵 ) )
10	6	fvexi	⊢ 𝐵 ∈ V
11	10	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
12		eqid	⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
13	1 6 8 12 2	evls1rhm	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐵 ) ) )
14	4 5 13	syl2anc	⊢ ( 𝜑 → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐵 ) ) )
15	3 9	rhmf	⊢ ( 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐵 ) ) → 𝑂 : 𝑈 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
16	14 15	syl	⊢ ( 𝜑 → 𝑂 : 𝑈 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
17	16 7	ffvelcdmd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑄 ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
18	8 6 9 4 11 17	pwselbas	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑄 ) : 𝐵 ⟶ 𝐵 )