Theorem mdegxrcl

Description: Closure of polynomial degree in the extended reals. (Contributed by Stefan O'Rear, 19-Mar-2015) (Proof shortened by AV, 27-Jul-2019)

	Ref	Expression
Hypotheses	mdegxrcl.d	$$⊢D=I\mathrm{mDeg}R$$
	mdegxrcl.p	$$⊢P=I\mathrm{mPoly}R$$
	mdegxrcl.b	$$⊢B={\mathrm{Base}}_P$$
Assertion	mdegxrcl	$$⊢F\in B\to D\left(F\right)\in {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		mdegxrcl.d	$$⊢D=I\mathrm{mDeg}R$$
2		mdegxrcl.p	$$⊢P=I\mathrm{mPoly}R$$
3		mdegxrcl.b	$$⊢B={\mathrm{Base}}_P$$
4		eqid	$$⊢0_R=0_R$$
5		eqid	$$⊢\left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
6		eqid	$$⊢\left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right)=\left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right)$$
7	1 2 3 4 5 6	mdegval	$$⊢F\in B\to D\left(F\right)=sup\left(\left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right)\left[F\mathrm{supp}{0}_R\right],{ℝ}^{*},<\right)$$
8		imassrn	$$⊢\left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right)\left[F\mathrm{supp}{0}_R\right]\subseteq \mathrm{ran}\left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right)$$
9	2 3	mplrcl	$$⊢F\in B\to I\in \mathrm{V}$$
10	5 6	tdeglem1	$$⊢I\in \mathrm{V}\to \left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right):\left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathbb{N}}_0$$
11		frn	$$⊢\left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right):\left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathbb{N}}_0\to \mathrm{ran}\left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right)\subseteq {\mathbb{N}}_0$$
12	9 10 11	3syl	$$⊢F\in B\to \mathrm{ran}\left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right)\subseteq {\mathbb{N}}_0$$
13		nn0ssre	$$⊢{\mathbb{N}}_0\subseteq ℝ$$
14		ressxr	$$⊢ℝ\subseteq {ℝ}^{*}$$
15	13 14	sstri	$$⊢{\mathbb{N}}_0\subseteq {ℝ}^{*}$$
16	12 15	sstrdi	$$⊢F\in B\to \mathrm{ran}\left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right)\subseteq {ℝ}^{*}$$
17	8 16	sstrid	$$⊢F\in B\to \left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right)\left[F\mathrm{supp}{0}_R\right]\subseteq {ℝ}^{*}$$
18		supxrcl	$$⊢\left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right)\left[F\mathrm{supp}{0}_R\right]\subseteq {ℝ}^{*}\to sup\left(\left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right)\left[F\mathrm{supp}{0}_R\right],{ℝ}^{*},<\right)\in {ℝ}^{*}$$
19	17 18	syl	$$⊢F\in B\to sup\left(\left(y\in \left\{x\in \left({{\mathbb{N}}_0}^I\right)|x^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}y\right)\left[F\mathrm{supp}{0}_R\right],{ℝ}^{*},<\right)\in {ℝ}^{*}$$
20	7 19	eqeltrd	$$⊢F\in B\to D\left(F\right)\in {ℝ}^{*}$$