This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 mDeg R$
		mdegval.p	$⊢ P = I mPoly R$
		mdegval.b	$⊢ B = {Base}_{P}$
		mdegval.z	$⊢ \underset{˙}{0} = 0_{R}$
		mdegval.a	$⊢ A = \{m \in ({ℕ_{0}}^{I}) \| m^{-1} [ℕ] \in Fin\}$
		mdegval.h	$⊢ H = (h \in A ⟼ \sum_{ℂ_{fld}} h)$
	Assertion	mdegval	$⊢ F \in B \to D (F) = sup (H [F supp \underset{˙}{0}] ℝ^{*} <)$

Proof

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