Metamath Proof Explorer


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=eval1R
evl1fval1.b B=BaseR
Assertion evl1fval1 Q=RevalSub1B

Proof

Step Hyp Ref Expression
1 evl1fval1.q Q=eval1R
2 evl1fval1.b B=BaseR
3 1 2 evl1fval1lem RVQ=RevalSub1B
4 fvprc ¬RVeval1R=
5 1 4 eqtrid ¬RVQ=
6 reldmevls1 ReldomevalSub1
7 6 ovprc1 ¬RVRevalSub1B=
8 5 7 eqtr4d ¬RVQ=RevalSub1B
9 3 8 pm2.61i Q=RevalSub1B