This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑅 ) ‘ 𝐵 )