This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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