Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-minply Structured version   Visualization version   GIF version

Definition df-minply 33693
Description: Define the minimal polynomial builder function. (Contributed by Thierry Arnoux, 19-Jan-2025.)
Assertion
Ref Expression
df-minply minPoly = (𝑒 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑒) ↦ ((idlGen1p‘(𝑒s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g𝑒)})))
Distinct variable group:   𝑒,𝑓,𝑝,𝑥

Detailed syntax breakdown of Definition df-minply
StepHypRef Expression
1 cminply 33692 . 2 class minPoly
2 ve . . 3 setvar 𝑒
3 vf . . 3 setvar 𝑓
4 cvv 3488 . . 3 class V
5 vx . . . 4 setvar 𝑥
62cv 1536 . . . . 5 class 𝑒
7 cbs 17258 . . . . 5 class Base
86, 7cfv 6573 . . . 4 class (Base‘𝑒)
95cv 1536 . . . . . . . 8 class 𝑥
10 vp . . . . . . . . . 10 setvar 𝑝
1110cv 1536 . . . . . . . . 9 class 𝑝
123cv 1536 . . . . . . . . . 10 class 𝑓
13 ces1 22338 . . . . . . . . . 10 class evalSub1
146, 12, 13co 7448 . . . . . . . . 9 class (𝑒 evalSub1 𝑓)
1511, 14cfv 6573 . . . . . . . 8 class ((𝑒 evalSub1 𝑓)‘𝑝)
169, 15cfv 6573 . . . . . . 7 class (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥)
17 c0g 17499 . . . . . . . 8 class 0g
186, 17cfv 6573 . . . . . . 7 class (0g𝑒)
1916, 18wceq 1537 . . . . . 6 wff (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g𝑒)
2014cdm 5700 . . . . . 6 class dom (𝑒 evalSub1 𝑓)
2119, 10, 20crab 3443 . . . . 5 class {𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g𝑒)}
22 cress 17287 . . . . . . 7 class s
236, 12, 22co 7448 . . . . . 6 class (𝑒s 𝑓)
24 cig1p 26189 . . . . . 6 class idlGen1p
2523, 24cfv 6573 . . . . 5 class (idlGen1p‘(𝑒s 𝑓))
2621, 25cfv 6573 . . . 4 class ((idlGen1p‘(𝑒s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g𝑒)})
275, 8, 26cmpt 5249 . . 3 class (𝑥 ∈ (Base‘𝑒) ↦ ((idlGen1p‘(𝑒s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g𝑒)}))
282, 3, 4, 4, 27cmpo 7450 . 2 class (𝑒 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑒) ↦ ((idlGen1p‘(𝑒s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g𝑒)})))
291, 28wceq 1537 1 wff minPoly = (𝑒 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑒) ↦ ((idlGen1p‘(𝑒s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g𝑒)})))
Colors of variables: wff setvar class
This definition is referenced by:  minplyval  33698
  Copyright terms: Public domain W3C validator