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 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 ) } ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cminply 
 |-  minPoly
1 ve 
 |-  e
2 cvv 
 |-  _V
3 vf 
 |-  f
4 vx 
 |-  x
5 cbs 
 |-  Base
6 1 cv 
 |-  e
7 6 5 cfv 
 |-  ( Base ` e )
8 cig1p 
 |-  idlGen1p
9 cress 
 |-  |`s
10 3 cv 
 |-  f
11 6 10 9 co 
 |-  ( e |`s f )
12 11 8 cfv 
 |-  ( idlGen1p ` ( e |`s f ) )
13 vp 
 |-  p
14 ces1 
 |-  evalSub1
15 6 10 14 co 
 |-  ( e evalSub1 f )
16 15 cdm 
 |-  dom ( e evalSub1 f )
17 13 cv 
 |-  p
18 17 15 cfv 
 |-  ( ( e evalSub1 f ) ` p )
19 4 cv 
 |-  x
20 19 18 cfv 
 |-  ( ( ( e evalSub1 f ) ` p ) ` x )
21 c0g 
 |-  0g
22 6 21 cfv 
 |-  ( 0g ` e )
23 20 22 wceq 
 |-  ( ( ( e evalSub1 f ) ` p ) ` x ) = ( 0g ` e )
24 23 13 16 crab 
 |-  { p e. dom ( e evalSub1 f ) | ( ( ( e evalSub1 f ) ` p ) ` x ) = ( 0g ` e ) }
25 24 12 cfv 
 |-  ( ( idlGen1p ` ( e |`s f ) ) ` { p e. dom ( e evalSub1 f ) | ( ( ( e evalSub1 f ) ` p ) ` x ) = ( 0g ` e ) } )
26 4 7 25 cmpt 
 |-  ( x e. ( Base ` e ) |-> ( ( idlGen1p ` ( e |`s f ) ) ` { p e. dom ( e evalSub1 f ) | ( ( ( e evalSub1 f ) ` p ) ` x ) = ( 0g ` e ) } ) )
27 1 3 2 2 26 cmpo 
 |-  ( 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 ) } ) ) )
28 0 27 wceq 
 |-  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 ) } ) ) )