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	⊢ 𝑄 = ( eval1 ‘ 𝑅 )
	evl1fval1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	evl1fval1	⊢ 𝑄 = ( 𝑅 evalSub1 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		evl1fval1.q	⊢ 𝑄 = ( eval1 ‘ 𝑅 )
2		evl1fval1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3	1 2	evl1fval1lem	⊢ ( 𝑅 ∈ V → 𝑄 = ( 𝑅 evalSub1 𝐵 ) )
4		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( eval1 ‘ 𝑅 ) = ∅ )
5	1 4	syl5eq	⊢ ( ¬ 𝑅 ∈ V → 𝑄 = ∅ )
6		reldmevls1	⊢ Rel dom evalSub1
7	6	ovprc1	⊢ ( ¬ 𝑅 ∈ V → ( 𝑅 evalSub1 𝐵 ) = ∅ )
8	5 7	eqtr4d	⊢ ( ¬ 𝑅 ∈ V → 𝑄 = ( 𝑅 evalSub1 𝐵 ) )
9	3 8	pm2.61i	⊢ 𝑄 = ( 𝑅 evalSub1 𝐵 )