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={\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$$
Assertion	deg1suble	$$⊢\phi \to D\left(F\underset{\dot{}}{-}G\right)\le if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\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		eqid	$$⊢{+}_Y={+}_Y$$
9	1	ply1ring	$$⊢R\in \mathrm{Ring}\to Y\in \mathrm{Ring}$$
10		ringgrp	$$⊢Y\in \mathrm{Ring}\to Y\in \mathrm{Grp}$$
11	3 9 10	3syl	$$⊢\phi \to Y\in \mathrm{Grp}$$
12		eqid	$$⊢{inv}_g\left(Y\right)={inv}_g\left(Y\right)$$
13	4 12	grpinvcl	$$⊢\left(Y\in \mathrm{Grp}\wedge G\in B\right)\to {inv}_g\left(Y\right)\left(G\right)\in B$$
14	11 7 13	syl2anc	$$⊢\phi \to {inv}_g\left(Y\right)\left(G\right)\in B$$
15	1 2 3 4 8 6 14	deg1addle	$$⊢\phi \to D\left(F{+}_Y{inv}_g\left(Y\right)\left(G\right)\right)\le if\left(D\left(F\right)\le D\left({inv}_g\left(Y\right)\left(G\right)\right),D\left({inv}_g\left(Y\right)\left(G\right)\right),D\left(F\right)\right)$$
16	4 8 12 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)$$
17	6 7 16	syl2anc	$$⊢\phi \to F\underset{\dot{}}{-}G=F{+}_Y{inv}_g\left(Y\right)\left(G\right)$$
18	17	fveq2d	$$⊢\phi \to D\left(F\underset{\dot{}}{-}G\right)=D\left(F{+}_Y{inv}_g\left(Y\right)\left(G\right)\right)$$
19	1 2 3 4 12 7	deg1invg	$$⊢\phi \to D\left({inv}_g\left(Y\right)\left(G\right)\right)=D\left(G\right)$$
20	19	eqcomd	$$⊢\phi \to D\left(G\right)=D\left({inv}_g\left(Y\right)\left(G\right)\right)$$
21	20	breq2d	$$⊢\phi \to \left(D\left(F\right)\le D\left(G\right)\leftrightarrow D\left(F\right)\le D\left({inv}_g\left(Y\right)\left(G\right)\right)\right)$$
22	21 20	ifbieq1d	$$⊢\phi \to if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)=if\left(D\left(F\right)\le D\left({inv}_g\left(Y\right)\left(G\right)\right),D\left({inv}_g\left(Y\right)\left(G\right)\right),D\left(F\right)\right)$$
23	15 18 22	3brtr4d	$$⊢\phi \to D\left(F\underset{\dot{}}{-}G\right)\le if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)$$