Definition df-evl 20289

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 = (𝑖 ∈ V, 𝑟 ∈ V ↦ ((𝑖 evalSub 𝑟)‘(Base‘𝑟)))

Distinct variable group:   𝑖,𝑟

Detailed syntax breakdown of Definition df-evl

Step	Hyp	Ref	Expression
1		cevl 20287	. 2 class eval
2		vi	. . 3 setvar 𝑖
3		vr	. . 3 setvar 𝑟
4		cvv 3496	. . 3 class V
5	3	cv 1536	. . . . 5 class 𝑟
6		cbs 16485	. . . . 5 class Base
7	5, 6	cfv 6357	. . . 4 class (Base‘𝑟)
8	2	cv 1536	. . . . 5 class 𝑖
9		ces 20286	. . . . 5 class evalSub
10	8, 5, 9	co 7158	. . . 4 class (𝑖 evalSub 𝑟)
11	7, 10	cfv 6357	. . 3 class ((𝑖 evalSub 𝑟)‘(Base‘𝑟))
12	2, 3, 4, 4, 11	cmpo 7160	. 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ ((𝑖 evalSub 𝑟)‘(Base‘𝑟)))
13	1, 12	wceq 1537	1 wff eval = (𝑖 ∈ V, 𝑟 ∈ V ↦ ((𝑖 evalSub 𝑟)‘(Base‘𝑟)))

This definition is referenced by:  evlval  20310  evl1fval  20493  mzpmfp  39351