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	⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
	deg1addle.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1addle.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	deg1addle.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	deg1addle.p	⊢ + = ( +g ‘ 𝑌 )
	deg1addle.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	deg1addle.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
	deg1add.l	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) < ( 𝐷 ‘ 𝐹 ) )
Assertion	deg1add	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) = ( 𝐷 ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		deg1addle.y	⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
2		deg1addle.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
3		deg1addle.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		deg1addle.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
5		deg1addle.p	⊢ + = ( +g ‘ 𝑌 )
6		deg1addle.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7		deg1addle.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
8		deg1add.l	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) < ( 𝐷 ‘ 𝐹 ) )
9	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑌 ∈ Ring )
10	3 9	syl	⊢ ( 𝜑 → 𝑌 ∈ Ring )
11	4 5	ringacl	⊢ ( ( 𝑌 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 + 𝐺 ) ∈ 𝐵 )
12	10 6 7 11	syl3anc	⊢ ( 𝜑 → ( 𝐹 + 𝐺 ) ∈ 𝐵 )
13	2 1 4	deg1xrcl	⊢ ( ( 𝐹 + 𝐺 ) ∈ 𝐵 → ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) ∈ ℝ* )
14	12 13	syl	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) ∈ ℝ* )
15	2 1 4	deg1xrcl	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* )
16	6 15	syl	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* )
17	1 2 3 4 5 6 7	deg1addle	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) )
18	2 1 4	deg1xrcl	⊢ ( 𝐺 ∈ 𝐵 → ( 𝐷 ‘ 𝐺 ) ∈ ℝ* )
19	7 18	syl	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ∈ ℝ* )
20		xrltnle	⊢ ( ( ( 𝐷 ‘ 𝐺 ) ∈ ℝ* ∧ ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ) → ( ( 𝐷 ‘ 𝐺 ) < ( 𝐷 ‘ 𝐹 ) ↔ ¬ ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) ) )
21	19 16 20	syl2anc	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐺 ) < ( 𝐷 ‘ 𝐹 ) ↔ ¬ ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) ) )
22	8 21	mpbid	⊢ ( 𝜑 → ¬ ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) )
23	22	iffalsed	⊢ ( 𝜑 → if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) = ( 𝐷 ‘ 𝐹 ) )
24	17 23	breqtrd	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) ≤ ( 𝐷 ‘ 𝐹 ) )
25		nltmnf	⊢ ( ( 𝐷 ‘ 𝐺 ) ∈ ℝ* → ¬ ( 𝐷 ‘ 𝐺 ) < -∞ )
26	19 25	syl	⊢ ( 𝜑 → ¬ ( 𝐷 ‘ 𝐺 ) < -∞ )
27	8	adantr	⊢ ( ( 𝜑 ∧ 𝐹 = ( 0g ‘ 𝑌 ) ) → ( 𝐷 ‘ 𝐺 ) < ( 𝐷 ‘ 𝐹 ) )
28		fveq2	⊢ ( 𝐹 = ( 0g ‘ 𝑌 ) → ( 𝐷 ‘ 𝐹 ) = ( 𝐷 ‘ ( 0g ‘ 𝑌 ) ) )
29		eqid	⊢ ( 0g ‘ 𝑌 ) = ( 0g ‘ 𝑌 )
30	2 1 29	deg1z	⊢ ( 𝑅 ∈ Ring → ( 𝐷 ‘ ( 0g ‘ 𝑌 ) ) = -∞ )
31	3 30	syl	⊢ ( 𝜑 → ( 𝐷 ‘ ( 0g ‘ 𝑌 ) ) = -∞ )
32	28 31	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝐹 = ( 0g ‘ 𝑌 ) ) → ( 𝐷 ‘ 𝐹 ) = -∞ )
33	27 32	breqtrd	⊢ ( ( 𝜑 ∧ 𝐹 = ( 0g ‘ 𝑌 ) ) → ( 𝐷 ‘ 𝐺 ) < -∞ )
34	33	ex	⊢ ( 𝜑 → ( 𝐹 = ( 0g ‘ 𝑌 ) → ( 𝐷 ‘ 𝐺 ) < -∞ ) )
35	34	necon3bd	⊢ ( 𝜑 → ( ¬ ( 𝐷 ‘ 𝐺 ) < -∞ → 𝐹 ≠ ( 0g ‘ 𝑌 ) ) )
36	26 35	mpd	⊢ ( 𝜑 → 𝐹 ≠ ( 0g ‘ 𝑌 ) )
37	2 1 29 4	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ ( 0g ‘ 𝑌 ) ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
38	3 6 36 37	syl3anc	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
39		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
40	1 4 5 39	coe1addfv	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐹 + 𝐺 ) ) ‘ ( 𝐷 ‘ 𝐹 ) ) = ( ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ) )
41	3 6 7 38 40	syl31anc	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝐹 + 𝐺 ) ) ‘ ( 𝐷 ‘ 𝐹 ) ) = ( ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ) )
42		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
43		eqid	⊢ ( coe1 ‘ 𝐺 ) = ( coe1 ‘ 𝐺 )
44	2 1 4 42 43	deg1lt	⊢ ( ( 𝐺 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝐷 ‘ 𝐺 ) < ( 𝐷 ‘ 𝐹 ) ) → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐹 ) ) = ( 0g ‘ 𝑅 ) )
45	7 38 8 44	syl3anc	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐹 ) ) = ( 0g ‘ 𝑅 ) )
46	45	oveq2d	⊢ ( 𝜑 → ( ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ) = ( ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
47		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
48	3 47	syl	⊢ ( 𝜑 → 𝑅 ∈ Grp )
49		eqid	⊢ ( coe1 ‘ 𝐹 ) = ( coe1 ‘ 𝐹 )
50		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
51	49 4 1 50	coe1f	⊢ ( 𝐹 ∈ 𝐵 → ( coe1 ‘ 𝐹 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
52	6 51	syl	⊢ ( 𝜑 → ( coe1 ‘ 𝐹 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
53	52 38	ffvelrnd	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ ( Base ‘ 𝑅 ) )
54	50 39 42	grprid	⊢ ( ( 𝑅 ∈ Grp ∧ ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) )
55	48 53 54	syl2anc	⊢ ( 𝜑 → ( ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) )
56	41 46 55	3eqtrd	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝐹 + 𝐺 ) ) ‘ ( 𝐷 ‘ 𝐹 ) ) = ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) )
57	2 1 29 4 42 49	deg1ldg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ ( 0g ‘ 𝑌 ) ) → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ ( 0g ‘ 𝑅 ) )
58	3 6 36 57	syl3anc	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ ( 0g ‘ 𝑅 ) )
59	56 58	eqnetrd	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝐹 + 𝐺 ) ) ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ ( 0g ‘ 𝑅 ) )
60		eqid	⊢ ( coe1 ‘ ( 𝐹 + 𝐺 ) ) = ( coe1 ‘ ( 𝐹 + 𝐺 ) )
61	2 1 4 42 60	deg1ge	⊢ ( ( ( 𝐹 + 𝐺 ) ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ∧ ( ( coe1 ‘ ( 𝐹 + 𝐺 ) ) ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) )
62	12 38 59 61	syl3anc	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) )
63	14 16 24 62	xrletrid	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 + 𝐺 ) ) = ( 𝐷 ‘ 𝐹 ) )