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	$$⊢O={\mathrm{eval}}_1\left(R\right)$$
	fveval1fvcl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	fveval1fvcl.b	$$⊢B={\mathrm{Base}}_R$$
	fveval1fvcl.u	$$⊢U={\mathrm{Base}}_P$$
	fveval1fvcl.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	fveval1fvcl.y	$$⊢\phi \to Y\in B$$
	fveval1fvcl.m	$$⊢\phi \to M\in U$$
Assertion	fveval1fvcl	$$⊢\phi \to O\left(M\right)\left(Y\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		fveval1fvcl.q	$$⊢O={\mathrm{eval}}_1\left(R\right)$$
2		fveval1fvcl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		fveval1fvcl.b	$$⊢B={\mathrm{Base}}_R$$
4		fveval1fvcl.u	$$⊢U={\mathrm{Base}}_P$$
5		fveval1fvcl.r	$$⊢\phi \to R\in \mathrm{CRing}$$
6		fveval1fvcl.y	$$⊢\phi \to Y\in B$$
7		fveval1fvcl.m	$$⊢\phi \to M\in U$$
8		eqid	$$⊢R{\uparrow }_{𝑠}B=R{\uparrow }_{𝑠}B$$
9		eqid	$$⊢{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}={\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
10	3	fvexi	$$⊢B\in \mathrm{V}$$
11	10	a1i	$$⊢\phi \to B\in \mathrm{V}$$
12	1 2 8 3	evl1rhm	$$⊢R\in \mathrm{CRing}\to O\in \left(P\mathrm{RingHom}\left(R{\uparrow }_{𝑠}B\right)\right)$$
13	4 9	rhmf	$$⊢O\in \left(P\mathrm{RingHom}\left(R{\uparrow }_{𝑠}B\right)\right)\to O:U⟶{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
14	5 12 13	3syl	$$⊢\phi \to O:U⟶{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
15	14 7	ffvelcdmd	$$⊢\phi \to O\left(M\right)\in {\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
16	8 3 9 5 11 15	pwselbas	$$⊢\phi \to O\left(M\right):B⟶B$$
17	16 6	ffvelcdmd	$$⊢\phi \to O\left(M\right)\left(Y\right)\in B$$