Metamath Proof Explorer

Definition df-dgraa

Description: Define the degree of an algebraic number as the smallest degree of any nonzero polynomial which has said number as a root. (Contributed by Stefan O'Rear, 25-Nov-2014) (Revised by AV, 29-Sep-2020)

Ref Expression
Assertion df-dgraa 
|- degAA = ( x e. AA |-> inf ( { d e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = d /\ ( p ` x ) = 0 ) } , RR , < ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdgraa 
 |-  degAA
1 vx 
 |-  x
2 caa 
 |-  AA
3 vd 
 |-  d
4 cn 
 |-  NN
5 vp 
 |-  p
6 cply 
 |-  Poly
7 cq 
 |-  QQ
8 7 6 cfv 
 |-  ( Poly ` QQ )
9 c0p 
 |-  0p
10 9 csn 
 |-  { 0p }
11 8 10 cdif 
 |-  ( ( Poly ` QQ ) \ { 0p } )
12 cdgr 
 |-  deg
13 5 cv 
 |-  p
14 13 12 cfv 
 |-  ( deg ` p )
15 3 cv 
 |-  d
16 14 15 wceq 
 |-  ( deg ` p ) = d
17 1 cv 
 |-  x
18 17 13 cfv 
 |-  ( p ` x )
19 cc0 
 |-  0
20 18 19 wceq 
 |-  ( p ` x ) = 0
21 16 20 wa 
 |-  ( ( deg ` p ) = d /\ ( p ` x ) = 0 )
22 21 5 11 wrex 
 |-  E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = d /\ ( p ` x ) = 0 )
23 22 3 4 crab 
 |-  { d e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = d /\ ( p ` x ) = 0 ) }
24 cr 
 |-  RR
25 clt 
 |-  <
26 23 24 25 cinf 
 |-  inf ( { d e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = d /\ ( p ` x ) = 0 ) } , RR , < )
27 1 2 26 cmpt 
 |-  ( x e. AA |-> inf ( { d e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = d /\ ( p ` x ) = 0 ) } , RR , < ) )
28 0 27 wceq 
 |-  degAA = ( x e. AA |-> inf ( { d e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = d /\ ( p ` x ) = 0 ) } , RR , < ) )