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	|- eval = ( i e. _V , r e. _V |-> ( ( i evalSub r ) ` ( Base ` r ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cevl	|- eval
1		vi	|- i
2		cvv	|- _V
3		vr	|- r
4	1	cv	|- i
5		ces	|- evalSub
6	3	cv	|- r
7	4 6 5	co	|- ( i evalSub r )
8		cbs	|- Base
9	6 8	cfv	|- ( Base ` r )
10	9 7	cfv	|- ( ( i evalSub r ) ` ( Base ` r ) )
11	1 3 2 2 10	cmpo	|- ( i e. _V , r e. _V |-> ( ( i evalSub r ) ` ( Base ` r ) ) )
12	0 11	wceq	|- eval = ( i e. _V , r e. _V |-> ( ( i evalSub r ) ` ( Base ` r ) ) )