Definition df-minply 32752

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 32751	. 2 class minPoly
2		ve	. . 3 setvar 𝑒
3		vf	. . 3 setvar 𝑓
4		cvv 3474	. . 3 class V
5		vx	. . . 4 setvar 𝑥
6	2	cv 1540	. . . . 5 class 𝑒
7		cbs 17143	. . . . 5 class Base
8	6, 7	cfv 6543	. . . 4 class (Base‘𝑒)
9	5	cv 1540	. . . . . . . 8 class 𝑥
10		vp	. . . . . . . . . 10 setvar 𝑝
11	10	cv 1540	. . . . . . . . 9 class 𝑝
12	3	cv 1540	. . . . . . . . . 10 class 𝑓
13		ces1 21831	. . . . . . . . . 10 class evalSub1
14	6, 12, 13	co 7408	. . . . . . . . 9 class (𝑒 evalSub1 𝑓)
15	11, 14	cfv 6543	. . . . . . . 8 class ((𝑒 evalSub1 𝑓)‘𝑝)
16	9, 15	cfv 6543	. . . . . . 7 class (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥)
17		c0g 17384	. . . . . . . 8 class 0g
18	6, 17	cfv 6543	. . . . . . 7 class (0g‘𝑒)
19	16, 18	wceq 1541	. . . . . 6 wff (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)
20	14	cdm 5676	. . . . . 6 class dom (𝑒 evalSub1 𝑓)
21	19, 10, 20	crab 3432	. . . . 5 class {𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)}
22		cress 17172	. . . . . . 7 class ↾s
23	6, 12, 22	co 7408	. . . . . 6 class (𝑒 ↾s 𝑓)
24		cig1p 25646	. . . . . 6 class idlGen1p
25	23, 24	cfv 6543	. . . . 5 class (idlGen1p‘(𝑒 ↾s 𝑓))
26	21, 25	cfv 6543	. . . 4 class ((idlGen1p‘(𝑒 ↾s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)})
27	5, 8, 26	cmpt 5231	. . 3 class (𝑥 ∈ (Base‘𝑒) ↦ ((idlGen1p‘(𝑒 ↾s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)}))
28	2, 3, 4, 4, 27	cmpo 7410	. 2 class (𝑒 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑒) ↦ ((idlGen1p‘(𝑒 ↾s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)})))
29	1, 28	wceq 1541	1 wff minPoly = (𝑒 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑒) ↦ ((idlGen1p‘(𝑒 ↾s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)})))

This definition is referenced by:  minplyval  32761