Theorem evl1fval1

Description: Value of the simple/same ring evaluation map function for univariate polynomials. (Contributed by AV, 11-Sep-2019)

	Ref	Expression
Hypotheses	evl1fval1.q	|- Q = ( eval1 ` R )
	evl1fval1.b	|- B = ( Base ` R )
Assertion	evl1fval1	|- Q = ( R evalSub1 B )

Proof

Step	Hyp	Ref	Expression
1		evl1fval1.q	|- Q = ( eval1 ` R )
2		evl1fval1.b	|- B = ( Base ` R )
3	1 2	evl1fval1lem	|- ( R e. _V -> Q = ( R evalSub1 B ) )
4		fvprc	|- ( -. R e. _V -> ( eval1 ` R ) = (/) )
5	1 4	eqtrid	|- ( -. R e. _V -> Q = (/) )
6		reldmevls1	|- Rel dom evalSub1
7	6	ovprc1	|- ( -. R e. _V -> ( R evalSub1 B ) = (/) )
8	5 7	eqtr4d	|- ( -. R e. _V -> Q = ( R evalSub1 B ) )
9	3 8	pm2.61i	|- Q = ( R evalSub1 B )