Definition df-minply

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

	Ref	Expression
Assertion	df-minply	Could not format assertion : No typesetting found for |- minPoly = ( e e. _V , f e. _V |-> ( x e. ( Base ` e ) |-> ( ( idlGen1p ` ( e |`s f ) ) ` { p e. dom ( e evalSub1 f ) | ( ( ( e evalSub1 f ) ` p ) ` x ) = ( 0g ` e ) } ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cminply	Could not format minPoly : No typesetting found for class minPoly with typecode class
1		ve	$$setvare$$
2		cvv	$$class\mathrm{V}$$
3		vf	$$setvarf$$
4		vx	$$setvarx$$
5		cbs	$$class\mathrm{Base}$$
6	1	cv	$$setvare$$
7	6 5	cfv	$$class{\mathrm{Base}}_e$$
8		cig1p	$$class{idlGen}_{\mathrm{1p}}$$
9		cress	$$class{\upharpoonright }_{𝑠}$$
10	3	cv	$$setvarf$$
11	6 10 9	co	$$class\left(e{\upharpoonright }_{𝑠}f\right)$$
12	11 8	cfv	$$class{idlGen}_{\mathrm{1p}}\left(e{\upharpoonright }_{𝑠}f\right)$$
13		vp	$$setvarp$$
14		ces1	$$class{\mathrm{evalSub}}_1$$
15	6 10 14	co	$$class\left(e{\mathrm{evalSub}}_{1}f\right)$$
16	15	cdm	$$class\mathrm{dom}\left(e{\mathrm{evalSub}}_{1}f\right)$$
17	13	cv	$$setvarp$$
18	17 15	cfv	$$class\left(e{\mathrm{evalSub}}_{1}f\right)\left(p\right)$$
19	4	cv	$$setvarx$$
20	19 18	cfv	$$class\left(e{\mathrm{evalSub}}_{1}f\right)\left(p\right)\left(x\right)$$
21		c0g	$$class{0}_{𝑔}$$
22	6 21	cfv	$$class{0}_e$$
23	20 22	wceq	$$wff\left(e{\mathrm{evalSub}}_{1}f\right)\left(p\right)\left(x\right)=0_e$$
24	23 13 16	crab	$$class\left\{p\in \mathrm{dom}\left(e{\mathrm{evalSub}}_{1}f\right)|\left(e{\mathrm{evalSub}}_{1}f\right)\left(p\right)\left(x\right)=0_e\right\}$$
25	24 12	cfv	$$class{idlGen}_{\mathrm{1p}}\left(e{\upharpoonright }_{𝑠}f\right)\left(\left\{p\in \mathrm{dom}\left(e{\mathrm{evalSub}}_{1}f\right)|\left(e{\mathrm{evalSub}}_{1}f\right)\left(p\right)\left(x\right)=0_e\right\}\right)$$
26	4 7 25	cmpt	$$class\left(x\in {\mathrm{Base}}_e⟼{idlGen}_{\mathrm{1p}}\left(e{\upharpoonright }_{𝑠}f\right)\left(\left\{p\in \mathrm{dom}\left(e{\mathrm{evalSub}}_{1}f\right)|\left(e{\mathrm{evalSub}}_{1}f\right)\left(p\right)\left(x\right)=0_e\right\}\right)\right)$$
27	1 3 2 2 26	cmpo	$$class\left(e\in \mathrm{V},f\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_e⟼{idlGen}_{\mathrm{1p}}\left(e{\upharpoonright }_{𝑠}f\right)\left(\left\{p\in \mathrm{dom}\left(e{\mathrm{evalSub}}_{1}f\right)|\left(e{\mathrm{evalSub}}_{1}f\right)\left(p\right)\left(x\right)=0_e\right\}\right)\right)\right)$$
28	0 27	wceq	Could not format minPoly = ( e e. _V , f e. _V |-> ( x e. ( Base ` e ) |-> ( ( idlGen1p ` ( e |`s f ) ) ` { p e. dom ( e evalSub1 f ) | ( ( ( e evalSub1 f ) ` p ) ` x ) = ( 0g ` e ) } ) ) ) : No typesetting found for wff minPoly = ( e e. _V , f e. _V |-> ( x e. ( Base ` e ) |-> ( ( idlGen1p ` ( e |`s f ) ) ` { p e. dom ( e evalSub1 f ) | ( ( ( e evalSub1 f ) ` p ) ` x ) = ( 0g ` e ) } ) ) ) with typecode wff