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={\mathrm{Poly}}_1\left(R\right)$$
	deg1addle.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	deg1addle.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	deg1suble.b	$$⊢B={\mathrm{Base}}_Y$$
	deg1suble.m	$$⊢\underset{\dot{}}{-}={-}_Y$$
	deg1suble.f	$$⊢\phi \to F\in B$$
	deg1suble.g	$$⊢\phi \to G\in B$$
	deg1sub.l	$$⊢\phi \to D\left(G\right)<D\left(F\right)$$
Assertion	deg1sub	$$⊢\phi \to D\left(F\underset{\dot{}}{-}G\right)=D\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		deg1addle.y	$$⊢Y={\mathrm{Poly}}_1\left(R\right)$$
2		deg1addle.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
3		deg1addle.r	$$⊢\phi \to R\in \mathrm{Ring}$$
4		deg1suble.b	$$⊢B={\mathrm{Base}}_Y$$
5		deg1suble.m	$$⊢\underset{\dot{}}{-}={-}_Y$$
6		deg1suble.f	$$⊢\phi \to F\in B$$
7		deg1suble.g	$$⊢\phi \to G\in B$$
8		deg1sub.l	$$⊢\phi \to D\left(G\right)<D\left(F\right)$$
9		eqid	$$⊢{+}_Y={+}_Y$$
10		eqid	$$⊢{inv}_g\left(Y\right)={inv}_g\left(Y\right)$$
11	4 9 10 5	grpsubval	$$⊢\left(F\in B\wedge G\in B\right)\to F\underset{\dot{}}{-}G=F{+}_Y{inv}_g\left(Y\right)\left(G\right)$$
12	6 7 11	syl2anc	$$⊢\phi \to F\underset{\dot{}}{-}G=F{+}_Y{inv}_g\left(Y\right)\left(G\right)$$
13	12	fveq2d	$$⊢\phi \to D\left(F\underset{\dot{}}{-}G\right)=D\left(F{+}_Y{inv}_g\left(Y\right)\left(G\right)\right)$$
14	1	ply1ring	$$⊢R\in \mathrm{Ring}\to Y\in \mathrm{Ring}$$
15		ringgrp	$$⊢Y\in \mathrm{Ring}\to Y\in \mathrm{Grp}$$
16	3 14 15	3syl	$$⊢\phi \to Y\in \mathrm{Grp}$$
17	4 10	grpinvcl	$$⊢\left(Y\in \mathrm{Grp}\wedge G\in B\right)\to {inv}_g\left(Y\right)\left(G\right)\in B$$
18	16 7 17	syl2anc	$$⊢\phi \to {inv}_g\left(Y\right)\left(G\right)\in B$$
19	1 2 3 4 10 7	deg1invg	$$⊢\phi \to D\left({inv}_g\left(Y\right)\left(G\right)\right)=D\left(G\right)$$
20	19 8	eqbrtrd	$$⊢\phi \to D\left({inv}_g\left(Y\right)\left(G\right)\right)<D\left(F\right)$$
21	1 2 3 4 9 6 18 20	deg1add	$$⊢\phi \to D\left(F{+}_Y{inv}_g\left(Y\right)\left(G\right)\right)=D\left(F\right)$$
22	13 21	eqtrd	$$⊢\phi \to D\left(F\underset{\dot{}}{-}G\right)=D\left(F\right)$$