Step | Hyp | Ref
| Expression |
1 | | hbtlem4.r |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Ring) |
2 | 1 | ad2antrr 724 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → 𝑅 ∈ Ring) |
3 | | hbtlem.p |
. . . . . . . . . 10
⊢ 𝑃 = (Poly1‘𝑅) |
4 | 3 | ply1ring 21619 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
5 | 2, 4 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → 𝑃 ∈ Ring) |
6 | | hbtlem4.i |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ 𝑈) |
7 | 6 | ad2antrr 724 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → 𝐼 ∈ 𝑈) |
8 | | eqid 2736 |
. . . . . . . . . 10
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
9 | | eqid 2736 |
. . . . . . . . . 10
⊢
(Base‘𝑃) =
(Base‘𝑃) |
10 | 8, 9 | mgpbas 19902 |
. . . . . . . . 9
⊢
(Base‘𝑃) =
(Base‘(mulGrp‘𝑃)) |
11 | | eqid 2736 |
. . . . . . . . 9
⊢
(.g‘(mulGrp‘𝑃)) =
(.g‘(mulGrp‘𝑃)) |
12 | 8 | ringmgp 19970 |
. . . . . . . . . 10
⊢ (𝑃 ∈ Ring →
(mulGrp‘𝑃) ∈
Mnd) |
13 | 5, 12 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → (mulGrp‘𝑃) ∈ Mnd) |
14 | | hbtlem4.x |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈
ℕ0) |
15 | 14 | ad2antrr 724 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → 𝑋 ∈
ℕ0) |
16 | | hbtlem4.y |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈
ℕ0) |
17 | 16 | ad2antrr 724 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → 𝑌 ∈
ℕ0) |
18 | | hbtlem4.xy |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ≤ 𝑌) |
19 | 18 | ad2antrr 724 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → 𝑋 ≤ 𝑌) |
20 | | nn0sub2 12564 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℕ0
∧ 𝑌 ∈
ℕ0 ∧ 𝑋
≤ 𝑌) → (𝑌 − 𝑋) ∈
ℕ0) |
21 | 15, 17, 19, 20 | syl3anc 1371 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → (𝑌 − 𝑋) ∈
ℕ0) |
22 | | eqid 2736 |
. . . . . . . . . . 11
⊢
(var1‘𝑅) = (var1‘𝑅) |
23 | 22, 3, 9 | vr1cl 21588 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring →
(var1‘𝑅)
∈ (Base‘𝑃)) |
24 | 2, 23 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → (var1‘𝑅) ∈ (Base‘𝑃)) |
25 | 10, 11, 13, 21, 24 | mulgnn0cld 18897 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → ((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝑃)) |
26 | | simplr 767 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → 𝑐 ∈ 𝐼) |
27 | | hbtlem.u |
. . . . . . . . 9
⊢ 𝑈 = (LIdeal‘𝑃) |
28 | | eqid 2736 |
. . . . . . . . 9
⊢
(.r‘𝑃) = (.r‘𝑃) |
29 | 27, 9, 28 | lidlmcl 20687 |
. . . . . . . 8
⊢ (((𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ (((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝑃) ∧ 𝑐 ∈ 𝐼)) → (((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐) ∈ 𝐼) |
30 | 5, 7, 25, 26, 29 | syl22anc 837 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → (((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐) ∈ 𝐼) |
31 | | eqid 2736 |
. . . . . . . . 9
⊢ (
deg1 ‘𝑅) =
( deg1 ‘𝑅) |
32 | 9, 27 | lidlss 20680 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ 𝑈 → 𝐼 ⊆ (Base‘𝑃)) |
33 | 7, 32 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → 𝐼 ⊆ (Base‘𝑃)) |
34 | 33, 26 | sseldd 3945 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → 𝑐 ∈ (Base‘𝑃)) |
35 | 31, 3, 22, 8, 11 | deg1pwle 25484 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝑌 − 𝑋) ∈ ℕ0) → ((
deg1 ‘𝑅)‘((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ≤ (𝑌 − 𝑋)) |
36 | 2, 21, 35 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → (( deg1 ‘𝑅)‘((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ≤ (𝑌 − 𝑋)) |
37 | | simpr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) |
38 | 3, 31, 2, 9, 28, 25, 34, 21, 15, 36, 37 | deg1mulle2 25474 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → (( deg1 ‘𝑅)‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐)) ≤ ((𝑌 − 𝑋) + 𝑋)) |
39 | 17 | nn0cnd 12475 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → 𝑌 ∈ ℂ) |
40 | 15 | nn0cnd 12475 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → 𝑋 ∈ ℂ) |
41 | 39, 40 | npcand 11516 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → ((𝑌 − 𝑋) + 𝑋) = 𝑌) |
42 | 38, 41 | breqtrd 5131 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → (( deg1 ‘𝑅)‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐)) ≤ 𝑌) |
43 | | eqid 2736 |
. . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) |
44 | 43, 3, 22, 8, 11, 9, 28, 2, 34, 21, 15 | coe1pwmulfv 21651 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → ((coe1‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐))‘((𝑌 − 𝑋) + 𝑋)) = ((coe1‘𝑐)‘𝑋)) |
45 | 41 | fveq2d 6846 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → ((coe1‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐))‘((𝑌 − 𝑋) + 𝑋)) = ((coe1‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐))‘𝑌)) |
46 | 44, 45 | eqtr3d 2778 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → ((coe1‘𝑐)‘𝑋) = ((coe1‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐))‘𝑌)) |
47 | | fveq2 6842 |
. . . . . . . . . 10
⊢ (𝑏 = (((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐) → (( deg1 ‘𝑅)‘𝑏) = (( deg1 ‘𝑅)‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐))) |
48 | 47 | breq1d 5115 |
. . . . . . . . 9
⊢ (𝑏 = (((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐) → ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ↔ (( deg1 ‘𝑅)‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐)) ≤ 𝑌)) |
49 | | fveq2 6842 |
. . . . . . . . . . 11
⊢ (𝑏 = (((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐) → (coe1‘𝑏) =
(coe1‘(((𝑌
− 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐))) |
50 | 49 | fveq1d 6844 |
. . . . . . . . . 10
⊢ (𝑏 = (((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐) → ((coe1‘𝑏)‘𝑌) = ((coe1‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐))‘𝑌)) |
51 | 50 | eqeq2d 2747 |
. . . . . . . . 9
⊢ (𝑏 = (((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐) → (((coe1‘𝑐)‘𝑋) = ((coe1‘𝑏)‘𝑌) ↔ ((coe1‘𝑐)‘𝑋) = ((coe1‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐))‘𝑌))) |
52 | 48, 51 | anbi12d 631 |
. . . . . . . 8
⊢ (𝑏 = (((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐) → (((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ ((coe1‘𝑐)‘𝑋) = ((coe1‘𝑏)‘𝑌)) ↔ ((( deg1 ‘𝑅)‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐)) ≤ 𝑌 ∧ ((coe1‘𝑐)‘𝑋) = ((coe1‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐))‘𝑌)))) |
53 | 52 | rspcev 3581 |
. . . . . . 7
⊢
(((((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐) ∈ 𝐼 ∧ ((( deg1 ‘𝑅)‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐)) ≤ 𝑌 ∧ ((coe1‘𝑐)‘𝑋) = ((coe1‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐))‘𝑌))) → ∃𝑏 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ ((coe1‘𝑐)‘𝑋) = ((coe1‘𝑏)‘𝑌))) |
54 | 30, 42, 46, 53 | syl12anc 835 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → ∃𝑏 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ ((coe1‘𝑐)‘𝑋) = ((coe1‘𝑏)‘𝑌))) |
55 | | eqeq1 2740 |
. . . . . . . 8
⊢ (𝑎 = ((coe1‘𝑐)‘𝑋) → (𝑎 = ((coe1‘𝑏)‘𝑌) ↔ ((coe1‘𝑐)‘𝑋) = ((coe1‘𝑏)‘𝑌))) |
56 | 55 | anbi2d 629 |
. . . . . . 7
⊢ (𝑎 = ((coe1‘𝑐)‘𝑋) → (((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ 𝑎 = ((coe1‘𝑏)‘𝑌)) ↔ ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ ((coe1‘𝑐)‘𝑋) = ((coe1‘𝑏)‘𝑌)))) |
57 | 56 | rexbidv 3175 |
. . . . . 6
⊢ (𝑎 = ((coe1‘𝑐)‘𝑋) → (∃𝑏 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ 𝑎 = ((coe1‘𝑏)‘𝑌)) ↔ ∃𝑏 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ ((coe1‘𝑐)‘𝑋) = ((coe1‘𝑏)‘𝑌)))) |
58 | 54, 57 | syl5ibrcom 246 |
. . . . 5
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → (𝑎 = ((coe1‘𝑐)‘𝑋) → ∃𝑏 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ 𝑎 = ((coe1‘𝑏)‘𝑌)))) |
59 | 58 | expimpd 454 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (((( deg1 ‘𝑅)‘𝑐) ≤ 𝑋 ∧ 𝑎 = ((coe1‘𝑐)‘𝑋)) → ∃𝑏 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ 𝑎 = ((coe1‘𝑏)‘𝑌)))) |
60 | 59 | rexlimdva 3152 |
. . 3
⊢ (𝜑 → (∃𝑐 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑐) ≤ 𝑋 ∧ 𝑎 = ((coe1‘𝑐)‘𝑋)) → ∃𝑏 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ 𝑎 = ((coe1‘𝑏)‘𝑌)))) |
61 | 60 | ss2abdv 4020 |
. 2
⊢ (𝜑 → {𝑎 ∣ ∃𝑐 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑐) ≤ 𝑋 ∧ 𝑎 = ((coe1‘𝑐)‘𝑋))} ⊆ {𝑎 ∣ ∃𝑏 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ 𝑎 = ((coe1‘𝑏)‘𝑌))}) |
62 | | hbtlem.s |
. . . 4
⊢ 𝑆 = (ldgIdlSeq‘𝑅) |
63 | 3, 27, 62, 31 | hbtlem1 41436 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑋) = {𝑎 ∣ ∃𝑐 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑐) ≤ 𝑋 ∧ 𝑎 = ((coe1‘𝑐)‘𝑋))}) |
64 | 1, 6, 14, 63 | syl3anc 1371 |
. 2
⊢ (𝜑 → ((𝑆‘𝐼)‘𝑋) = {𝑎 ∣ ∃𝑐 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑐) ≤ 𝑋 ∧ 𝑎 = ((coe1‘𝑐)‘𝑋))}) |
65 | 3, 27, 62, 31 | hbtlem1 41436 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑌 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑌) = {𝑎 ∣ ∃𝑏 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ 𝑎 = ((coe1‘𝑏)‘𝑌))}) |
66 | 1, 6, 16, 65 | syl3anc 1371 |
. 2
⊢ (𝜑 → ((𝑆‘𝐼)‘𝑌) = {𝑎 ∣ ∃𝑏 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ 𝑎 = ((coe1‘𝑏)‘𝑌))}) |
67 | 61, 64, 66 | 3sstr4d 3991 |
1
⊢ (𝜑 → ((𝑆‘𝐼)‘𝑋) ⊆ ((𝑆‘𝐼)‘𝑌)) |