![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-evl | Structured version Visualization version GIF version |
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 |
---|---|
df-evl | ⊢ eval = (𝑖 ∈ V, 𝑟 ∈ V ↦ ((𝑖 evalSub 𝑟)‘(Base‘𝑟))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cevl 21634 | . 2 class eval | |
2 | vi | . . 3 setvar 𝑖 | |
3 | vr | . . 3 setvar 𝑟 | |
4 | cvv 3475 | . . 3 class V | |
5 | 3 | cv 1541 | . . . . 5 class 𝑟 |
6 | cbs 17144 | . . . . 5 class Base | |
7 | 5, 6 | cfv 6544 | . . . 4 class (Base‘𝑟) |
8 | 2 | cv 1541 | . . . . 5 class 𝑖 |
9 | ces 21633 | . . . . 5 class evalSub | |
10 | 8, 5, 9 | co 7409 | . . . 4 class (𝑖 evalSub 𝑟) |
11 | 7, 10 | cfv 6544 | . . 3 class ((𝑖 evalSub 𝑟)‘(Base‘𝑟)) |
12 | 2, 3, 4, 4, 11 | cmpo 7411 | . 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ ((𝑖 evalSub 𝑟)‘(Base‘𝑟))) |
13 | 1, 12 | wceq 1542 | 1 wff eval = (𝑖 ∈ V, 𝑟 ∈ V ↦ ((𝑖 evalSub 𝑟)‘(Base‘𝑟))) |
Colors of variables: wff setvar class |
This definition is referenced by: evlval 21658 evl1fval 21847 mzpmfp 41485 |
Copyright terms: Public domain | W3C validator |