Metamath Proof Explorer

Definition df-minply

Description: Define the minimal polynomial builder function. (Contributed by Thierry Arnoux, 19-Jan-2025)

Ref Expression
Assertion df-minply ⊢ minPoly = e ∈ V , f ∈ V ⟼ x ∈ Base e ⟼ idlGen 1p ⁡ e ↾ 𝑠 f ⁡ p ∈ dom ⁡ e evalSub 1 f | e evalSub 1 f ⁡ p ⁡ x = 0 e

Detailed syntax breakdown

Step Hyp Ref Expression
0 cminply class minPoly
1 ve setvar e
2 cvv class V
3 vf setvar f
4 vx setvar x
5 cbs class Base
6 1 cv setvar e
7 6 5 cfv class Base e
8 cig1p class idlGen 1p
9 cress class ↾ 𝑠
10 3 cv setvar f
11 6 10 9 co class e ↾ 𝑠 f
12 11 8 cfv class idlGen 1p ⁡ e ↾ 𝑠 f
13 vp setvar p
14 ces1 class evalSub 1
15 6 10 14 co class e evalSub 1 f
16 15 cdm class dom ⁡ e evalSub 1 f
17 13 cv setvar p
18 17 15 cfv class e evalSub 1 f ⁡ p
19 4 cv setvar x
20 19 18 cfv class e evalSub 1 f ⁡ p ⁡ x
21 c0g class 0 𝑔
22 6 21 cfv class 0 e
23 20 22 wceq wff e evalSub 1 f ⁡ p ⁡ x = 0 e
24 23 13 16 crab class p ∈ dom ⁡ e evalSub 1 f | e evalSub 1 f ⁡ p ⁡ x = 0 e
25 24 12 cfv class idlGen 1p ⁡ e ↾ 𝑠 f ⁡ p ∈ dom ⁡ e evalSub 1 f | e evalSub 1 f ⁡ p ⁡ x = 0 e
26 4 7 25 cmpt class x ∈ Base e ⟼ idlGen 1p ⁡ e ↾ 𝑠 f ⁡ p ∈ dom ⁡ e evalSub 1 f | e evalSub 1 f ⁡ p ⁡ x = 0 e
27 1 3 2 2 26 cmpo class e ∈ V , f ∈ V ⟼ x ∈ Base e ⟼ idlGen 1p ⁡ e ↾ 𝑠 f ⁡ p ∈ dom ⁡ e evalSub 1 f | e evalSub 1 f ⁡ p ⁡ x = 0 e
28 0 27 wceq wff minPoly = e ∈ V , f ∈ V ⟼ x ∈ Base e ⟼ idlGen 1p ⁡ e ↾ 𝑠 f ⁡ p ∈ dom ⁡ e evalSub 1 f | e evalSub 1 f ⁡ p ⁡ x = 0 e