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\in 𝔸\to {\mathrm{deg}}_{𝔸}\left(A\right)=sup\left(\left\{d\in \mathbb{N}|\exists p\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\left(\mathrm{deg}\left(p\right)=d\wedge p\left(A\right)=0\right)\right\},ℝ,<\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	$$⊢a=A\to \left(p\left(a\right)=0\leftrightarrow p\left(A\right)=0\right)$$
2	1	anbi2d	$$⊢a=A\to \left(\left(\mathrm{deg}\left(p\right)=d\wedge p\left(a\right)=0\right)\leftrightarrow \left(\mathrm{deg}\left(p\right)=d\wedge p\left(A\right)=0\right)\right)$$
3	2	rexbidv	$$⊢a=A\to \left(\exists p\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\left(\mathrm{deg}\left(p\right)=d\wedge p\left(a\right)=0\right)\leftrightarrow \exists p\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\left(\mathrm{deg}\left(p\right)=d\wedge p\left(A\right)=0\right)\right)$$
4	3	rabbidv	$$⊢a=A\to \left\{d\in \mathbb{N}|\exists p\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\left(\mathrm{deg}\left(p\right)=d\wedge p\left(a\right)=0\right)\right\}=\left\{d\in \mathbb{N}|\exists p\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\left(\mathrm{deg}\left(p\right)=d\wedge p\left(A\right)=0\right)\right\}$$
5	4	infeq1d	$$⊢a=A\to sup\left(\left\{d\in \mathbb{N}|\exists p\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\left(\mathrm{deg}\left(p\right)=d\wedge p\left(a\right)=0\right)\right\},ℝ,<\right)=sup\left(\left\{d\in \mathbb{N}|\exists p\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\left(\mathrm{deg}\left(p\right)=d\wedge p\left(A\right)=0\right)\right\},ℝ,<\right)$$
6		df-dgraa	$$⊢{\mathrm{deg}}_{𝔸}=\left(a\in 𝔸⟼sup\left(\left\{d\in \mathbb{N}|\exists p\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\left(\mathrm{deg}\left(p\right)=d\wedge p\left(a\right)=0\right)\right\},ℝ,<\right)\right)$$
7		ltso	$$⊢<\mathrm{Or}ℝ$$
8	7	infex	$$⊢sup\left(\left\{d\in \mathbb{N}|\exists p\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\left(\mathrm{deg}\left(p\right)=d\wedge p\left(A\right)=0\right)\right\},ℝ,<\right)\in \mathrm{V}$$
9	5 6 8	fvmpt	$$⊢A\in 𝔸\to {\mathrm{deg}}_{𝔸}\left(A\right)=sup\left(\left\{d\in \mathbb{N}|\exists p\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\left(\mathrm{deg}\left(p\right)=d\wedge p\left(A\right)=0\right)\right\},ℝ,<\right)$$