deg1addle

Description: The degree of a sum is at most the maximum of the degrees of 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$
	deg1addle.b	$⊢ B = {Base}_{Y}$
	deg1addle.p	$⊢ \underset{˙}{+} = +_{Y}$
	deg1addle.f	$⊢ φ \to F \in B$
	deg1addle.g	$⊢ φ \to G \in B$
Assertion	deg1addle	$⊢ φ \to D (F \underset{˙}{+} G) \leq if (D (F) \leq D (G), D (G), D (F))$

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		deg1addle.b	$⊢ B = {Base}_{Y}$
5		deg1addle.p	$⊢ \underset{˙}{+} = +_{Y}$
6		deg1addle.f	$⊢ φ \to F \in B$
7		deg1addle.g	$⊢ φ \to G \in B$
8		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
9	2	deg1fval	$⊢ D = 1_{𝑜} mDeg R$
10		1on	$⊢ 1_{𝑜} \in On$
11	10	a1i	$⊢ φ \to 1_{𝑜} \in On$
12		eqid	$⊢ {Base}_{(1_{𝑜} mPoly R)} = {Base}_{(1_{𝑜} mPoly R)}$
13	1 8 5	ply1plusg	$⊢ \underset{˙}{+} = +_{(1_{𝑜} mPoly R)}$
14	1 4	ply1bascl2	$⊢ F \in B \to F \in {Base}_{(1_{𝑜} mPoly R)}$
15	6 14	syl	$⊢ φ \to F \in {Base}_{(1_{𝑜} mPoly R)}$
16	1 4	ply1bascl2	$⊢ G \in B \to G \in {Base}_{(1_{𝑜} mPoly R)}$
17	7 16	syl	$⊢ φ \to G \in {Base}_{(1_{𝑜} mPoly R)}$
18	8 9 11 3 12 13 15 17	mdegaddle	$⊢ φ \to D (F \underset{˙}{+} G) \leq if (D (F) \leq D (G), D (G), D (F))$

Metamath Proof Explorer