Theorem reldmevls

Description: Well-behaved binary operation property of evalSub . (Contributed by Stefan O'Rear, 19-Mar-2015)

	Ref	Expression
Assertion	reldmevls	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{evalSub}$$

Proof

Step	Hyp	Ref	Expression
1		df-evls	$$⊢\mathrm{evalSub}=\left(i\in \mathrm{V},s\in \mathrm{CRing}⟼⦋{\mathrm{Base}}_s/b⦌\left(r\in \mathrm{SubRing}\left(s\right)⟼⦋\left(i\mathrm{mPoly}\left(s{\upharpoonright }_{𝑠}r\right)\right)/w⦌\left(\iota f\in \left(w\mathrm{RingHom}\left(s{\uparrow }_{𝑠}\left(b^i\right)\right)\right)|\left(f\circ \mathrm{algSc}\left(w\right)=\left(x\in r⟼\left(b^i\right)\times \left\{x\right\}\right)\wedge f\circ \left(i\mathrm{mVar}\left(s{\upharpoonright }_{𝑠}r\right)\right)=\left(x\in i⟼\left(g\in \left(b^i\right)⟼g\left(x\right)\right)\right)\right)\right)\right)\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{evalSub}$$