Metamath Proof Explorer

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 \in V, r \in V ⟼ (i evalSub r) ({Base}_{r}))$

Detailed syntax breakdown

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