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	⊢ 𝐷 = ( 𝐼 mDeg 𝑅 )
		mdegval.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
		mdegval.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
		mdegval.z	⊢ 0 = ( 0_g ‘ 𝑅 )
		mdegval.a	⊢ 𝐴 = { 𝑚 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑚 “ ℕ ) ∈ Fin }
		mdegval.h	⊢ 𝐻 = ( ℎ ∈ 𝐴 ↦ ( ℂ_fld Σ_g ℎ ) )
	Assertion	mdegval	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) = sup ( ( 𝐻 “ ( 𝐹 supp 0 ) ) , ℝ^* , < ) )

Proof

Step	Hyp	Ref	Expression
1		mdegval.d	⊢ 𝐷 = ( 𝐼 mDeg 𝑅 )
2		mdegval.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
3		mdegval.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		mdegval.z	⊢ 0 = ( 0_g ‘ 𝑅 )
5		mdegval.a	⊢ 𝐴 = { 𝑚 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑚 “ ℕ ) ∈ Fin }
6		mdegval.h	⊢ 𝐻 = ( ℎ ∈ 𝐴 ↦ ( ℂ_fld Σ_g ℎ ) )
7		oveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 supp 0 ) = ( 𝐹 supp 0 ) )
8	7	imaeq2d	⊢ ( 𝑓 = 𝐹 → ( 𝐻 “ ( 𝑓 supp 0 ) ) = ( 𝐻 “ ( 𝐹 supp 0 ) ) )
9	8	supeq1d	⊢ ( 𝑓 = 𝐹 → sup ( ( 𝐻 “ ( 𝑓 supp 0 ) ) , ℝ^* , < ) = sup ( ( 𝐻 “ ( 𝐹 supp 0 ) ) , ℝ^* , < ) )
10	1 2 3 4 5 6	mdegfval	⊢ 𝐷 = ( 𝑓 ∈ 𝐵 ↦ sup ( ( 𝐻 “ ( 𝑓 supp 0 ) ) , ℝ^* , < ) )
11		xrltso	⊢ < Or ℝ^*
12	11	supex	⊢ sup ( ( 𝐻 “ ( 𝐹 supp 0 ) ) , ℝ^* , < ) ∈ V
13	9 10 12	fvmpt	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) = sup ( ( 𝐻 “ ( 𝐹 supp 0 ) ) , ℝ^* , < ) )