Metamath Proof Explorer


Theorem dgrmul2

Description: The degree of a product of polynomials is at most the sum of degrees. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses dgradd.1 𝑀 = ( deg ‘ 𝐹 )
dgradd.2 𝑁 = ( deg ‘ 𝐺 )
Assertion dgrmul2 ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( 𝐹f · 𝐺 ) ) ≤ ( 𝑀 + 𝑁 ) )

Proof

Step Hyp Ref Expression
1 dgradd.1 𝑀 = ( deg ‘ 𝐹 )
2 dgradd.2 𝑁 = ( deg ‘ 𝐺 )
3 eqid ( coeff ‘ 𝐹 ) = ( coeff ‘ 𝐹 )
4 eqid ( coeff ‘ 𝐺 ) = ( coeff ‘ 𝐺 )
5 3 4 1 2 coemullem ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( coeff ‘ ( 𝐹f · 𝐺 ) ) = ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑘 ) · ( ( coeff ‘ 𝐺 ) ‘ ( 𝑛𝑘 ) ) ) ) ∧ ( deg ‘ ( 𝐹f · 𝐺 ) ) ≤ ( 𝑀 + 𝑁 ) ) )
6 5 simprd ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( 𝐹f · 𝐺 ) ) ≤ ( 𝑀 + 𝑁 ) )