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 32424
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 32423 . 2 class minPoly
2 ve . . 3 setvar 𝑒
3 vf . . 3 setvar 𝑓
4 cvv 3444 . . 3 class V
5 vx . . . 4 setvar 𝑥
62cv 1541 . . . . 5 class 𝑒
7 cbs 17088 . . . . 5 class Base
86, 7cfv 6497 . . . 4 class (Base‘𝑒)
95cv 1541 . . . . . . . 8 class 𝑥
10 vp . . . . . . . . . 10 setvar 𝑝
1110cv 1541 . . . . . . . . 9 class 𝑝
123cv 1541 . . . . . . . . . 10 class 𝑓
13 ces1 21695 . . . . . . . . . 10 class evalSub1
146, 12, 13co 7358 . . . . . . . . 9 class (𝑒 evalSub1 𝑓)
1511, 14cfv 6497 . . . . . . . 8 class ((𝑒 evalSub1 𝑓)‘𝑝)
169, 15cfv 6497 . . . . . . 7 class (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥)
17 c0g 17326 . . . . . . . 8 class 0g
186, 17cfv 6497 . . . . . . 7 class (0g𝑒)
1916, 18wceq 1542 . . . . . 6 wff (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g𝑒)
2014cdm 5634 . . . . . 6 class dom (𝑒 evalSub1 𝑓)
2119, 10, 20crab 3406 . . . . 5 class {𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g𝑒)}
22 cress 17117 . . . . . . 7 class s
236, 12, 22co 7358 . . . . . 6 class (𝑒s 𝑓)
24 cig1p 25510 . . . . . 6 class idlGen1p
2523, 24cfv 6497 . . . . 5 class (idlGen1p‘(𝑒s 𝑓))
2621, 25cfv 6497 . . . 4 class ((idlGen1p‘(𝑒s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g𝑒)})
275, 8, 26cmpt 5189 . . 3 class (𝑥 ∈ (Base‘𝑒) ↦ ((idlGen1p‘(𝑒s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g𝑒)}))
282, 3, 4, 4, 27cmpo 7360 . 2 class (𝑒 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑒) ↦ ((idlGen1p‘(𝑒s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g𝑒)})))
291, 28wceq 1542 1 wff minPoly = (𝑒 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑒) ↦ ((idlGen1p‘(𝑒s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g𝑒)})))
Colors of variables: wff setvar class
This definition is referenced by:  minplyval  32429
  Copyright terms: Public domain W3C validator