Definition df-minply 33743

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

Step	Hyp	Ref	Expression
1		cminply 33742	. 2 class minPoly
2		ve	. . 3 setvar 𝑒
3		vf	. . 3 setvar 𝑓
4		cvv 3480	. . 3 class V
5		vx	. . . 4 setvar 𝑥
6	2	cv 1539	. . . . 5 class 𝑒
7		cbs 17247	. . . . 5 class Base
8	6, 7	cfv 6561	. . . 4 class (Base‘𝑒)
9	5	cv 1539	. . . . . . . 8 class 𝑥
10		vp	. . . . . . . . . 10 setvar 𝑝
11	10	cv 1539	. . . . . . . . 9 class 𝑝
12	3	cv 1539	. . . . . . . . . 10 class 𝑓
13		ces1 22317	. . . . . . . . . 10 class evalSub1
14	6, 12, 13	co 7431	. . . . . . . . 9 class (𝑒 evalSub1 𝑓)
15	11, 14	cfv 6561	. . . . . . . 8 class ((𝑒 evalSub1 𝑓)‘𝑝)
16	9, 15	cfv 6561	. . . . . . 7 class (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥)
17		c0g 17484	. . . . . . . 8 class 0g
18	6, 17	cfv 6561	. . . . . . 7 class (0g‘𝑒)
19	16, 18	wceq 1540	. . . . . 6 wff (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)
20	14	cdm 5685	. . . . . 6 class dom (𝑒 evalSub1 𝑓)
21	19, 10, 20	crab 3436	. . . . 5 class {𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)}
22		cress 17274	. . . . . . 7 class ↾s
23	6, 12, 22	co 7431	. . . . . 6 class (𝑒 ↾s 𝑓)
24		cig1p 26169	. . . . . 6 class idlGen1p
25	23, 24	cfv 6561	. . . . 5 class (idlGen1p‘(𝑒 ↾s 𝑓))
26	21, 25	cfv 6561	. . . 4 class ((idlGen1p‘(𝑒 ↾s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)})
27	5, 8, 26	cmpt 5225	. . 3 class (𝑥 ∈ (Base‘𝑒) ↦ ((idlGen1p‘(𝑒 ↾s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)}))
28	2, 3, 4, 4, 27	cmpo 7433	. 2 class (𝑒 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑒) ↦ ((idlGen1p‘(𝑒 ↾s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)})))
29	1, 28	wceq 1540	1 wff minPoly = (𝑒 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑒) ↦ ((idlGen1p‘(𝑒 ↾s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)})))

This definition is referenced by:  minplyval  33748