evlval

Description: Value of the simple/same ring evaluation map. (Contributed by Stefan O'Rear, 19-Mar-2015) (Revised by Mario Carneiro, 12-Jun-2015)

Step	Hyp	Ref	Expression
1		evlval.q	$⊢ Q = I eval R$
2		evlval.b	$⊢ B = {Base}_{R}$
3		oveq12	$⊢ (i = I \land r = R) \to i evalSub r = I evalSub R$
4		fveq2	$⊢ r = R \to {Base}_{r} = {Base}_{R}$
5	4 2	eqtr4di	$⊢ r = R \to {Base}_{r} = B$
6	5	adantl	$⊢ (i = I \land r = R) \to {Base}_{r} = B$
7	3 6	fveq12d	$⊢ (i = I \land r = R) \to (i evalSub r) ({Base}_{r}) = (I evalSub R) (B)$
8		df-evl	$⊢ eval = (i \in V, r \in V ⟼ (i evalSub r) ({Base}_{r}))$
9		fvex	$⊢ (I evalSub R) (B) \in V$
10	7 8 9	ovmpoa	$⊢ (I \in V \land R \in V) \to I eval R = (I evalSub R) (B)$
11	8	mpondm0	$⊢ \neg (I \in V \land R \in V) \to I eval R = \emptyset$
12		0fv	$⊢ \emptyset (B) = \emptyset$
13	11 12	eqtr4di	$⊢ \neg (I \in V \land R \in V) \to I eval R = \emptyset (B)$
14		reldmevls	$⊢ Rel dom evalSub$
15	14	ovprc	$⊢ \neg (I \in V \land R \in V) \to I evalSub R = \emptyset$
16	15	fveq1d	$⊢ \neg (I \in V \land R \in V) \to (I evalSub R) (B) = \emptyset (B)$
17	13 16	eqtr4d	$⊢ \neg (I \in V \land R \in V) \to I eval R = (I evalSub R) (B)$
18	10 17	pm2.61i	$⊢ I eval R = (I evalSub R) (B)$
19	1 18	eqtri	$⊢ Q = (I evalSub R) (B)$

Metamath Proof Explorer