Theorem fveval1fvcl

Description: The function value of the evaluation function of a polynomial is an element of the underlying ring. (Contributed by AV, 17-Sep-2019)

	Ref	Expression
Hypotheses	fveval1fvcl.q	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
	fveval1fvcl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	fveval1fvcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	fveval1fvcl.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
	fveval1fvcl.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	fveval1fvcl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	fveval1fvcl.m	⊢ ( 𝜑 → 𝑀 ∈ 𝑈 )
Assertion	fveval1fvcl	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fveval1fvcl.q	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
2		fveval1fvcl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		fveval1fvcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		fveval1fvcl.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
5		fveval1fvcl.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
6		fveval1fvcl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		fveval1fvcl.m	⊢ ( 𝜑 → 𝑀 ∈ 𝑈 )
8		eqid	⊢ ( 𝑅 ↑s 𝐵 ) = ( 𝑅 ↑s 𝐵 )
9		eqid	⊢ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) = ( Base ‘ ( 𝑅 ↑s 𝐵 ) )
10	3	fvexi	⊢ 𝐵 ∈ V
11	10	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
12	1 2 8 3	evl1rhm	⊢ ( 𝑅 ∈ CRing → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐵 ) ) )
13	4 9	rhmf	⊢ ( 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐵 ) ) → 𝑂 : 𝑈 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
14	5 12 13	3syl	⊢ ( 𝜑 → 𝑂 : 𝑈 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
15	14 7	ffvelrnd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑀 ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
16	8 3 9 5 11 15	pwselbas	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑀 ) : 𝐵 ⟶ 𝐵 )
17	16 6	ffvelrnd	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ∈ 𝐵 )