Metamath Proof Explorer

Theorem mdegfval

Description: Value of the multivariate degree function. (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 mdegfval 𝐷 = ( 𝑓 ∈ 𝐵 ↦ 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 oveq12 ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑖 mPoly 𝑟 ) = ( 𝐼 mPoly 𝑅 ) )
8 7 2 eqtr4di ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑖 mPoly 𝑟 ) = 𝑃 )
9 8 fveq2d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) = ( Base ‘ 𝑃 ) )
10 9 3 eqtr4di ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) = 𝐵 )
11 fveq2 ⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
12 11 4 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = 0 )
13 12 oveq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑓 supp ( 0g ‘ 𝑟 ) ) = ( 𝑓 supp 0 ) )
14 13 mpteq1d ⊢ ( 𝑟 = 𝑅 → ( ℎ ∈ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ↦ ( ℂfld Σg ℎ ) ) = ( ℎ ∈ ( 𝑓 supp 0 ) ↦ ( ℂfld Σg ℎ ) ) )
15 14 rneqd ⊢ ( 𝑟 = 𝑅 → ran ( ℎ ∈ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ↦ ( ℂfld Σg ℎ ) ) = ran ( ℎ ∈ ( 𝑓 supp 0 ) ↦ ( ℂfld Σg ℎ ) ) )
16 15 supeq1d ⊢ ( 𝑟 = 𝑅 → sup ( ran ( ℎ ∈ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ↦ ( ℂfld Σg ℎ ) ) , ℝ* , < ) = sup ( ran ( ℎ ∈ ( 𝑓 supp 0 ) ↦ ( ℂfld Σg ℎ ) ) , ℝ* , < ) )
17 16 adantl ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → sup ( ran ( ℎ ∈ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ↦ ( ℂfld Σg ℎ ) ) , ℝ* , < ) = sup ( ran ( ℎ ∈ ( 𝑓 supp 0 ) ↦ ( ℂfld Σg ℎ ) ) , ℝ* , < ) )
18 10 17 mpteq12dv ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ sup ( ran ( ℎ ∈ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ↦ ( ℂfld Σg ℎ ) ) , ℝ* , < ) ) = ( 𝑓 ∈ 𝐵 ↦ sup ( ran ( ℎ ∈ ( 𝑓 supp 0 ) ↦ ( ℂfld Σg ℎ ) ) , ℝ* , < ) ) )
19 df-mdeg ⊢ mDeg = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ sup ( ran ( ℎ ∈ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ↦ ( ℂfld Σg ℎ ) ) , ℝ* , < ) ) )
20 3 fvexi ⊢ 𝐵 ∈ V
21 20 mptex ⊢ ( 𝑓 ∈ 𝐵 ↦ sup ( ran ( ℎ ∈ ( 𝑓 supp 0 ) ↦ ( ℂfld Σg ℎ ) ) , ℝ* , < ) ) ∈ V
22 18 19 21 ovmpoa ⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 mDeg 𝑅 ) = ( 𝑓 ∈ 𝐵 ↦ sup ( ran ( ℎ ∈ ( 𝑓 supp 0 ) ↦ ( ℂfld Σg ℎ ) ) , ℝ* , < ) ) )
23 6 reseq1i ⊢ ( 𝐻 ↾ ( 𝑓 supp 0 ) ) = ( ( ℎ ∈ 𝐴 ↦ ( ℂfld Σg ℎ ) ) ↾ ( 𝑓 supp 0 ) )
24 suppssdm ⊢ ( 𝑓 supp 0 ) ⊆ dom 𝑓
25 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
26 simpr ⊢ ( ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ∧ 𝑓 ∈ 𝐵 ) → 𝑓 ∈ 𝐵 )
27 2 25 3 5 26 mplelf ⊢ ( ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ∧ 𝑓 ∈ 𝐵 ) → 𝑓 : 𝐴 ⟶ ( Base ‘ 𝑅 ) )
28 24 27 fssdm ⊢ ( ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ∧ 𝑓 ∈ 𝐵 ) → ( 𝑓 supp 0 ) ⊆ 𝐴 )
29 28 resmptd ⊢ ( ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ∧ 𝑓 ∈ 𝐵 ) → ( ( ℎ ∈ 𝐴 ↦ ( ℂfld Σg ℎ ) ) ↾ ( 𝑓 supp 0 ) ) = ( ℎ ∈ ( 𝑓 supp 0 ) ↦ ( ℂfld Σg ℎ ) ) )
30 23 29 syl5req ⊢ ( ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ∧ 𝑓 ∈ 𝐵 ) → ( ℎ ∈ ( 𝑓 supp 0 ) ↦ ( ℂfld Σg ℎ ) ) = ( 𝐻 ↾ ( 𝑓 supp 0 ) ) )
31 30 rneqd ⊢ ( ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ∧ 𝑓 ∈ 𝐵 ) → ran ( ℎ ∈ ( 𝑓 supp 0 ) ↦ ( ℂfld Σg ℎ ) ) = ran ( 𝐻 ↾ ( 𝑓 supp 0 ) ) )
32 df-ima ⊢ ( 𝐻 “ ( 𝑓 supp 0 ) ) = ran ( 𝐻 ↾ ( 𝑓 supp 0 ) )
33 31 32 eqtr4di ⊢ ( ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ∧ 𝑓 ∈ 𝐵 ) → ran ( ℎ ∈ ( 𝑓 supp 0 ) ↦ ( ℂfld Σg ℎ ) ) = ( 𝐻 “ ( 𝑓 supp 0 ) ) )
34 33 supeq1d ⊢ ( ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ∧ 𝑓 ∈ 𝐵 ) → sup ( ran ( ℎ ∈ ( 𝑓 supp 0 ) ↦ ( ℂfld Σg ℎ ) ) , ℝ* , < ) = sup ( ( 𝐻 “ ( 𝑓 supp 0 ) ) , ℝ* , < ) )
35 34 mpteq2dva ⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑓 ∈ 𝐵 ↦ sup ( ran ( ℎ ∈ ( 𝑓 supp 0 ) ↦ ( ℂfld Σg ℎ ) ) , ℝ* , < ) ) = ( 𝑓 ∈ 𝐵 ↦ sup ( ( 𝐻 “ ( 𝑓 supp 0 ) ) , ℝ* , < ) ) )
36 22 35 eqtrd ⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 mDeg 𝑅 ) = ( 𝑓 ∈ 𝐵 ↦ sup ( ( 𝐻 “ ( 𝑓 supp 0 ) ) , ℝ* , < ) ) )
37 reldmmdeg ⊢ Rel dom mDeg
38 37 ovprc ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 mDeg 𝑅 ) = ∅ )
39 mpt0 ⊢ ( 𝑓 ∈ ∅ ↦ sup ( ( 𝐻 “ ( 𝑓 supp 0 ) ) , ℝ* , < ) ) = ∅
40 38 39 eqtr4di ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 mDeg 𝑅 ) = ( 𝑓 ∈ ∅ ↦ sup ( ( 𝐻 “ ( 𝑓 supp 0 ) ) , ℝ* , < ) ) )
41 reldmmpl ⊢ Rel dom mPoly
42 41 ovprc ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 mPoly 𝑅 ) = ∅ )
43 2 42 syl5eq ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → 𝑃 = ∅ )
44 43 fveq2d ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( Base ‘ 𝑃 ) = ( Base ‘ ∅ ) )
45 base0 ⊢ ∅ = ( Base ‘ ∅ )
46 44 3 45 3eqtr4g ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → 𝐵 = ∅ )
47 46 mpteq1d ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑓 ∈ 𝐵 ↦ sup ( ( 𝐻 “ ( 𝑓 supp 0 ) ) , ℝ* , < ) ) = ( 𝑓 ∈ ∅ ↦ sup ( ( 𝐻 “ ( 𝑓 supp 0 ) ) , ℝ* , < ) ) )
48 40 47 eqtr4d ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 mDeg 𝑅 ) = ( 𝑓 ∈ 𝐵 ↦ sup ( ( 𝐻 “ ( 𝑓 supp 0 ) ) , ℝ* , < ) ) )
49 36 48 pm2.61i ⊢ ( 𝐼 mDeg 𝑅 ) = ( 𝑓 ∈ 𝐵 ↦ sup ( ( 𝐻 “ ( 𝑓 supp 0 ) ) , ℝ* , < ) )
50 1 49 eqtri ⊢ 𝐷 = ( 𝑓 ∈ 𝐵 ↦ sup ( ( 𝐻 “ ( 𝑓 supp 0 ) ) , ℝ* , < ) )