Step | Hyp | Ref
| Expression |
1 | | hbtlem4.r |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Ring) |
2 | 1 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → 𝑅 ∈ Ring) |
3 | | hbtlem.p |
. . . . . . . . . 10
⊢ 𝑃 = (Poly1‘𝑅) |
4 | 3 | ply1ring 21419 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
5 | 2, 4 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → 𝑃 ∈ Ring) |
6 | | hbtlem4.i |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ 𝑈) |
7 | 6 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → 𝐼 ∈ 𝑈) |
8 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
9 | 8 | ringmgp 19789 |
. . . . . . . . . 10
⊢ (𝑃 ∈ Ring →
(mulGrp‘𝑃) ∈
Mnd) |
10 | 5, 9 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → (mulGrp‘𝑃) ∈ Mnd) |
11 | | hbtlem4.x |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈
ℕ0) |
12 | 11 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → 𝑋 ∈
ℕ0) |
13 | | hbtlem4.y |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈
ℕ0) |
14 | 13 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → 𝑌 ∈
ℕ0) |
15 | | hbtlem4.xy |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ≤ 𝑌) |
16 | 15 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → 𝑋 ≤ 𝑌) |
17 | | nn0sub2 12381 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℕ0
∧ 𝑌 ∈
ℕ0 ∧ 𝑋
≤ 𝑌) → (𝑌 − 𝑋) ∈
ℕ0) |
18 | 12, 14, 16, 17 | syl3anc 1370 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → (𝑌 − 𝑋) ∈
ℕ0) |
19 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(var1‘𝑅) = (var1‘𝑅) |
20 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(Base‘𝑃) =
(Base‘𝑃) |
21 | 19, 3, 20 | vr1cl 21388 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring →
(var1‘𝑅)
∈ (Base‘𝑃)) |
22 | 2, 21 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → (var1‘𝑅) ∈ (Base‘𝑃)) |
23 | 8, 20 | mgpbas 19726 |
. . . . . . . . . 10
⊢
(Base‘𝑃) =
(Base‘(mulGrp‘𝑃)) |
24 | | eqid 2738 |
. . . . . . . . . 10
⊢
(.g‘(mulGrp‘𝑃)) =
(.g‘(mulGrp‘𝑃)) |
25 | 23, 24 | mulgnn0cl 18720 |
. . . . . . . . 9
⊢
(((mulGrp‘𝑃)
∈ Mnd ∧ (𝑌 −
𝑋) ∈
ℕ0 ∧ (var1‘𝑅) ∈ (Base‘𝑃)) → ((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝑃)) |
26 | 10, 18, 22, 25 | syl3anc 1370 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → ((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝑃)) |
27 | | simplr 766 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → 𝑐 ∈ 𝐼) |
28 | | hbtlem.u |
. . . . . . . . 9
⊢ 𝑈 = (LIdeal‘𝑃) |
29 | | eqid 2738 |
. . . . . . . . 9
⊢
(.r‘𝑃) = (.r‘𝑃) |
30 | 28, 20, 29 | lidlmcl 20488 |
. . . . . . . 8
⊢ (((𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ (((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝑃) ∧ 𝑐 ∈ 𝐼)) → (((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐) ∈ 𝐼) |
31 | 5, 7, 26, 27, 30 | syl22anc 836 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → (((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐) ∈ 𝐼) |
32 | | eqid 2738 |
. . . . . . . . 9
⊢ (
deg1 ‘𝑅) =
( deg1 ‘𝑅) |
33 | 20, 28 | lidlss 20481 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ 𝑈 → 𝐼 ⊆ (Base‘𝑃)) |
34 | 7, 33 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → 𝐼 ⊆ (Base‘𝑃)) |
35 | 34, 27 | sseldd 3922 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → 𝑐 ∈ (Base‘𝑃)) |
36 | 32, 3, 19, 8, 24 | deg1pwle 25284 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝑌 − 𝑋) ∈ ℕ0) → ((
deg1 ‘𝑅)‘((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ≤ (𝑌 − 𝑋)) |
37 | 2, 18, 36 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → (( deg1 ‘𝑅)‘((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ≤ (𝑌 − 𝑋)) |
38 | | simpr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) |
39 | 3, 32, 2, 20, 29, 26, 35, 18, 12, 37, 38 | deg1mulle2 25274 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → (( deg1 ‘𝑅)‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐)) ≤ ((𝑌 − 𝑋) + 𝑋)) |
40 | 14 | nn0cnd 12295 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → 𝑌 ∈ ℂ) |
41 | 12 | nn0cnd 12295 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → 𝑋 ∈ ℂ) |
42 | 40, 41 | npcand 11336 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → ((𝑌 − 𝑋) + 𝑋) = 𝑌) |
43 | 39, 42 | breqtrd 5100 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → (( deg1 ‘𝑅)‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐)) ≤ 𝑌) |
44 | | eqid 2738 |
. . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) |
45 | 44, 3, 19, 8, 24, 20, 29, 2, 35, 18, 12 | coe1pwmulfv 21451 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → ((coe1‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐))‘((𝑌 − 𝑋) + 𝑋)) = ((coe1‘𝑐)‘𝑋)) |
46 | 42 | fveq2d 6778 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → ((coe1‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐))‘((𝑌 − 𝑋) + 𝑋)) = ((coe1‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐))‘𝑌)) |
47 | 45, 46 | eqtr3d 2780 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → ((coe1‘𝑐)‘𝑋) = ((coe1‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐))‘𝑌)) |
48 | | fveq2 6774 |
. . . . . . . . . 10
⊢ (𝑏 = (((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐) → (( deg1 ‘𝑅)‘𝑏) = (( deg1 ‘𝑅)‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐))) |
49 | 48 | breq1d 5084 |
. . . . . . . . 9
⊢ (𝑏 = (((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐) → ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ↔ (( deg1 ‘𝑅)‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐)) ≤ 𝑌)) |
50 | | fveq2 6774 |
. . . . . . . . . . 11
⊢ (𝑏 = (((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐) → (coe1‘𝑏) =
(coe1‘(((𝑌
− 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐))) |
51 | 50 | fveq1d 6776 |
. . . . . . . . . 10
⊢ (𝑏 = (((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐) → ((coe1‘𝑏)‘𝑌) = ((coe1‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐))‘𝑌)) |
52 | 51 | eqeq2d 2749 |
. . . . . . . . 9
⊢ (𝑏 = (((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐) → (((coe1‘𝑐)‘𝑋) = ((coe1‘𝑏)‘𝑌) ↔ ((coe1‘𝑐)‘𝑋) = ((coe1‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐))‘𝑌))) |
53 | 49, 52 | anbi12d 631 |
. . . . . . . 8
⊢ (𝑏 = (((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐) → (((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ ((coe1‘𝑐)‘𝑋) = ((coe1‘𝑏)‘𝑌)) ↔ ((( deg1 ‘𝑅)‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐)) ≤ 𝑌 ∧ ((coe1‘𝑐)‘𝑋) = ((coe1‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐))‘𝑌)))) |
54 | 53 | rspcev 3561 |
. . . . . . 7
⊢
(((((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐) ∈ 𝐼 ∧ ((( deg1 ‘𝑅)‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐)) ≤ 𝑌 ∧ ((coe1‘𝑐)‘𝑋) = ((coe1‘(((𝑌 − 𝑋)(.g‘(mulGrp‘𝑃))(var1‘𝑅))(.r‘𝑃)𝑐))‘𝑌))) → ∃𝑏 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ ((coe1‘𝑐)‘𝑋) = ((coe1‘𝑏)‘𝑌))) |
55 | 31, 43, 47, 54 | syl12anc 834 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → ∃𝑏 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ ((coe1‘𝑐)‘𝑋) = ((coe1‘𝑏)‘𝑌))) |
56 | | eqeq1 2742 |
. . . . . . . 8
⊢ (𝑎 = ((coe1‘𝑐)‘𝑋) → (𝑎 = ((coe1‘𝑏)‘𝑌) ↔ ((coe1‘𝑐)‘𝑋) = ((coe1‘𝑏)‘𝑌))) |
57 | 56 | anbi2d 629 |
. . . . . . 7
⊢ (𝑎 = ((coe1‘𝑐)‘𝑋) → (((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ 𝑎 = ((coe1‘𝑏)‘𝑌)) ↔ ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ ((coe1‘𝑐)‘𝑋) = ((coe1‘𝑏)‘𝑌)))) |
58 | 57 | rexbidv 3226 |
. . . . . 6
⊢ (𝑎 = ((coe1‘𝑐)‘𝑋) → (∃𝑏 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ 𝑎 = ((coe1‘𝑏)‘𝑌)) ↔ ∃𝑏 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ ((coe1‘𝑐)‘𝑋) = ((coe1‘𝑏)‘𝑌)))) |
59 | 55, 58 | syl5ibrcom 246 |
. . . . 5
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐼) ∧ (( deg1 ‘𝑅)‘𝑐) ≤ 𝑋) → (𝑎 = ((coe1‘𝑐)‘𝑋) → ∃𝑏 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ 𝑎 = ((coe1‘𝑏)‘𝑌)))) |
60 | 59 | expimpd 454 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐼) → (((( deg1 ‘𝑅)‘𝑐) ≤ 𝑋 ∧ 𝑎 = ((coe1‘𝑐)‘𝑋)) → ∃𝑏 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ 𝑎 = ((coe1‘𝑏)‘𝑌)))) |
61 | 60 | rexlimdva 3213 |
. . 3
⊢ (𝜑 → (∃𝑐 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑐) ≤ 𝑋 ∧ 𝑎 = ((coe1‘𝑐)‘𝑋)) → ∃𝑏 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ 𝑎 = ((coe1‘𝑏)‘𝑌)))) |
62 | 61 | ss2abdv 3997 |
. 2
⊢ (𝜑 → {𝑎 ∣ ∃𝑐 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑐) ≤ 𝑋 ∧ 𝑎 = ((coe1‘𝑐)‘𝑋))} ⊆ {𝑎 ∣ ∃𝑏 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ 𝑎 = ((coe1‘𝑏)‘𝑌))}) |
63 | | hbtlem.s |
. . . 4
⊢ 𝑆 = (ldgIdlSeq‘𝑅) |
64 | 3, 28, 63, 32 | hbtlem1 40948 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑋) = {𝑎 ∣ ∃𝑐 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑐) ≤ 𝑋 ∧ 𝑎 = ((coe1‘𝑐)‘𝑋))}) |
65 | 1, 6, 11, 64 | syl3anc 1370 |
. 2
⊢ (𝜑 → ((𝑆‘𝐼)‘𝑋) = {𝑎 ∣ ∃𝑐 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑐) ≤ 𝑋 ∧ 𝑎 = ((coe1‘𝑐)‘𝑋))}) |
66 | 3, 28, 63, 32 | hbtlem1 40948 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑌 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑌) = {𝑎 ∣ ∃𝑏 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ 𝑎 = ((coe1‘𝑏)‘𝑌))}) |
67 | 1, 6, 13, 66 | syl3anc 1370 |
. 2
⊢ (𝜑 → ((𝑆‘𝐼)‘𝑌) = {𝑎 ∣ ∃𝑏 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑏) ≤ 𝑌 ∧ 𝑎 = ((coe1‘𝑏)‘𝑌))}) |
68 | 62, 65, 67 | 3sstr4d 3968 |
1
⊢ (𝜑 → ((𝑆‘𝐼)‘𝑋) ⊆ ((𝑆‘𝐼)‘𝑌)) |