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

Metamath Proof Explorer

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