Theorem mdegval

Description: Value of the multivariate degree function at some particular polynomial. (Contributed by Stefan O'Rear, 19-Mar-2015) (Revised by AV, 25-Jun-2019)

	Ref	Expression
Hypotheses	mdegval.d	$$⊢D=I\mathrm{mDeg}R$$
	mdegval.p	$$⊢P=I\mathrm{mPoly}R$$
	mdegval.b	$$⊢B={\mathrm{Base}}_P$$
	mdegval.z	$$⊢\underset{\dot{}}{0}=0_R$$
	mdegval.a	$$⊢A=\left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	mdegval.h	$$⊢H=\left(h\in A⟼{\sum }_{{ℂ}_{\mathrm{fld}}}h\right)$$
Assertion	mdegval	$$⊢F\in B\to D\left(F\right)=sup\left(H\left[F\mathrm{supp}\underset{\dot{}}{0}\right],{ℝ}^{*},<\right)$$

Proof

Step	Hyp	Ref	Expression
1		mdegval.d	$$⊢D=I\mathrm{mDeg}R$$
2		mdegval.p	$$⊢P=I\mathrm{mPoly}R$$
3		mdegval.b	$$⊢B={\mathrm{Base}}_P$$
4		mdegval.z	$$⊢\underset{\dot{}}{0}=0_R$$
5		mdegval.a	$$⊢A=\left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
6		mdegval.h	$$⊢H=\left(h\in A⟼{\sum }_{{ℂ}_{\mathrm{fld}}}h\right)$$
7		oveq1	$$⊢f=F\to f\mathrm{supp}\underset{\dot{}}{0}=F\mathrm{supp}\underset{\dot{}}{0}$$
8	7	imaeq2d	$$⊢f=F\to H\left[f\mathrm{supp}\underset{\dot{}}{0}\right]=H\left[F\mathrm{supp}\underset{\dot{}}{0}\right]$$
9	8	supeq1d	$$⊢f=F\to sup\left(H\left[f\mathrm{supp}\underset{\dot{}}{0}\right],{ℝ}^{*},<\right)=sup\left(H\left[F\mathrm{supp}\underset{\dot{}}{0}\right],{ℝ}^{*},<\right)$$
10	1 2 3 4 5 6	mdegfval	$$⊢D=\left(f\in B⟼sup\left(H\left[f\mathrm{supp}\underset{\dot{}}{0}\right],{ℝ}^{*},<\right)\right)$$
11		xrltso	$$⊢<\mathrm{Or}{ℝ}^{*}$$
12	11	supex	$$⊢sup\left(H\left[F\mathrm{supp}\underset{\dot{}}{0}\right],{ℝ}^{*},<\right)\in \mathrm{V}$$
13	9 10 12	fvmpt	$$⊢F\in B\to D\left(F\right)=sup\left(H\left[F\mathrm{supp}\underset{\dot{}}{0}\right],{ℝ}^{*},<\right)$$