Step | Hyp | Ref
| Expression |
1 | | cminply 32423 |
. 2
class
minPoly |
2 | | ve |
. . 3
setvar 𝑒 |
3 | | vf |
. . 3
setvar 𝑓 |
4 | | cvv 3444 |
. . 3
class
V |
5 | | vx |
. . . 4
setvar 𝑥 |
6 | 2 | cv 1541 |
. . . . 5
class 𝑒 |
7 | | cbs 17088 |
. . . . 5
class
Base |
8 | 6, 7 | cfv 6497 |
. . . 4
class
(Base‘𝑒) |
9 | 5 | cv 1541 |
. . . . . . . 8
class 𝑥 |
10 | | vp |
. . . . . . . . . 10
setvar 𝑝 |
11 | 10 | cv 1541 |
. . . . . . . . 9
class 𝑝 |
12 | 3 | cv 1541 |
. . . . . . . . . 10
class 𝑓 |
13 | | ces1 21695 |
. . . . . . . . . 10
class
evalSub1 |
14 | 6, 12, 13 | co 7358 |
. . . . . . . . 9
class (𝑒 evalSub1 𝑓) |
15 | 11, 14 | cfv 6497 |
. . . . . . . 8
class ((𝑒 evalSub1 𝑓)‘𝑝) |
16 | 9, 15 | cfv 6497 |
. . . . . . 7
class (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) |
17 | | c0g 17326 |
. . . . . . . 8
class
0g |
18 | 6, 17 | cfv 6497 |
. . . . . . 7
class
(0g‘𝑒) |
19 | 16, 18 | wceq 1542 |
. . . . . 6
wff (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g‘𝑒) |
20 | 14 | cdm 5634 |
. . . . . 6
class dom
(𝑒 evalSub1
𝑓) |
21 | 19, 10, 20 | crab 3406 |
. . . . 5
class {𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)} |
22 | | cress 17117 |
. . . . . . 7
class
↾s |
23 | 6, 12, 22 | co 7358 |
. . . . . 6
class (𝑒 ↾s 𝑓) |
24 | | cig1p 25510 |
. . . . . 6
class
idlGen1p |
25 | 23, 24 | cfv 6497 |
. . . . 5
class
(idlGen1p‘(𝑒 ↾s 𝑓)) |
26 | 21, 25 | cfv 6497 |
. . . 4
class
((idlGen1p‘(𝑒 ↾s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)}) |
27 | 5, 8, 26 | cmpt 5189 |
. . 3
class (𝑥 ∈ (Base‘𝑒) ↦
((idlGen1p‘(𝑒 ↾s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)})) |
28 | 2, 3, 4, 4, 27 | cmpo 7360 |
. 2
class (𝑒 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑒) ↦ ((idlGen1p‘(𝑒 ↾s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)}))) |
29 | 1, 28 | wceq 1542 |
1
wff minPoly =
(𝑒 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑒) ↦
((idlGen1p‘(𝑒 ↾s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)}))) |