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={\mathrm{eval}}_1\left(R\right)$$
	evl1fval1.b	$$⊢B={\mathrm{Base}}_R$$
Assertion	evl1fval1	$$⊢Q=R{\mathrm{evalSub}}_{1}B$$

Proof

Step	Hyp	Ref	Expression
1		evl1fval1.q	$$⊢Q={\mathrm{eval}}_1\left(R\right)$$
2		evl1fval1.b	$$⊢B={\mathrm{Base}}_R$$
3	1 2	evl1fval1lem	$$⊢R\in \mathrm{V}\to Q=R{\mathrm{evalSub}}_{1}B$$
4		fvprc	$$⊢\neg R\in \mathrm{V}\to {\mathrm{eval}}_1\left(R\right)=\varnothing$$
5	1 4	syl5eq	$$⊢\neg R\in \mathrm{V}\to Q=\varnothing$$
6		reldmevls1	$$⊢\mathrm{Rel}\mathrm{dom}{\mathrm{evalSub}}_1$$
7	6	ovprc1	$$⊢\neg R\in \mathrm{V}\to R{\mathrm{evalSub}}_{1}B=\varnothing$$
8	5 7	eqtr4d	$$⊢\neg R\in \mathrm{V}\to Q=R{\mathrm{evalSub}}_{1}B$$
9	3 8	pm2.61i	$$⊢Q=R{\mathrm{evalSub}}_{1}B$$