Theorem deg1sublt

Description: Subtraction of two polynomials limited to the same degree with the same leading coefficient gives a polynomial with a smaller degree. (Contributed by Stefan O'Rear, 26-Mar-2015)

	Ref	Expression
Hypotheses	deg1sublt.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1sublt.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	deg1sublt.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	deg1sublt.m	⊢ − = ( -g ‘ 𝑃 )
	deg1sublt.l	⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
	deg1sublt.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	deg1sublt.fb	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	deg1sublt.fd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ 𝐿 )
	deg1sublt.gb	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
	deg1sublt.gd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ≤ 𝐿 )
	deg1sublt.a	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
	deg1sublt.c	⊢ 𝐶 = ( coe1 ‘ 𝐺 )
	deg1sublt.eq	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐹 ) ‘ 𝐿 ) = ( ( coe1 ‘ 𝐺 ) ‘ 𝐿 ) )
Assertion	deg1sublt	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) < 𝐿 )

Proof

Step	Hyp	Ref	Expression
1		deg1sublt.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		deg1sublt.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		deg1sublt.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		deg1sublt.m	⊢ − = ( -g ‘ 𝑃 )
5		deg1sublt.l	⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
6		deg1sublt.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
7		deg1sublt.fb	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
8		deg1sublt.fd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ 𝐿 )
9		deg1sublt.gb	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
10		deg1sublt.gd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ≤ 𝐿 )
11		deg1sublt.a	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
12		deg1sublt.c	⊢ 𝐶 = ( coe1 ‘ 𝐺 )
13		deg1sublt.eq	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐹 ) ‘ 𝐿 ) = ( ( coe1 ‘ 𝐺 ) ‘ 𝐿 ) )
14		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
15		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
16		eqid	⊢ ( coe1 ‘ ( 𝐹 − 𝐺 ) ) = ( coe1 ‘ ( 𝐹 − 𝐺 ) )
17	2	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
18		ringgrp	⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ Grp )
19	6 17 18	3syl	⊢ ( 𝜑 → 𝑃 ∈ Grp )
20	3 4	grpsubcl	⊢ ( ( 𝑃 ∈ Grp ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 − 𝐺 ) ∈ 𝐵 )
21	19 7 9 20	syl3anc	⊢ ( 𝜑 → ( 𝐹 − 𝐺 ) ∈ 𝐵 )
22		eqid	⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
23	2 3 4 22	coe1subfv	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝐿 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐹 − 𝐺 ) ) ‘ 𝐿 ) = ( ( ( coe1 ‘ 𝐹 ) ‘ 𝐿 ) ( -g ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ 𝐿 ) ) )
24	6 7 9 5 23	syl31anc	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝐹 − 𝐺 ) ) ‘ 𝐿 ) = ( ( ( coe1 ‘ 𝐹 ) ‘ 𝐿 ) ( -g ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ 𝐿 ) ) )
25	13	oveq1d	⊢ ( 𝜑 → ( ( ( coe1 ‘ 𝐹 ) ‘ 𝐿 ) ( -g ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ 𝐿 ) ) = ( ( ( coe1 ‘ 𝐺 ) ‘ 𝐿 ) ( -g ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ 𝐿 ) ) )
26		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
27	6 26	syl	⊢ ( 𝜑 → 𝑅 ∈ Grp )
28		eqid	⊢ ( coe1 ‘ 𝐺 ) = ( coe1 ‘ 𝐺 )
29		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
30	28 3 2 29	coe1f	⊢ ( 𝐺 ∈ 𝐵 → ( coe1 ‘ 𝐺 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
31	9 30	syl	⊢ ( 𝜑 → ( coe1 ‘ 𝐺 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
32	31 5	ffvelcdmd	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ 𝐿 ) ∈ ( Base ‘ 𝑅 ) )
33	29 15 22	grpsubid	⊢ ( ( 𝑅 ∈ Grp ∧ ( ( coe1 ‘ 𝐺 ) ‘ 𝐿 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( coe1 ‘ 𝐺 ) ‘ 𝐿 ) ( -g ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ 𝐿 ) ) = ( 0g ‘ 𝑅 ) )
34	27 32 33	syl2anc	⊢ ( 𝜑 → ( ( ( coe1 ‘ 𝐺 ) ‘ 𝐿 ) ( -g ‘ 𝑅 ) ( ( coe1 ‘ 𝐺 ) ‘ 𝐿 ) ) = ( 0g ‘ 𝑅 ) )
35	24 25 34	3eqtrd	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝐹 − 𝐺 ) ) ‘ 𝐿 ) = ( 0g ‘ 𝑅 ) )
36	1 2 14 3 15 16 6 21 5 35	deg1ldgn	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) ≠ 𝐿 )
37	36	neneqd	⊢ ( 𝜑 → ¬ ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) = 𝐿 )
38	1 2 3	deg1xrcl	⊢ ( ( 𝐹 − 𝐺 ) ∈ 𝐵 → ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) ∈ ℝ* )
39	21 38	syl	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) ∈ ℝ* )
40	1 2 3	deg1xrcl	⊢ ( 𝐺 ∈ 𝐵 → ( 𝐷 ‘ 𝐺 ) ∈ ℝ* )
41	9 40	syl	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ∈ ℝ* )
42	1 2 3	deg1xrcl	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* )
43	7 42	syl	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* )
44	41 43	ifcld	⊢ ( 𝜑 → if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ∈ ℝ* )
45	5	nn0red	⊢ ( 𝜑 → 𝐿 ∈ ℝ )
46	45	rexrd	⊢ ( 𝜑 → 𝐿 ∈ ℝ* )
47	2 1 6 3 4 7 9	deg1suble	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) ≤ if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) )
48		xrmaxle	⊢ ( ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ ( 𝐷 ‘ 𝐺 ) ∈ ℝ* ∧ 𝐿 ∈ ℝ* ) → ( if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ≤ 𝐿 ↔ ( ( 𝐷 ‘ 𝐹 ) ≤ 𝐿 ∧ ( 𝐷 ‘ 𝐺 ) ≤ 𝐿 ) ) )
49	43 41 46 48	syl3anc	⊢ ( 𝜑 → ( if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ≤ 𝐿 ↔ ( ( 𝐷 ‘ 𝐹 ) ≤ 𝐿 ∧ ( 𝐷 ‘ 𝐺 ) ≤ 𝐿 ) ) )
50	8 10 49	mpbir2and	⊢ ( 𝜑 → if ( ( 𝐷 ‘ 𝐹 ) ≤ ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐺 ) , ( 𝐷 ‘ 𝐹 ) ) ≤ 𝐿 )
51	39 44 46 47 50	xrletrd	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) ≤ 𝐿 )
52		xrleloe	⊢ ( ( ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) ∈ ℝ* ∧ 𝐿 ∈ ℝ* ) → ( ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) ≤ 𝐿 ↔ ( ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) < 𝐿 ∨ ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) = 𝐿 ) ) )
53	39 46 52	syl2anc	⊢ ( 𝜑 → ( ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) ≤ 𝐿 ↔ ( ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) < 𝐿 ∨ ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) = 𝐿 ) ) )
54	51 53	mpbid	⊢ ( 𝜑 → ( ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) < 𝐿 ∨ ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) = 𝐿 ) )
55		orel2	⊢ ( ¬ ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) = 𝐿 → ( ( ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) < 𝐿 ∨ ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) = 𝐿 ) → ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) < 𝐿 ) )
56	37 54 55	sylc	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) < 𝐿 )