Theorem mdegxrf

Description: Functionality 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	mdegxrf	$$⊢D:B⟶{ℝ}^{*}$$

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		xrltso	$$⊢<\mathrm{Or}{ℝ}^{*}$$
5	4	supex	$$⊢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[z\mathrm{supp}{0}_R\right],{ℝ}^{*},<\right)\in \mathrm{V}$$
6		eqid	$$⊢0_R=0_R$$
7		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\}$$
8		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)$$
9	1 2 3 6 7 8	mdegfval	$$⊢D=\left(z\in B⟼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[z\mathrm{supp}{0}_R\right],{ℝ}^{*},<\right)\right)$$
10	5 9	fnmpti	$$⊢DFnB$$
11	1 2 3	mdegxrcl	$$⊢f\in B\to D\left(f\right)\in {ℝ}^{*}$$
12	11	rgen	$$⊢\forall f\in BD\left(f\right)\in {ℝ}^{*}$$
13		ffnfv	$$⊢D:B⟶{ℝ}^{*}\leftrightarrow \left(DFnB\wedge \forall f\in BD\left(f\right)\in {ℝ}^{*}\right)$$
14	10 12 13	mpbir2an	$$⊢D:B⟶{ℝ}^{*}$$