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