Theorem 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)

	Ref	Expression
Hypotheses	evlval.q	⊢ 𝑄 = ( 𝐼 eval 𝑅 )
	evlval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	evlval	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑅 ) ‘ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		evlval.q	⊢ 𝑄 = ( 𝐼 eval 𝑅 )
2		evlval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		oveq12	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑖 evalSub 𝑟 ) = ( 𝐼 evalSub 𝑅 ) )
4		fveq2	⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
5	4 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = 𝐵 )
6	5	adantl	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( Base ‘ 𝑟 ) = 𝐵 )
7	3 6	fveq12d	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( ( 𝑖 evalSub 𝑟 ) ‘ ( Base ‘ 𝑟 ) ) = ( ( 𝐼 evalSub 𝑅 ) ‘ 𝐵 ) )
8		df-evl	⊢ eval = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( ( 𝑖 evalSub 𝑟 ) ‘ ( Base ‘ 𝑟 ) ) )
9		fvex	⊢ ( ( 𝐼 evalSub 𝑅 ) ‘ 𝐵 ) ∈ V
10	7 8 9	ovmpoa	⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 eval 𝑅 ) = ( ( 𝐼 evalSub 𝑅 ) ‘ 𝐵 ) )
11	8	mpondm0	⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 eval 𝑅 ) = ∅ )
12		0fv	⊢ ( ∅ ‘ 𝐵 ) = ∅
13	11 12	eqtr4di	⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 eval 𝑅 ) = ( ∅ ‘ 𝐵 ) )
14		reldmevls	⊢ Rel dom evalSub
15	14	ovprc	⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 evalSub 𝑅 ) = ∅ )
16	15	fveq1d	⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( ( 𝐼 evalSub 𝑅 ) ‘ 𝐵 ) = ( ∅ ‘ 𝐵 ) )
17	13 16	eqtr4d	⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 eval 𝑅 ) = ( ( 𝐼 evalSub 𝑅 ) ‘ 𝐵 ) )
18	10 17	pm2.61i	⊢ ( 𝐼 eval 𝑅 ) = ( ( 𝐼 evalSub 𝑅 ) ‘ 𝐵 )
19	1 18	eqtri	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑅 ) ‘ 𝐵 )