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 = ( eval1 ` R )
	fveval1fvcl.p	|- P = ( Poly1 ` R )
	fveval1fvcl.b	|- B = ( Base ` R )
	fveval1fvcl.u	|- U = ( Base ` P )
	fveval1fvcl.r	|- ( ph -> R e. CRing )
	fveval1fvcl.y	|- ( ph -> Y e. B )
	fveval1fvcl.m	|- ( ph -> M e. U )
Assertion	fveval1fvcl	|- ( ph -> ( ( O ` M ) ` Y ) e. B )

Proof

Step	Hyp	Ref	Expression
1		fveval1fvcl.q	|- O = ( eval1 ` R )
2		fveval1fvcl.p	|- P = ( Poly1 ` R )
3		fveval1fvcl.b	|- B = ( Base ` R )
4		fveval1fvcl.u	|- U = ( Base ` P )
5		fveval1fvcl.r	|- ( ph -> R e. CRing )
6		fveval1fvcl.y	|- ( ph -> Y e. B )
7		fveval1fvcl.m	|- ( ph -> M e. U )
8		eqid	|- ( R ^s B ) = ( R ^s B )
9		eqid	|- ( Base ` ( R ^s B ) ) = ( Base ` ( R ^s B ) )
10	3	fvexi	|- B e. _V
11	10	a1i	|- ( ph -> B e. _V )
12	1 2 8 3	evl1rhm	|- ( R e. CRing -> O e. ( P RingHom ( R ^s B ) ) )
13	4 9	rhmf	|- ( O e. ( P RingHom ( R ^s B ) ) -> O : U --> ( Base ` ( R ^s B ) ) )
14	5 12 13	3syl	|- ( ph -> O : U --> ( Base ` ( R ^s B ) ) )
15	14 7	ffvelrnd	|- ( ph -> ( O ` M ) e. ( Base ` ( R ^s B ) ) )
16	8 3 9 5 11 15	pwselbas	|- ( ph -> ( O ` M ) : B --> B )
17	16 6	ffvelrnd	|- ( ph -> ( ( O ` M ) ` Y ) e. B )