Metamath Proof Explorer

Theorem mdegpropd

Description: Property deduction for polynomial degree. (Contributed by Stefan O'Rear, 28-Mar-2015) (Proof shortened by AV, 27-Jul-2019)

Ref Expression
Hypotheses mdegpropd.b1 ⊢ φ → B = Base R
mdegpropd.b2 ⊢ φ → B = Base S
mdegpropd.p ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + R y = x + S y
Assertion mdegpropd ⊢ φ → I mDeg R = I mDeg S

Proof

Step Hyp Ref Expression
1 mdegpropd.b1 ⊢ φ → B = Base R
2 mdegpropd.b2 ⊢ φ → B = Base S
3 mdegpropd.p ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + R y = x + S y
4 1 2 3 mplbaspropd ⊢ φ → Base I mPoly R = Base I mPoly S
5 1 2 3 grpidpropd ⊢ φ → 0 R = 0 S
6 5 oveq2d ⊢ φ → c supp 0 R = c supp 0 S
7 6 imaeq2d ⊢ φ → b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b c supp 0 R = b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b c supp 0 S
8 7 supeq1d ⊢ φ → sup b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b c supp 0 R ℝ * < = sup b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b c supp 0 S ℝ * <
9 4 8 mpteq12dv ⊢ φ → c ∈ Base I mPoly R ⟼ sup b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b c supp 0 R ℝ * < = c ∈ Base I mPoly S ⟼ sup b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b c supp 0 S ℝ * <
10 eqid ⊢ I mDeg R = I mDeg R
11 eqid ⊢ I mPoly R = I mPoly R
12 eqid ⊢ Base I mPoly R = Base I mPoly R
13 eqid ⊢ 0 R = 0 R
14 eqid ⊢ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin = a ∈ ℕ 0 I | a -1 ℕ ∈ Fin
15 eqid ⊢ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b = b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b
16 10 11 12 13 14 15 mdegfval ⊢ I mDeg R = c ∈ Base I mPoly R ⟼ sup b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b c supp 0 R ℝ * <
17 eqid ⊢ I mDeg S = I mDeg S
18 eqid ⊢ I mPoly S = I mPoly S
19 eqid ⊢ Base I mPoly S = Base I mPoly S
20 eqid ⊢ 0 S = 0 S
21 17 18 19 20 14 15 mdegfval ⊢ I mDeg S = c ∈ Base I mPoly S ⟼ sup b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b c supp 0 S ℝ * <
22 9 16 21 3eqtr4g ⊢ φ → I mDeg R = I mDeg S