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 = ( 0g ‘ 𝑅 )
	mdegval.a	⊢ 𝐴 = { 𝑚 ∈ ( ℕ0 ↑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 = ( 0g ‘ 𝑅 )
5		mdegval.a	⊢ 𝐴 = { 𝑚 ∈ ( ℕ0 ↑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 ) ) , ℝ* , < ) )