Theorem deg1add

Description: Exact degree of a sum 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}$$
	deg1addle.b	$$⊢B={\mathrm{Base}}_Y$$
	deg1addle.p	$$⊢\underset{\dot{}}{+}={+}_Y$$
	deg1addle.f	$$⊢\phi \to F\in B$$
	deg1addle.g	$$⊢\phi \to G\in B$$
	deg1add.l	$$⊢\phi \to D\left(G\right)<D\left(F\right)$$
Assertion	deg1add	$$⊢\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		deg1addle.b	$$⊢B={\mathrm{Base}}_Y$$
5		deg1addle.p	$$⊢\underset{\dot{}}{+}={+}_Y$$
6		deg1addle.f	$$⊢\phi \to F\in B$$
7		deg1addle.g	$$⊢\phi \to G\in B$$
8		deg1add.l	$$⊢\phi \to D\left(G\right)<D\left(F\right)$$
9	1	ply1ring	$$⊢R\in \mathrm{Ring}\to Y\in \mathrm{Ring}$$
10	3 9	syl	$$⊢\phi \to Y\in \mathrm{Ring}$$
11	4 5	ringacl	$$⊢\left(Y\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to F\underset{\dot{}}{+}G\in B$$
12	10 6 7 11	syl3anc	$$⊢\phi \to F\underset{\dot{}}{+}G\in B$$
13	2 1 4	deg1xrcl	$$⊢F\underset{\dot{}}{+}G\in B\to D\left(F\underset{\dot{}}{+}G\right)\in {ℝ}^{*}$$
14	12 13	syl	$$⊢\phi \to D\left(F\underset{\dot{}}{+}G\right)\in {ℝ}^{*}$$
15	2 1 4	deg1xrcl	$$⊢F\in B\to D\left(F\right)\in {ℝ}^{*}$$
16	6 15	syl	$$⊢\phi \to D\left(F\right)\in {ℝ}^{*}$$
17	1 2 3 4 5 6 7	deg1addle	$$⊢\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)$$
18	2 1 4	deg1xrcl	$$⊢G\in B\to D\left(G\right)\in {ℝ}^{*}$$
19	7 18	syl	$$⊢\phi \to D\left(G\right)\in {ℝ}^{*}$$
20		xrltnle	$$⊢\left(D\left(G\right)\in {ℝ}^{*}\wedge D\left(F\right)\in {ℝ}^{*}\right)\to \left(D\left(G\right)<D\left(F\right)\leftrightarrow \neg D\left(F\right)\le D\left(G\right)\right)$$
21	19 16 20	syl2anc	$$⊢\phi \to \left(D\left(G\right)<D\left(F\right)\leftrightarrow \neg D\left(F\right)\le D\left(G\right)\right)$$
22	8 21	mpbid	$$⊢\phi \to \neg D\left(F\right)\le D\left(G\right)$$
23	22	iffalsed	$$⊢\phi \to if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)=D\left(F\right)$$
24	17 23	breqtrd	$$⊢\phi \to D\left(F\underset{\dot{}}{+}G\right)\le D\left(F\right)$$
25		nltmnf	$$⊢D\left(G\right)\in {ℝ}^{*}\to \neg D\left(G\right)<\mathrm{-\infty }$$
26	19 25	syl	$$⊢\phi \to \neg D\left(G\right)<\mathrm{-\infty }$$
27	8	adantr	$$⊢\left(\phi \wedge F=0_Y\right)\to D\left(G\right)<D\left(F\right)$$
28		fveq2	$$⊢F=0_Y\to D\left(F\right)=D\left(0_Y\right)$$
29		eqid	$$⊢0_Y=0_Y$$
30	2 1 29	deg1z	$$⊢R\in \mathrm{Ring}\to D\left(0_Y\right)=\mathrm{-\infty }$$
31	3 30	syl	$$⊢\phi \to D\left(0_Y\right)=\mathrm{-\infty }$$
32	28 31	sylan9eqr	$$⊢\left(\phi \wedge F=0_Y\right)\to D\left(F\right)=\mathrm{-\infty }$$
33	27 32	breqtrd	$$⊢\left(\phi \wedge F=0_Y\right)\to D\left(G\right)<\mathrm{-\infty }$$
34	33	ex	$$⊢\phi \to \left(F=0_Y\to D\left(G\right)<\mathrm{-\infty }\right)$$
35	34	necon3bd	$$⊢\phi \to \left(\neg D\left(G\right)<\mathrm{-\infty }\to F\ne 0_Y\right)$$
36	26 35	mpd	$$⊢\phi \to F\ne 0_Y$$
37	2 1 29 4	deg1nn0cl	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge F\ne 0_Y\right)\to D\left(F\right)\in {\mathbb{N}}_0$$
38	3 6 36 37	syl3anc	$$⊢\phi \to D\left(F\right)\in {\mathbb{N}}_0$$
39		eqid	$$⊢{+}_R={+}_R$$
40	1 4 5 39	coe1addfv	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge D\left(F\right)\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(F\underset{\dot{}}{+}G\right)\left(D\left(F\right)\right)={\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right){+}_R{\mathrm{coe}}_1\left(G\right)\left(D\left(F\right)\right)$$
41	3 6 7 38 40	syl31anc	$$⊢\phi \to {\mathrm{coe}}_1\left(F\underset{\dot{}}{+}G\right)\left(D\left(F\right)\right)={\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right){+}_R{\mathrm{coe}}_1\left(G\right)\left(D\left(F\right)\right)$$
42		eqid	$$⊢0_R=0_R$$
43		eqid	$$⊢{\mathrm{coe}}_1\left(G\right)={\mathrm{coe}}_1\left(G\right)$$
44	2 1 4 42 43	deg1lt	$$⊢\left(G\in B\wedge D\left(F\right)\in {\mathbb{N}}_0\wedge D\left(G\right)<D\left(F\right)\right)\to {\mathrm{coe}}_1\left(G\right)\left(D\left(F\right)\right)=0_R$$
45	7 38 8 44	syl3anc	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(D\left(F\right)\right)=0_R$$
46	45	oveq2d	$$⊢\phi \to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right){+}_R{\mathrm{coe}}_1\left(G\right)\left(D\left(F\right)\right)={\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right){+}_R{0}_R$$
47		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
48	3 47	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
49		eqid	$$⊢{\mathrm{coe}}_1\left(F\right)={\mathrm{coe}}_1\left(F\right)$$
50		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
51	49 4 1 50	coe1f	$$⊢F\in B\to {\mathrm{coe}}_1\left(F\right):{\mathbb{N}}_0⟶{\mathrm{Base}}_R$$
52	6 51	syl	$$⊢\phi \to {\mathrm{coe}}_1\left(F\right):{\mathbb{N}}_0⟶{\mathrm{Base}}_R$$
53	52 38	ffvelcdmd	$$⊢\phi \to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)\in {\mathrm{Base}}_R$$
54	50 39 42	grprid	$$⊢\left(R\in \mathrm{Grp}\wedge {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)\in {\mathrm{Base}}_R\right)\to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right){+}_R{0}_R={\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)$$
55	48 53 54	syl2anc	$$⊢\phi \to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right){+}_R{0}_R={\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)$$
56	41 46 55	3eqtrd	$$⊢\phi \to {\mathrm{coe}}_1\left(F\underset{\dot{}}{+}G\right)\left(D\left(F\right)\right)={\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)$$
57	2 1 29 4 42 49	deg1ldg	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge F\ne 0_Y\right)\to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)\ne 0_R$$
58	3 6 36 57	syl3anc	$$⊢\phi \to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)\ne 0_R$$
59	56 58	eqnetrd	$$⊢\phi \to {\mathrm{coe}}_1\left(F\underset{\dot{}}{+}G\right)\left(D\left(F\right)\right)\ne 0_R$$
60		eqid	$$⊢{\mathrm{coe}}_1\left(F\underset{\dot{}}{+}G\right)={\mathrm{coe}}_1\left(F\underset{\dot{}}{+}G\right)$$
61	2 1 4 42 60	deg1ge	$$⊢\left(F\underset{\dot{}}{+}G\in B\wedge D\left(F\right)\in {\mathbb{N}}_0\wedge {\mathrm{coe}}_1\left(F\underset{\dot{}}{+}G\right)\left(D\left(F\right)\right)\ne 0_R\right)\to D\left(F\right)\le D\left(F\underset{\dot{}}{+}G\right)$$
62	12 38 59 61	syl3anc	$$⊢\phi \to D\left(F\right)\le D\left(F\underset{\dot{}}{+}G\right)$$
63	14 16 24 62	xrletrid	$$⊢\phi \to D\left(F\underset{\dot{}}{+}G\right)=D\left(F\right)$$