Definition df-evl

Description: A simplification of evalSub when the evaluation ring is the same as the coefficient ring. (Contributed by Stefan O'Rear, 19-Mar-2015)

	Ref	Expression
Assertion	df-evl	$$⊢\mathrm{eval}=\left(i\in \mathrm{V},r\in \mathrm{V}⟼\left(i\mathrm{evalSub}r\right)\left({\mathrm{Base}}_r\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cevl	$$class\mathrm{eval}$$
1		vi	$$setvari$$
2		cvv	$$class\mathrm{V}$$
3		vr	$$setvarr$$
4	1	cv	$$setvari$$
5		ces	$$class\mathrm{evalSub}$$
6	3	cv	$$setvarr$$
7	4 6 5	co	$$class\left(i\mathrm{evalSub}r\right)$$
8		cbs	$$class\mathrm{Base}$$
9	6 8	cfv	$$class{\mathrm{Base}}_r$$
10	9 7	cfv	$$class\left(i\mathrm{evalSub}r\right)\left({\mathrm{Base}}_r\right)$$
11	1 3 2 2 10	cmpo	$$class\left(i\in \mathrm{V},r\in \mathrm{V}⟼\left(i\mathrm{evalSub}r\right)\left({\mathrm{Base}}_r\right)\right)$$
12	0 11	wceq	$$wff\mathrm{eval}=\left(i\in \mathrm{V},r\in \mathrm{V}⟼\left(i\mathrm{evalSub}r\right)\left({\mathrm{Base}}_r\right)\right)$$