Theorem dgrval

Description: Value of the degree function. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Hypothesis	dgrval.1	$$⊢A=\mathrm{coeff}\left(F\right)$$
Assertion	dgrval	$$⊢F\in \mathrm{Poly}\left(S\right)\to \mathrm{deg}\left(F\right)=sup\left(A^{-1}\left[ℂ\setminus \left\{0\right\}\right],{\mathbb{N}}_0,<\right)$$

Proof

Step	Hyp	Ref	Expression
1		dgrval.1	$$⊢A=\mathrm{coeff}\left(F\right)$$
2		plyssc	$$⊢\mathrm{Poly}\left(S\right)\subseteq \mathrm{Poly}\left(ℂ\right)$$
3	2	sseli	$$⊢F\in \mathrm{Poly}\left(S\right)\to F\in \mathrm{Poly}\left(ℂ\right)$$
4		fveq2	$$⊢f=F\to \mathrm{coeff}\left(f\right)=\mathrm{coeff}\left(F\right)$$
5	4 1	eqtr4di	$$⊢f=F\to \mathrm{coeff}\left(f\right)=A$$
6	5	cnveqd	$$⊢f=F\to {\mathrm{coeff}\left(f\right)}^{-1}=A^{-1}$$
7	6	imaeq1d	$$⊢f=F\to {\mathrm{coeff}\left(f\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right]=A^{-1}\left[ℂ\setminus \left\{0\right\}\right]$$
8	7	supeq1d	$$⊢f=F\to sup\left({\mathrm{coeff}\left(f\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right],{\mathbb{N}}_0,<\right)=sup\left(A^{-1}\left[ℂ\setminus \left\{0\right\}\right],{\mathbb{N}}_0,<\right)$$
9		df-dgr	$$⊢\mathrm{deg}=\left(f\in \mathrm{Poly}\left(ℂ\right)⟼sup\left({\mathrm{coeff}\left(f\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right],{\mathbb{N}}_0,<\right)\right)$$
10		nn0ssre	$$⊢{\mathbb{N}}_0\subseteq ℝ$$
11		ltso	$$⊢<\mathrm{Or}ℝ$$
12		soss	$$⊢{\mathbb{N}}_0\subseteq ℝ\to \left(<\mathrm{Or}ℝ\to <\mathrm{Or}{\mathbb{N}}_0\right)$$
13	10 11 12	mp2	$$⊢<\mathrm{Or}{\mathbb{N}}_0$$
14	13	supex	$$⊢sup\left(A^{-1}\left[ℂ\setminus \left\{0\right\}\right],{\mathbb{N}}_0,<\right)\in \mathrm{V}$$
15	8 9 14	fvmpt	$$⊢F\in \mathrm{Poly}\left(ℂ\right)\to \mathrm{deg}\left(F\right)=sup\left(A^{-1}\left[ℂ\setminus \left\{0\right\}\right],{\mathbb{N}}_0,<\right)$$
16	3 15	syl	$$⊢F\in \mathrm{Poly}\left(S\right)\to \mathrm{deg}\left(F\right)=sup\left(A^{-1}\left[ℂ\setminus \left\{0\right\}\right],{\mathbb{N}}_0,<\right)$$