Metamath Proof Explorer


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 ( 𝜑 → ( 𝐷 ‘ ( 𝐹 𝐺 ) ) < 𝑋 )