Proof of Theorem deg1add
Step | Hyp | Ref
| Expression |
1 | | deg1addle.y |
. . . 4
⊢ 𝑌 = (Poly1‘𝑅) |
2 | | deg1addle.d |
. . . 4
⊢ 𝐷 = ( deg1
‘𝑅) |
3 | | deg1addle.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
4 | | deg1addle.b |
. . . 4
⊢ 𝐵 = (Base‘𝑌) |
5 | | deg1addle.p |
. . . 4
⊢ + =
(+g‘𝑌) |
6 | | deg1addle.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
7 | | deg1addle.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ 𝐵) |
8 | 1, 2, 3, 4, 5, 6, 7 | deg1addle 23665 |
. . 3
⊢ (𝜑 → (𝐷‘(𝐹 + 𝐺)) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹))) |
9 | | deg1add.l |
. . . . 5
⊢ (𝜑 → (𝐷‘𝐺) < (𝐷‘𝐹)) |
10 | 2, 1, 4 | deg1xrcl 23646 |
. . . . . . 7
⊢ (𝐺 ∈ 𝐵 → (𝐷‘𝐺) ∈
ℝ*) |
11 | 7, 10 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐷‘𝐺) ∈
ℝ*) |
12 | 2, 1, 4 | deg1xrcl 23646 |
. . . . . . 7
⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈
ℝ*) |
13 | 6, 12 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐷‘𝐹) ∈
ℝ*) |
14 | | xrltnle 9984 |
. . . . . 6
⊢ (((𝐷‘𝐺) ∈ ℝ* ∧ (𝐷‘𝐹) ∈ ℝ*) → ((𝐷‘𝐺) < (𝐷‘𝐹) ↔ ¬ (𝐷‘𝐹) ≤ (𝐷‘𝐺))) |
15 | 11, 13, 14 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ((𝐷‘𝐺) < (𝐷‘𝐹) ↔ ¬ (𝐷‘𝐹) ≤ (𝐷‘𝐺))) |
16 | 9, 15 | mpbid 221 |
. . . 4
⊢ (𝜑 → ¬ (𝐷‘𝐹) ≤ (𝐷‘𝐺)) |
17 | 16 | iffalsed 4047 |
. . 3
⊢ (𝜑 → if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) = (𝐷‘𝐹)) |
18 | 8, 17 | breqtrd 4609 |
. 2
⊢ (𝜑 → (𝐷‘(𝐹 + 𝐺)) ≤ (𝐷‘𝐹)) |
19 | 1 | ply1ring 19439 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑌 ∈ Ring) |
20 | 3, 19 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ Ring) |
21 | 4, 5 | ringacl 18401 |
. . . 4
⊢ ((𝑌 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 + 𝐺) ∈ 𝐵) |
22 | 20, 6, 7, 21 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (𝐹 + 𝐺) ∈ 𝐵) |
23 | | nltmnf 11839 |
. . . . . 6
⊢ ((𝐷‘𝐺) ∈ ℝ* → ¬
(𝐷‘𝐺) < -∞) |
24 | 11, 23 | syl 17 |
. . . . 5
⊢ (𝜑 → ¬ (𝐷‘𝐺) < -∞) |
25 | 9 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹 = (0g‘𝑌)) → (𝐷‘𝐺) < (𝐷‘𝐹)) |
26 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝐹 = (0g‘𝑌) → (𝐷‘𝐹) = (𝐷‘(0g‘𝑌))) |
27 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(0g‘𝑌) = (0g‘𝑌) |
28 | 2, 1, 27 | deg1z 23651 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → (𝐷‘(0g‘𝑌)) = -∞) |
29 | 3, 28 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐷‘(0g‘𝑌)) = -∞) |
30 | 26, 29 | sylan9eqr 2666 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹 = (0g‘𝑌)) → (𝐷‘𝐹) = -∞) |
31 | 25, 30 | breqtrd 4609 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹 = (0g‘𝑌)) → (𝐷‘𝐺) < -∞) |
32 | 31 | ex 449 |
. . . . . 6
⊢ (𝜑 → (𝐹 = (0g‘𝑌) → (𝐷‘𝐺) < -∞)) |
33 | 32 | necon3bd 2796 |
. . . . 5
⊢ (𝜑 → (¬ (𝐷‘𝐺) < -∞ → 𝐹 ≠ (0g‘𝑌))) |
34 | 24, 33 | mpd 15 |
. . . 4
⊢ (𝜑 → 𝐹 ≠ (0g‘𝑌)) |
35 | 2, 1, 27, 4 | deg1nn0cl 23652 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ (0g‘𝑌)) → (𝐷‘𝐹) ∈
ℕ0) |
36 | 3, 6, 34, 35 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (𝐷‘𝐹) ∈
ℕ0) |
37 | | eqid 2610 |
. . . . . . 7
⊢
(+g‘𝑅) = (+g‘𝑅) |
38 | 1, 4, 5, 37 | coe1addfv 19456 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝐷‘𝐹) ∈ ℕ0) →
((coe1‘(𝐹
+ 𝐺))‘(𝐷‘𝐹)) = (((coe1‘𝐹)‘(𝐷‘𝐹))(+g‘𝑅)((coe1‘𝐺)‘(𝐷‘𝐹)))) |
39 | 3, 6, 7, 36, 38 | syl31anc 1321 |
. . . . 5
⊢ (𝜑 →
((coe1‘(𝐹
+ 𝐺))‘(𝐷‘𝐹)) = (((coe1‘𝐹)‘(𝐷‘𝐹))(+g‘𝑅)((coe1‘𝐺)‘(𝐷‘𝐹)))) |
40 | | eqid 2610 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
41 | | eqid 2610 |
. . . . . . . 8
⊢
(coe1‘𝐺) = (coe1‘𝐺) |
42 | 2, 1, 4, 40, 41 | deg1lt 23661 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝐵 ∧ (𝐷‘𝐹) ∈ ℕ0 ∧ (𝐷‘𝐺) < (𝐷‘𝐹)) → ((coe1‘𝐺)‘(𝐷‘𝐹)) = (0g‘𝑅)) |
43 | 7, 36, 9, 42 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 →
((coe1‘𝐺)‘(𝐷‘𝐹)) = (0g‘𝑅)) |
44 | 43 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 →
(((coe1‘𝐹)‘(𝐷‘𝐹))(+g‘𝑅)((coe1‘𝐺)‘(𝐷‘𝐹))) = (((coe1‘𝐹)‘(𝐷‘𝐹))(+g‘𝑅)(0g‘𝑅))) |
45 | | ringgrp 18375 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
46 | 3, 45 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Grp) |
47 | | eqid 2610 |
. . . . . . . . 9
⊢
(coe1‘𝐹) = (coe1‘𝐹) |
48 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) |
49 | 47, 4, 1, 48 | coe1f 19402 |
. . . . . . . 8
⊢ (𝐹 ∈ 𝐵 → (coe1‘𝐹):ℕ0⟶(Base‘𝑅)) |
50 | 6, 49 | syl 17 |
. . . . . . 7
⊢ (𝜑 →
(coe1‘𝐹):ℕ0⟶(Base‘𝑅)) |
51 | 50, 36 | ffvelrnd 6268 |
. . . . . 6
⊢ (𝜑 →
((coe1‘𝐹)‘(𝐷‘𝐹)) ∈ (Base‘𝑅)) |
52 | 48, 37, 40 | grprid 17276 |
. . . . . 6
⊢ ((𝑅 ∈ Grp ∧
((coe1‘𝐹)‘(𝐷‘𝐹)) ∈ (Base‘𝑅)) → (((coe1‘𝐹)‘(𝐷‘𝐹))(+g‘𝑅)(0g‘𝑅)) = ((coe1‘𝐹)‘(𝐷‘𝐹))) |
53 | 46, 51, 52 | syl2anc 691 |
. . . . 5
⊢ (𝜑 →
(((coe1‘𝐹)‘(𝐷‘𝐹))(+g‘𝑅)(0g‘𝑅)) = ((coe1‘𝐹)‘(𝐷‘𝐹))) |
54 | 39, 44, 53 | 3eqtrd 2648 |
. . . 4
⊢ (𝜑 →
((coe1‘(𝐹
+ 𝐺))‘(𝐷‘𝐹)) = ((coe1‘𝐹)‘(𝐷‘𝐹))) |
55 | 2, 1, 27, 4, 40, 47 | deg1ldg 23656 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ (0g‘𝑌)) → ((coe1‘𝐹)‘(𝐷‘𝐹)) ≠ (0g‘𝑅)) |
56 | 3, 6, 34, 55 | syl3anc 1318 |
. . . 4
⊢ (𝜑 →
((coe1‘𝐹)‘(𝐷‘𝐹)) ≠ (0g‘𝑅)) |
57 | 54, 56 | eqnetrd 2849 |
. . 3
⊢ (𝜑 →
((coe1‘(𝐹
+ 𝐺))‘(𝐷‘𝐹)) ≠ (0g‘𝑅)) |
58 | | eqid 2610 |
. . . 4
⊢
(coe1‘(𝐹 + 𝐺)) = (coe1‘(𝐹 + 𝐺)) |
59 | 2, 1, 4, 40, 58 | deg1ge 23662 |
. . 3
⊢ (((𝐹 + 𝐺) ∈ 𝐵 ∧ (𝐷‘𝐹) ∈ ℕ0 ∧
((coe1‘(𝐹
+ 𝐺))‘(𝐷‘𝐹)) ≠ (0g‘𝑅)) → (𝐷‘𝐹) ≤ (𝐷‘(𝐹 + 𝐺))) |
60 | 22, 36, 57, 59 | syl3anc 1318 |
. 2
⊢ (𝜑 → (𝐷‘𝐹) ≤ (𝐷‘(𝐹 + 𝐺))) |
61 | 2, 1, 4 | deg1xrcl 23646 |
. . . 4
⊢ ((𝐹 + 𝐺) ∈ 𝐵 → (𝐷‘(𝐹 + 𝐺)) ∈
ℝ*) |
62 | 22, 61 | syl 17 |
. . 3
⊢ (𝜑 → (𝐷‘(𝐹 + 𝐺)) ∈
ℝ*) |
63 | | xrletri3 11861 |
. . 3
⊢ (((𝐷‘(𝐹 + 𝐺)) ∈ ℝ* ∧ (𝐷‘𝐹) ∈ ℝ*) → ((𝐷‘(𝐹 + 𝐺)) = (𝐷‘𝐹) ↔ ((𝐷‘(𝐹 + 𝐺)) ≤ (𝐷‘𝐹) ∧ (𝐷‘𝐹) ≤ (𝐷‘(𝐹 + 𝐺))))) |
64 | 62, 13, 63 | syl2anc 691 |
. 2
⊢ (𝜑 → ((𝐷‘(𝐹 + 𝐺)) = (𝐷‘𝐹) ↔ ((𝐷‘(𝐹 + 𝐺)) ≤ (𝐷‘𝐹) ∧ (𝐷‘𝐹) ≤ (𝐷‘(𝐹 + 𝐺))))) |
65 | 18, 60, 64 | mpbir2and 959 |
1
⊢ (𝜑 → (𝐷‘(𝐹 + 𝐺)) = (𝐷‘𝐹)) |