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

Metamath Proof Explorer

Theorem deg1mulle2

Description: Produce a bound on the product of two univariate polynomials given bounds on the factors. (Contributed by Stefan O'Rear, 26-Mar-2015)

Ref Expression
Hypotheses deg1addle.y ⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
deg1addle.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
deg1addle.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
deg1mulle2.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
deg1mulle2.t ⊢ · = ( .r ‘ 𝑌 )
deg1mulle2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
deg1mulle2.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
deg1mulle2.j1 ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
deg1mulle2.k1 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
deg1mulle2.j2 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ 𝐽 )
deg1mulle2.k2 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ≤ 𝐾 )
Assertion deg1mulle2 ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ≤ ( 𝐽 + 𝐾 ) )

Proof

Step Hyp Ref Expression
1 deg1addle.y ⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
2 deg1addle.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
3 deg1addle.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
4 deg1mulle2.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
5 deg1mulle2.t ⊢ · = ( .r ‘ 𝑌 )
6 deg1mulle2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7 deg1mulle2.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
8 deg1mulle2.j1 ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
9 deg1mulle2.k1 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
10 deg1mulle2.j2 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ 𝐽 )
11 deg1mulle2.k2 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ≤ 𝐾 )
12 eqid ⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
13 2 deg1fval ⊢ 𝐷 = ( 1o mDeg 𝑅 )
14 1on ⊢ 1o ∈ On
15 14 a1i ⊢ ( 𝜑 → 1o ∈ On )
16 1 4 ply1bas ⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
17 1 12 5 ply1mulr ⊢ · = ( .r ‘ ( 1o mPoly 𝑅 ) )
18 12 13 15 3 16 17 6 7 8 9 10 11 mdegmulle2 ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ≤ ( 𝐽 + 𝐾 ) )