Theorem deg1submon1p

Description: The difference of two monic polynomials of the same degree is a polynomial of lesser degree. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	deg1submon1p.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1submon1p.o	⊢ 𝑂 = ( Monic1p ‘ 𝑅 )
	deg1submon1p.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	deg1submon1p.m	⊢ − = ( -g ‘ 𝑃 )
	deg1submon1p.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	deg1submon1p.f1	⊢ ( 𝜑 → 𝐹 ∈ 𝑂 )
	deg1submon1p.f2	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) = 𝑋 )
	deg1submon1p.g1	⊢ ( 𝜑 → 𝐺 ∈ 𝑂 )
	deg1submon1p.g2	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) = 𝑋 )
Assertion	deg1submon1p	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) < 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		deg1submon1p.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		deg1submon1p.o	⊢ 𝑂 = ( Monic1p ‘ 𝑅 )
3		deg1submon1p.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4		deg1submon1p.m	⊢ − = ( -g ‘ 𝑃 )
5		deg1submon1p.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6		deg1submon1p.f1	⊢ ( 𝜑 → 𝐹 ∈ 𝑂 )
7		deg1submon1p.f2	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) = 𝑋 )
8		deg1submon1p.g1	⊢ ( 𝜑 → 𝐺 ∈ 𝑂 )
9		deg1submon1p.g2	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) = 𝑋 )
10		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
11	3 10 2	mon1pcl	⊢ ( 𝐹 ∈ 𝑂 → 𝐹 ∈ ( Base ‘ 𝑃 ) )
12	6 11	syl	⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ 𝑃 ) )
13		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
14	3 13 2	mon1pn0	⊢ ( 𝐹 ∈ 𝑂 → 𝐹 ≠ ( 0g ‘ 𝑃 ) )
15	6 14	syl	⊢ ( 𝜑 → 𝐹 ≠ ( 0g ‘ 𝑃 ) )
16	1 3 13 10	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ ( Base ‘ 𝑃 ) ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
17	5 12 15 16	syl3anc	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
18	7 17	eqeltrrd	⊢ ( 𝜑 → 𝑋 ∈ ℕ0 )
19	18	nn0red	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
20	19	leidd	⊢ ( 𝜑 → 𝑋 ≤ 𝑋 )
21	7 20	eqbrtrd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ 𝑋 )
22	3 10 2	mon1pcl	⊢ ( 𝐺 ∈ 𝑂 → 𝐺 ∈ ( Base ‘ 𝑃 ) )
23	8 22	syl	⊢ ( 𝜑 → 𝐺 ∈ ( Base ‘ 𝑃 ) )
24	9 20	eqbrtrd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ≤ 𝑋 )
25		eqid	⊢ ( coe1 ‘ 𝐹 ) = ( coe1 ‘ 𝐹 )
26		eqid	⊢ ( coe1 ‘ 𝐺 ) = ( coe1 ‘ 𝐺 )
27	7	fveq2d	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) = ( ( coe1 ‘ 𝐹 ) ‘ 𝑋 ) )
28		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
29	1 28 2	mon1pldg	⊢ ( 𝐹 ∈ 𝑂 → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) = ( 1r ‘ 𝑅 ) )
30	6 29	syl	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) = ( 1r ‘ 𝑅 ) )
31	27 30	eqtr3d	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐹 ) ‘ 𝑋 ) = ( 1r ‘ 𝑅 ) )
32	1 28 2	mon1pldg	⊢ ( 𝐺 ∈ 𝑂 → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) = ( 1r ‘ 𝑅 ) )
33	8 32	syl	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) = ( 1r ‘ 𝑅 ) )
34	9	fveq2d	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) = ( ( coe1 ‘ 𝐺 ) ‘ 𝑋 ) )
35	31 33 34	3eqtr2d	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐹 ) ‘ 𝑋 ) = ( ( coe1 ‘ 𝐺 ) ‘ 𝑋 ) )
36	1 3 10 4 18 5 12 21 23 24 25 26 35	deg1sublt	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 − 𝐺 ) ) < 𝑋 )