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	$⊢ Y = {Poly}_{1} (R)$
		deg1addle.d	$⊢ D = \deg_{1} (R)$
		deg1addle.r	$⊢ φ \to R \in Ring$
		deg1mulle2.b	$⊢ B = {Base}_{Y}$
		deg1mulle2.t	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
		deg1mulle2.f	$⊢ φ \to F \in B$
		deg1mulle2.g	$⊢ φ \to G \in B$
		deg1mulle2.j1	$⊢ φ \to J \in ℕ_{0}$
		deg1mulle2.k1	$⊢ φ \to K \in ℕ_{0}$
		deg1mulle2.j2	$⊢ φ \to D (F) \leq J$
		deg1mulle2.k2	$⊢ φ \to D (G) \leq K$
	Assertion	deg1mulle2	$⊢ φ \to D (F \underset{˙}{\cdot} G) \leq J + K$

Proof

Step	Hyp	Ref	Expression
1		deg1addle.y	$⊢ Y = {Poly}_{1} (R)$
2		deg1addle.d	$⊢ D = \deg_{1} (R)$
3		deg1addle.r	$⊢ φ \to R \in Ring$
4		deg1mulle2.b	$⊢ B = {Base}_{Y}$
5		deg1mulle2.t	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
6		deg1mulle2.f	$⊢ φ \to F \in B$
7		deg1mulle2.g	$⊢ φ \to G \in B$
8		deg1mulle2.j1	$⊢ φ \to J \in ℕ_{0}$
9		deg1mulle2.k1	$⊢ φ \to K \in ℕ_{0}$
10		deg1mulle2.j2	$⊢ φ \to D (F) \leq J$
11		deg1mulle2.k2	$⊢ φ \to D (G) \leq K$
12		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
13	2	deg1fval	$⊢ D = 1_{𝑜} mDeg R$
14		1on	$⊢ 1_{𝑜} \in On$
15	14	a1i	$⊢ φ \to 1_{𝑜} \in On$
16	1 4	ply1bas	$⊢ B = {Base}_{(1_{𝑜} mPoly R)}$
17	1 12 5	ply1mulr	$⊢ \underset{˙}{\cdot} = \cdot_{(1_{𝑜} mPoly R)}$
18	12 13 15 3 16 17 6 7 8 9 10 11	mdegmulle2	$⊢ φ \to D (F \underset{˙}{\cdot} G) \leq J + K$