This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) )