Theorem 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	⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
	deg1addle.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1addle.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	deg1addle.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	deg1addle.p	⊢ + = ( +g ‘ 𝑌 )
	deg1addle.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	deg1addle.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
Assertion	deg1addle	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		deg1addle.y	⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
2		deg1addle.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
3		deg1addle.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		deg1addle.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
5		deg1addle.p	⊢ + = ( +g ‘ 𝑌 )
6		deg1addle.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7		deg1addle.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
8		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
9	2	deg1fval	⊢ 𝐷 = ( 1o mDeg 𝑅 )
10		1on	⊢ 1o ∈ On
11	10	a1i	⊢ ( 𝜑 → 1o ∈ On )
12		eqid	⊢ ( Base ‘ ( 1o mPoly 𝑅 ) ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
13	1 8 5	ply1plusg	⊢ + = ( +g ‘ ( 1o mPoly 𝑅 ) )
14	1 4	ply1bascl2	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ ( Base ‘ ( 1o mPoly 𝑅 ) ) )
15	6 14	syl	⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( 1o mPoly 𝑅 ) ) )
16	1 4	ply1bascl2	⊢ ( 𝐺 ∈ 𝐵 → 𝐺 ∈ ( Base ‘ ( 1o mPoly 𝑅 ) ) )
17	7 16	syl	⊢ ( 𝜑 → 𝐺 ∈ ( Base ‘ ( 1o mPoly 𝑅 ) ) )
18	8 9 11 3 12 13 15 17	mdegaddle	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) )