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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cevl	⊢ eval
1		vi	⊢ 𝑖
2		cvv	⊢ V
3		vr	⊢ 𝑟
4	1	cv	⊢ 𝑖
5		ces	⊢ evalSub
6	3	cv	⊢ 𝑟
7	4 6 5	co	⊢ ( 𝑖 evalSub 𝑟 )
8		cbs	⊢ Base
9	6 8	cfv	⊢ ( Base ‘ 𝑟 )
10	9 7	cfv	⊢ ( ( 𝑖 evalSub 𝑟 ) ‘ ( Base ‘ 𝑟 ) )
11	1 3 2 2 10	cmpo	⊢ ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( ( 𝑖 evalSub 𝑟 ) ‘ ( Base ‘ 𝑟 ) ) )
12	0 11	wceq	⊢ eval = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( ( 𝑖 evalSub 𝑟 ) ‘ ( Base ‘ 𝑟 ) ) )