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

Metamath Proof Explorer

Theorem deg1vscale

Description: The degree of a scalar times a polynomial is at most the degree of the original polynomial. (Contributed by Stefan O'Rear, 26-Mar-2015)

Ref Expression
Hypotheses deg1addle.y ⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
deg1addle.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
deg1addle.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
deg1vscale.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
deg1vscale.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
deg1vscale.p ⊢ · = ( ·𝑠 ‘ 𝑌 )
deg1vscale.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐾 )
deg1vscale.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
Assertion deg1vscale ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ≤ ( 𝐷 ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 deg1addle.y ⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
2 deg1addle.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
3 deg1addle.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
4 deg1vscale.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
5 deg1vscale.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
6 deg1vscale.p ⊢ · = ( ·𝑠 ‘ 𝑌 )
7 deg1vscale.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐾 )
8 deg1vscale.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
9 eqid ⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
10 2 deg1fval ⊢ 𝐷 = ( 1o mDeg 𝑅 )
11 1on ⊢ 1o ∈ On
12 11 a1i ⊢ ( 𝜑 → 1o ∈ On )
13 1 4 ply1bas ⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
14 1 9 6 ply1vsca ⊢ · = ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) )
15 9 10 12 3 13 5 14 7 8 mdegvscale ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ≤ ( 𝐷 ‘ 𝐺 ) )