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		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
17	1 16 4	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
18	1 12 5	ply1mulr	⊢ · = ( .r ‘ ( 1o mPoly 𝑅 ) )
19	12 13 15 3 17 18 6 7 8 9 10 11	mdegmulle2	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ≤ ( 𝐽 + 𝐾 ) )