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 eqid ( PwSer1𝑅 ) = ( PwSer1𝑅 )
14 1 13 4 ply1bas 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
15 1 9 6 ply1vsca · = ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) )
16 9 10 12 3 14 5 15 7 8 mdegvscale ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ≤ ( 𝐷𝐺 ) )