Theorem deg1sub

Description: Exact degree of a difference of two polynomials of unequal degree. (Contributed by Stefan O'Rear, 28-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 )
	deg1sub.l	|- ( ph -> ( D ` G ) < ( D ` F ) )
Assertion	deg1sub	|- ( ph -> ( D ` ( F .- 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		deg1sub.l	|- ( ph -> ( D ` G ) < ( D ` F ) )
9		eqid	|- ( +g ` Y ) = ( +g ` Y )
10		eqid	|- ( invg ` Y ) = ( invg ` Y )
11	4 9 10 5	grpsubval	|- ( ( F e. B /\ G e. B ) -> ( F .- G ) = ( F ( +g ` Y ) ( ( invg ` Y ) ` G ) ) )
12	6 7 11	syl2anc	|- ( ph -> ( F .- G ) = ( F ( +g ` Y ) ( ( invg ` Y ) ` G ) ) )
13	12	fveq2d	|- ( ph -> ( D ` ( F .- G ) ) = ( D ` ( F ( +g ` Y ) ( ( invg ` Y ) ` G ) ) ) )
14	1	ply1ring	|- ( R e. Ring -> Y e. Ring )
15		ringgrp	|- ( Y e. Ring -> Y e. Grp )
16	3 14 15	3syl	|- ( ph -> Y e. Grp )
17	4 10	grpinvcl	|- ( ( Y e. Grp /\ G e. B ) -> ( ( invg ` Y ) ` G ) e. B )
18	16 7 17	syl2anc	|- ( ph -> ( ( invg ` Y ) ` G ) e. B )
19	1 2 3 4 10 7	deg1invg	|- ( ph -> ( D ` ( ( invg ` Y ) ` G ) ) = ( D ` G ) )
20	19 8	eqbrtrd	|- ( ph -> ( D ` ( ( invg ` Y ) ` G ) ) < ( D ` F ) )
21	1 2 3 4 9 6 18 20	deg1add	|- ( ph -> ( D ` ( F ( +g ` Y ) ( ( invg ` Y ) ` G ) ) ) = ( D ` F ) )
22	13 21	eqtrd	|- ( ph -> ( D ` ( F .- G ) ) = ( D ` F ) )