This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mdegmulle2

Description: The multivariate degree of a product of polynomials is at most the sum of the degrees of the polynomials. (Contributed by Stefan O'Rear, 26-Mar-2015)

Ref Expression
Hypotheses mdegaddle.y ⊢ Y = I mPoly R
mdegaddle.d ⊢ D = I mDeg R
mdegaddle.i ⊢ φ → I ∈ V
mdegaddle.r ⊢ φ → R ∈ Ring
mdegmulle2.b ⊢ B = Base Y
mdegmulle2.t ⊢ · ˙ = ⋅ Y
mdegmulle2.f ⊢ φ → F ∈ B
mdegmulle2.g ⊢ φ → G ∈ B
mdegmulle2.j1 ⊢ φ → J ∈ ℕ 0
mdegmulle2.k1 ⊢ φ → K ∈ ℕ 0
mdegmulle2.j2 ⊢ φ → D ⁡ F ≤ J
mdegmulle2.k2 ⊢ φ → D ⁡ G ≤ K
Assertion mdegmulle2 ⊢ φ → D ⁡ F · ˙ G ≤ J + K

Proof

Step Hyp Ref Expression
1 mdegaddle.y ⊢ Y = I mPoly R
2 mdegaddle.d ⊢ D = I mDeg R
3 mdegaddle.i ⊢ φ → I ∈ V
4 mdegaddle.r ⊢ φ → R ∈ Ring
5 mdegmulle2.b ⊢ B = Base Y
6 mdegmulle2.t ⊢ · ˙ = ⋅ Y
7 mdegmulle2.f ⊢ φ → F ∈ B
8 mdegmulle2.g ⊢ φ → G ∈ B
9 mdegmulle2.j1 ⊢ φ → J ∈ ℕ 0
10 mdegmulle2.k1 ⊢ φ → K ∈ ℕ 0
11 mdegmulle2.j2 ⊢ φ → D ⁡ F ≤ J
12 mdegmulle2.k2 ⊢ φ → D ⁡ G ≤ K
13 eqid ⊢ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin = a ∈ ℕ 0 I | a -1 ℕ ∈ Fin
14 eqid ⊢ b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b = b ∈ a ∈ ℕ 0 I | a -1 ℕ ∈ Fin ⟼ ∑ ℂ fld b
15 1 2 3 4 5 6 7 8 9 10 11 12 13 14 mdegmullem ⊢ φ → D ⁡ F · ˙ G ≤ J + K