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

Metamath Proof Explorer

Theorem deg1suble

Description: The degree of a difference of polynomials is bounded by the maximum of degrees. (Contributed by Stefan O'Rear, 26-Mar-2015)

Ref Expression
Hypotheses deg1addle.y ⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
deg1addle.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
deg1addle.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
deg1suble.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
deg1suble.m ⊢ − = ( -g ‘ 𝑌 )
deg1suble.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
deg1suble.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
Assertion deg1suble ( 𝜑 → ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 deg1addle.y ⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
2 deg1addle.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
3 deg1addle.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
4 deg1suble.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
5 deg1suble.m ⊢ − = ( -g ‘ 𝑌 )
6 deg1suble.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7 deg1suble.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
8 eqid ⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 )
9 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑌 ∈ Ring )
10 ringgrp ⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ Grp )
11 3 9 10 3syl ⊢ ( 𝜑 → 𝑌 ∈ Grp )
12 eqid ⊢ ( invg ‘ 𝑌 ) = ( invg ‘ 𝑌 )
13 4 12 grpinvcl ⊢ ( ( 𝑌 ∈ Grp ∧ 𝐺 ∈ 𝐵 ) → ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ∈ 𝐵 )
14 11 7 13 syl2anc ⊢ ( 𝜑 → ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ∈ 𝐵 )
15 1 2 3 4 8 6 14 deg1addle ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 ( +g ‘ 𝑌 ) ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) , ( 𝐷 ‘ ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) , ( 𝐷 ‘ 𝐹 ) ) )
16 4 8 12 5 grpsubval ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 − 𝐺 ) = ( 𝐹 ( +g ‘ 𝑌 ) ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) )
17 6 7 16 syl2anc ⊢ ( 𝜑 → ( 𝐹 − 𝐺 ) = ( 𝐹 ( +g ‘ 𝑌 ) ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) )
18 17 fveq2d ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) = ( 𝐷 ‘ ( 𝐹 ( +g ‘ 𝑌 ) ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) ) )
19 1 2 3 4 12 7 deg1invg ⊢ ( 𝜑 → ( 𝐷 ‘ ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) = ( 𝐷 ‘ 𝐺 ) )
20 19 eqcomd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) = ( 𝐷 ‘ ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) )
21 20 breq2d ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) ↔ ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) ) )
22 21 20 ifbieq1d ⊢ ( 𝜑 → if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) = if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) , ( 𝐷 ‘ ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) , ( 𝐷 ‘ 𝐹 ) ) )
23 15 18 22 3brtr4d ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) )