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 
|- Y = ( Poly1 ` R )
deg1addle.d 
|- D = ( deg1 ` R )
deg1addle.r 
|- ( ph -> R e. Ring )
deg1suble.b 
|- B = ( Base ` Y )
deg1suble.m 
|- .- = ( -g ` Y )
deg1suble.f 
|- ( ph -> F e. B )
deg1suble.g 
|- ( ph -> G e. B )
Assertion deg1suble 
|- ( ph -> ( D ` ( F .- G ) ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) )

Proof

Step Hyp Ref Expression
1 deg1addle.y 
 |-  Y = ( Poly1 ` R )
2 deg1addle.d 
 |-  D = ( deg1 ` R )
3 deg1addle.r 
 |-  ( ph -> R e. Ring )
4 deg1suble.b 
 |-  B = ( Base ` Y )
5 deg1suble.m 
 |-  .- = ( -g ` Y )
6 deg1suble.f 
 |-  ( ph -> F e. B )
7 deg1suble.g 
 |-  ( ph -> G e. B )
8 eqid 
 |-  ( +g ` Y ) = ( +g ` Y )
9 1 ply1ring 
 |-  ( R e. Ring -> Y e. Ring )
10 ringgrp 
 |-  ( Y e. Ring -> Y e. Grp )
11 3 9 10 3syl 
 |-  ( ph -> Y e. Grp )
12 eqid 
 |-  ( invg ` Y ) = ( invg ` Y )
13 4 12 grpinvcl 
 |-  ( ( Y e. Grp /\ G e. B ) -> ( ( invg ` Y ) ` G ) e. B )
14 11 7 13 syl2anc 
 |-  ( ph -> ( ( invg ` Y ) ` G ) e. B )
15 1 2 3 4 8 6 14 deg1addle 
 |-  ( ph -> ( D ` ( F ( +g ` Y ) ( ( invg ` Y ) ` G ) ) ) <_ if ( ( D ` F ) <_ ( D ` ( ( invg ` Y ) ` G ) ) , ( D ` ( ( invg ` Y ) ` G ) ) , ( D ` F ) ) )
16 4 8 12 5 grpsubval 
 |-  ( ( F e. B /\ G e. B ) -> ( F .- G ) = ( F ( +g ` Y ) ( ( invg ` Y ) ` G ) ) )
17 6 7 16 syl2anc 
 |-  ( ph -> ( F .- G ) = ( F ( +g ` Y ) ( ( invg ` Y ) ` G ) ) )
18 17 fveq2d 
 |-  ( ph -> ( D ` ( F .- G ) ) = ( D ` ( F ( +g ` Y ) ( ( invg ` Y ) ` G ) ) ) )
19 1 2 3 4 12 7 deg1invg 
 |-  ( ph -> ( D ` ( ( invg ` Y ) ` G ) ) = ( D ` G ) )
20 19 eqcomd 
 |-  ( ph -> ( D ` G ) = ( D ` ( ( invg ` Y ) ` G ) ) )
21 20 breq2d 
 |-  ( ph -> ( ( D ` F ) <_ ( D ` G ) <-> ( D ` F ) <_ ( D ` ( ( invg ` Y ) ` G ) ) ) )
22 21 20 ifbieq1d 
 |-  ( ph -> if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) = if ( ( D ` F ) <_ ( D ` ( ( invg ` Y ) ` G ) ) , ( D ` ( ( invg ` Y ) ` G ) ) , ( D ` F ) ) )
23 15 18 22 3brtr4d 
 |-  ( ph -> ( D ` ( F .- G ) ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) )