Theorem evls1fn

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

	Ref	Expression
Hypotheses	evls1fn.o	⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
	evls1fn.p	⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
	evls1fn.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
	evls1fn.1	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	evls1fn.2	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
Assertion	evls1fn	⊢ ( 𝜑 → 𝑂 Fn 𝑈 )

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		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7		eqid	⊢ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) = ( 𝑅 ↑s ( Base ‘ 𝑅 ) )
8		eqid	⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
9	1 6 7 8 2	evls1rhm	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) )
10	4 5 9	syl2anc	⊢ ( 𝜑 → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) )
11		eqid	⊢ ( Base ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) = ( Base ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) )
12	3 11	rhmf	⊢ ( 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) → 𝑂 : 𝑈 ⟶ ( Base ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) )
13	10 12	syl	⊢ ( 𝜑 → 𝑂 : 𝑈 ⟶ ( Base ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) )
14	13	ffnd	⊢ ( 𝜑 → 𝑂 Fn 𝑈 )