Definition df-evl 19507

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

Assertion

Ref	Expression
df-evl	|- eval = ( i e. _V , r e. _V |-> ( ( i evalSub r ) ` ( Base ` r ) ) )

Distinct variable group:   i, r

Detailed syntax breakdown of Definition df-evl

Step	Hyp	Ref	Expression
1		cevl 19505	. 2 class eval
2		vi	. . 3 setvar i
3		vr	. . 3 setvar r
4		cvv 3200	. . 3 class _V
5	3	cv 1482	. . . . 5 class r
6		cbs 15857	. . . . 5 class Base
7	5, 6	cfv 5888	. . . 4 class ( Base ` r )
8	2	cv 1482	. . . . 5 class i
9		ces 19504	. . . . 5 class evalSub
10	8, 5, 9	co 6650	. . . 4 class ( i evalSub r )
11	7, 10	cfv 5888	. . 3 class ( ( i evalSub r ) ` ( Base ` r ) )
12	2, 3, 4, 4, 11	cmpt2 6652	. 2 class ( i e. _V , r e. _V |-> ( ( i evalSub r ) ` ( Base ` r ) ) )
13	1, 12	wceq 1483	1 wff eval = ( i e. _V , r e. _V |-> ( ( i evalSub r ) ` ( Base ` r ) ) )

This definition is referenced by:  evlval  19524  evl1fval  19692  mzpmfp  37310