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 ⊢ D = I mDeg R
mdegval.p ⊢ P = I mPoly R
mdegval.b ⊢ B = Base P
mdegval.z ⊢ 0 ˙ = 0 R
mdegval.a ⊢ A = m ∈ ℕ 0 I | m -1 ℕ ∈ Fin
mdegval.h ⊢ H = h ∈ A ⟼ ∑ ℂ fld h
Assertion mdegfval ⊢ D = f ∈ B ⟼ sup H f supp 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 ⊢ 0 ˙ = 0 R
5 mdegval.a ⊢ A = m ∈ ℕ 0 I | m -1 ℕ ∈ Fin
6 mdegval.h ⊢ H = h ∈ A ⟼ ∑ ℂ fld h
7 oveq12 ⊢ i = I ∧ r = R → i mPoly r = I mPoly R
8 7 2 eqtr4di ⊢ i = I ∧ r = R → i mPoly r = P
9 8 fveq2d ⊢ i = I ∧ r = R → Base i mPoly r = Base P
10 9 3 eqtr4di ⊢ i = I ∧ r = R → Base i mPoly r = B
11 fveq2 ⊢ r = R → 0 r = 0 R
12 11 4 eqtr4di ⊢ r = R → 0 r = 0 ˙
13 12 oveq2d ⊢ r = R → f supp 0 r = f supp 0 ˙
14 13 mpteq1d ⊢ r = R → h ∈ supp 0 r⁡ f ⟼ ∑ ℂ fld h = h ∈ supp 0 ˙⁡ f ⟼ ∑ ℂ fld h
15 14 rneqd ⊢ r = R → ran ⁡ h ∈ supp 0 r⁡ f ⟼ ∑ ℂ fld h = ran ⁡ h ∈ supp 0 ˙⁡ f ⟼ ∑ ℂ fld h
16 15 supeq1d ⊢ r = R → sup ran ⁡ h ∈ supp 0 r⁡ f ⟼ ∑ ℂ fld h ℝ * < = sup ran ⁡ h ∈ supp 0 ˙⁡ f ⟼ ∑ ℂ fld h ℝ * <
17 16 adantl ⊢ i = I ∧ r = R → sup ran ⁡ h ∈ supp 0 r⁡ f ⟼ ∑ ℂ fld h ℝ * < = sup ran ⁡ h ∈ supp 0 ˙⁡ f ⟼ ∑ ℂ fld h ℝ * <
18 10 17 mpteq12dv ⊢ i = I ∧ r = R → f ∈ Base i mPoly r ⟼ sup ran ⁡ h ∈ supp 0 r⁡ f ⟼ ∑ ℂ fld h ℝ * < = f ∈ B ⟼ sup ran ⁡ h ∈ supp 0 ˙⁡ f ⟼ ∑ ℂ fld h ℝ * <
19 df-mdeg ⊢ mDeg = i ∈ V , r ∈ V ⟼ f ∈ Base i mPoly r ⟼ sup ran ⁡ h ∈ supp 0 r⁡ f ⟼ ∑ ℂ fld h ℝ * <
20 3 fvexi ⊢ B ∈ V
21 20 mptex ⊢ f ∈ B ⟼ sup ran ⁡ h ∈ supp 0 ˙⁡ f ⟼ ∑ ℂ fld h ℝ * < ∈ V
22 18 19 21 ovmpoa ⊢ I ∈ V ∧ R ∈ V → I mDeg R = f ∈ B ⟼ sup ran ⁡ h ∈ supp 0 ˙⁡ f ⟼ ∑ ℂ fld h ℝ * <
23 6 reseq1i ⊢ H ↾ supp 0 ˙⁡ f = h ∈ A ⟼ ∑ ℂ fld h ↾ supp 0 ˙⁡ f
24 suppssdm ⊢ f supp 0 ˙ ⊆ dom ⁡ f
25 eqid ⊢ Base R = Base R
26 simpr ⊢ I ∈ V ∧ R ∈ V ∧ f ∈ B → f ∈ B
27 2 25 3 5 26 mplelf ⊢ I ∈ V ∧ R ∈ V ∧ f ∈ B → f : A ⟶ Base R
28 24 27 fssdm ⊢ I ∈ V ∧ R ∈ V ∧ f ∈ B → f supp 0 ˙ ⊆ A
29 28 resmptd ⊢ I ∈ V ∧ R ∈ V ∧ f ∈ B → h ∈ A ⟼ ∑ ℂ fld h ↾ supp 0 ˙⁡ f = h ∈ supp 0 ˙⁡ f ⟼ ∑ ℂ fld h
30 23 29 eqtr2id ⊢ I ∈ V ∧ R ∈ V ∧ f ∈ B → h ∈ supp 0 ˙⁡ f ⟼ ∑ ℂ fld h = H ↾ supp 0 ˙⁡ f
31 30 rneqd ⊢ I ∈ V ∧ R ∈ V ∧ f ∈ B → ran ⁡ h ∈ supp 0 ˙⁡ f ⟼ ∑ ℂ fld h = ran ⁡ H ↾ supp 0 ˙⁡ f
32 df-ima ⊢ H f supp 0 ˙ = ran ⁡ H ↾ supp 0 ˙⁡ f
33 31 32 eqtr4di ⊢ I ∈ V ∧ R ∈ V ∧ f ∈ B → ran ⁡ h ∈ supp 0 ˙⁡ f ⟼ ∑ ℂ fld h = H f supp 0 ˙
34 33 supeq1d ⊢ I ∈ V ∧ R ∈ V ∧ f ∈ B → sup ran ⁡ h ∈ supp 0 ˙⁡ f ⟼ ∑ ℂ fld h ℝ * < = sup H f supp 0 ˙ ℝ * <
35 34 mpteq2dva ⊢ I ∈ V ∧ R ∈ V → f ∈ B ⟼ sup ran ⁡ h ∈ supp 0 ˙⁡ f ⟼ ∑ ℂ fld h ℝ * < = f ∈ B ⟼ sup H f supp 0 ˙ ℝ * <
36 22 35 eqtrd ⊢ I ∈ V ∧ R ∈ V → I mDeg R = f ∈ B ⟼ sup H f supp 0 ˙ ℝ * <
37 reldmmdeg ⊢ Rel ⁡ dom ⁡ mDeg
38 37 ovprc ⊢ ¬ I ∈ V ∧ R ∈ V → I mDeg R = ∅
39 mpt0 ⊢ f ∈ ∅ ⟼ sup H f supp 0 ˙ ℝ * < = ∅
40 38 39 eqtr4di ⊢ ¬ I ∈ V ∧ R ∈ V → I mDeg R = f ∈ ∅ ⟼ sup H f supp 0 ˙ ℝ * <
41 reldmmpl ⊢ Rel ⁡ dom ⁡ mPoly
42 41 ovprc ⊢ ¬ I ∈ V ∧ R ∈ V → I mPoly R = ∅
43 2 42 syl5eq ⊢ ¬ I ∈ V ∧ R ∈ V → P = ∅
44 43 fveq2d ⊢ ¬ I ∈ V ∧ R ∈ V → Base P = Base ∅
45 base0 ⊢ ∅ = Base ∅
46 44 3 45 3eqtr4g ⊢ ¬ I ∈ V ∧ R ∈ V → B = ∅
47 46 mpteq1d ⊢ ¬ I ∈ V ∧ R ∈ V → f ∈ B ⟼ sup H f supp 0 ˙ ℝ * < = f ∈ ∅ ⟼ sup H f supp 0 ˙ ℝ * <
48 40 47 eqtr4d ⊢ ¬ I ∈ V ∧ R ∈ V → I mDeg R = f ∈ B ⟼ sup H f supp 0 ˙ ℝ * <
49 36 48 pm2.61i ⊢ I mDeg R = f ∈ B ⟼ sup H f supp 0 ˙ ℝ * <
50 1 49 eqtri ⊢ D = f ∈ B ⟼ sup H f supp 0 ˙ ℝ * <