Theorem dgraaval

Description: Value of the degree function on an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014) (Revised by AV, 29-Sep-2020)

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

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	|- ( a = A -> ( ( p ` a ) = 0 <-> ( p ` A ) = 0 ) )
2	1	anbi2d	|- ( a = A -> ( ( ( deg ` p ) = d /\ ( p ` a ) = 0 ) <-> ( ( deg ` p ) = d /\ ( p ` A ) = 0 ) ) )
3	2	rexbidv	|- ( a = A -> ( E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = d /\ ( p ` a ) = 0 ) <-> E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = d /\ ( p ` A ) = 0 ) ) )
4	3	rabbidv	|- ( a = A -> { d e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = d /\ ( p ` a ) = 0 ) } = { d e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = d /\ ( p ` A ) = 0 ) } )
5	4	infeq1d	|- ( a = A -> inf ( { d e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = d /\ ( p ` a ) = 0 ) } , RR , < ) = inf ( { d e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = d /\ ( p ` A ) = 0 ) } , RR , < ) )
6		df-dgraa	|- degAA = ( a e. AA |-> inf ( { d e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = d /\ ( p ` a ) = 0 ) } , RR , < ) )
7		ltso	|- < Or RR
8	7	infex	|- inf ( { d e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = d /\ ( p ` A ) = 0 ) } , RR , < ) e. _V
9	5 6 8	fvmpt	|- ( A e. AA -> ( degAA ` A ) = inf ( { d e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = d /\ ( p ` A ) = 0 ) } , RR , < ) )