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 𝐴 = { 𝑚 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑚 “ ℕ ) ∈ 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 𝐴 = { 𝑚 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑚 “ ℕ ) ∈ 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 eqtr2id ( ( ( 𝐼 ∈ 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 ) ) , ℝ* , < ) )