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 ⊢ 𝑌 = ( 𝐼 mPoly 𝑅 )
mdegaddle.d ⊢ 𝐷 = ( 𝐼 mDeg 𝑅 )
mdegaddle.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
mdegaddle.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mdegmulle2.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
mdegmulle2.t ⊢ · = ( .r ‘ 𝑌 )
mdegmulle2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
mdegmulle2.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
mdegmulle2.j1 ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
mdegmulle2.k1 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
mdegmulle2.j2 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ 𝐽 )
mdegmulle2.k2 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ≤ 𝐾 )
Assertion mdegmulle2 ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ≤ ( 𝐽 + 𝐾 ) )

Proof

Step Hyp Ref Expression
1 mdegaddle.y ⊢ 𝑌 = ( 𝐼 mPoly 𝑅 )
2 mdegaddle.d ⊢ 𝐷 = ( 𝐼 mDeg 𝑅 )
3 mdegaddle.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4 mdegaddle.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 mdegmulle2.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
6 mdegmulle2.t ⊢ · = ( .r ‘ 𝑌 )
7 mdegmulle2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
8 mdegmulle2.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
9 mdegmulle2.j1 ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
10 mdegmulle2.k1 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
11 mdegmulle2.j2 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ 𝐽 )
12 mdegmulle2.k2 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ≤ 𝐾 )
13 eqid ⊢ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } = { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin }
14 eqid ⊢ ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) ) = ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑏 ) )
15 1 2 3 4 5 6 7 8 9 10 11 12 13 14 mdegmullem ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ≤ ( 𝐽 + 𝐾 ) )