Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . . . . . . 9
⊢ ((((
deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥)) → 𝑦 = ((coe1‘𝑗)‘𝑥)) |
2 | 1 | reximi 2994 |
. . . . . . . 8
⊢
(∃𝑗 ∈
𝐼 ((( deg1
‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥)) → ∃𝑗 ∈ 𝐼 𝑦 = ((coe1‘𝑗)‘𝑥)) |
3 | 2 | ss2abi 3637 |
. . . . . . 7
⊢ {𝑦 ∣ ∃𝑗 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))} ⊆ {𝑦 ∣ ∃𝑗 ∈ 𝐼 𝑦 = ((coe1‘𝑗)‘𝑥)} |
4 | | abrexexg 7034 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑈 → {𝑦 ∣ ∃𝑗 ∈ 𝐼 𝑦 = ((coe1‘𝑗)‘𝑥)} ∈ V) |
5 | | ssexg 4732 |
. . . . . . 7
⊢ (({𝑦 ∣ ∃𝑗 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))} ⊆ {𝑦 ∣ ∃𝑗 ∈ 𝐼 𝑦 = ((coe1‘𝑗)‘𝑥)} ∧ {𝑦 ∣ ∃𝑗 ∈ 𝐼 𝑦 = ((coe1‘𝑗)‘𝑥)} ∈ V) → {𝑦 ∣ ∃𝑗 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))} ∈ V) |
6 | 3, 4, 5 | sylancr 694 |
. . . . . 6
⊢ (𝐼 ∈ 𝑈 → {𝑦 ∣ ∃𝑗 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))} ∈ V) |
7 | 6 | ralrimivw 2950 |
. . . . 5
⊢ (𝐼 ∈ 𝑈 → ∀𝑥 ∈ ℕ0 {𝑦 ∣ ∃𝑗 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))} ∈ V) |
8 | 7 | adantl 481 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → ∀𝑥 ∈ ℕ0 {𝑦 ∣ ∃𝑗 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))} ∈ V) |
9 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ ℕ0
↦ {𝑦 ∣
∃𝑗 ∈ 𝐼 ((( deg1
‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))}) = (𝑥 ∈ ℕ0 ↦ {𝑦 ∣ ∃𝑗 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))}) |
10 | 9 | fnmpt 5933 |
. . . 4
⊢
(∀𝑥 ∈
ℕ0 {𝑦
∣ ∃𝑗 ∈
𝐼 ((( deg1
‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))} ∈ V → (𝑥 ∈ ℕ0 ↦ {𝑦 ∣ ∃𝑗 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))}) Fn ℕ0) |
11 | 8, 10 | syl 17 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝑥 ∈ ℕ0 ↦ {𝑦 ∣ ∃𝑗 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))}) Fn ℕ0) |
12 | | hbtlem.s |
. . . . . . 7
⊢ 𝑆 = (ldgIdlSeq‘𝑅) |
13 | | elex 3185 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑅 ∈ V) |
14 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑅 → (Poly1‘𝑟) =
(Poly1‘𝑅)) |
15 | | hbtlem.p |
. . . . . . . . . . . . 13
⊢ 𝑃 = (Poly1‘𝑅) |
16 | 14, 15 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (Poly1‘𝑟) = 𝑃) |
17 | 16 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 →
(LIdeal‘(Poly1‘𝑟)) = (LIdeal‘𝑃)) |
18 | | hbtlem.u |
. . . . . . . . . . 11
⊢ 𝑈 = (LIdeal‘𝑃) |
19 | 17, 18 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 →
(LIdeal‘(Poly1‘𝑟)) = 𝑈) |
20 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑅 → ( deg1 ‘𝑟) = ( deg1
‘𝑅)) |
21 | 20 | fveq1d 6105 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = 𝑅 → (( deg1 ‘𝑟)‘𝑗) = (( deg1 ‘𝑅)‘𝑗)) |
22 | 21 | breq1d 4593 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = 𝑅 → ((( deg1 ‘𝑟)‘𝑗) ≤ 𝑥 ↔ (( deg1 ‘𝑅)‘𝑗) ≤ 𝑥)) |
23 | 22 | anbi1d 737 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑅 → (((( deg1 ‘𝑟)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥)) ↔ ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥)))) |
24 | 23 | rexbidv 3034 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (∃𝑗 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥)) ↔ ∃𝑗 ∈ 𝑖 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥)))) |
25 | 24 | abbidv 2728 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → {𝑦 ∣ ∃𝑗 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))} = {𝑦 ∣ ∃𝑗 ∈ 𝑖 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))}) |
26 | 25 | mpteq2dv 4673 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (𝑥 ∈ ℕ0 ↦ {𝑦 ∣ ∃𝑗 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))}) = (𝑥 ∈ ℕ0 ↦ {𝑦 ∣ ∃𝑗 ∈ 𝑖 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))})) |
27 | 19, 26 | mpteq12dv 4663 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (𝑖 ∈
(LIdeal‘(Poly1‘𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑦 ∣ ∃𝑗 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))})) = (𝑖 ∈ 𝑈 ↦ (𝑥 ∈ ℕ0 ↦ {𝑦 ∣ ∃𝑗 ∈ 𝑖 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))}))) |
28 | | df-ldgis 36711 |
. . . . . . . . 9
⊢ ldgIdlSeq
= (𝑟 ∈ V ↦
(𝑖 ∈
(LIdeal‘(Poly1‘𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑦 ∣ ∃𝑗 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))}))) |
29 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(LIdeal‘𝑃)
∈ V |
30 | 18, 29 | eqeltri 2684 |
. . . . . . . . . 10
⊢ 𝑈 ∈ V |
31 | 30 | mptex 6390 |
. . . . . . . . 9
⊢ (𝑖 ∈ 𝑈 ↦ (𝑥 ∈ ℕ0 ↦ {𝑦 ∣ ∃𝑗 ∈ 𝑖 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))})) ∈ V |
32 | 27, 28, 31 | fvmpt 6191 |
. . . . . . . 8
⊢ (𝑅 ∈ V →
(ldgIdlSeq‘𝑅) =
(𝑖 ∈ 𝑈 ↦ (𝑥 ∈ ℕ0 ↦ {𝑦 ∣ ∃𝑗 ∈ 𝑖 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))}))) |
33 | 13, 32 | syl 17 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(ldgIdlSeq‘𝑅) =
(𝑖 ∈ 𝑈 ↦ (𝑥 ∈ ℕ0 ↦ {𝑦 ∣ ∃𝑗 ∈ 𝑖 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))}))) |
34 | 12, 33 | syl5eq 2656 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑆 = (𝑖 ∈ 𝑈 ↦ (𝑥 ∈ ℕ0 ↦ {𝑦 ∣ ∃𝑗 ∈ 𝑖 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))}))) |
35 | 34 | fveq1d 6105 |
. . . . 5
⊢ (𝑅 ∈ Ring → (𝑆‘𝐼) = ((𝑖 ∈ 𝑈 ↦ (𝑥 ∈ ℕ0 ↦ {𝑦 ∣ ∃𝑗 ∈ 𝑖 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))}))‘𝐼)) |
36 | | rexeq 3116 |
. . . . . . . 8
⊢ (𝑖 = 𝐼 → (∃𝑗 ∈ 𝑖 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥)) ↔ ∃𝑗 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥)))) |
37 | 36 | abbidv 2728 |
. . . . . . 7
⊢ (𝑖 = 𝐼 → {𝑦 ∣ ∃𝑗 ∈ 𝑖 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))} = {𝑦 ∣ ∃𝑗 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))}) |
38 | 37 | mpteq2dv 4673 |
. . . . . 6
⊢ (𝑖 = 𝐼 → (𝑥 ∈ ℕ0 ↦ {𝑦 ∣ ∃𝑗 ∈ 𝑖 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))}) = (𝑥 ∈ ℕ0 ↦ {𝑦 ∣ ∃𝑗 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))})) |
39 | | eqid 2610 |
. . . . . 6
⊢ (𝑖 ∈ 𝑈 ↦ (𝑥 ∈ ℕ0 ↦ {𝑦 ∣ ∃𝑗 ∈ 𝑖 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))})) = (𝑖 ∈ 𝑈 ↦ (𝑥 ∈ ℕ0 ↦ {𝑦 ∣ ∃𝑗 ∈ 𝑖 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))})) |
40 | | nn0ex 11175 |
. . . . . . 7
⊢
ℕ0 ∈ V |
41 | 40 | mptex 6390 |
. . . . . 6
⊢ (𝑥 ∈ ℕ0
↦ {𝑦 ∣
∃𝑗 ∈ 𝐼 ((( deg1
‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))}) ∈ V |
42 | 38, 39, 41 | fvmpt 6191 |
. . . . 5
⊢ (𝐼 ∈ 𝑈 → ((𝑖 ∈ 𝑈 ↦ (𝑥 ∈ ℕ0 ↦ {𝑦 ∣ ∃𝑗 ∈ 𝑖 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))}))‘𝐼) = (𝑥 ∈ ℕ0 ↦ {𝑦 ∣ ∃𝑗 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))})) |
43 | 35, 42 | sylan9eq 2664 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝑆‘𝐼) = (𝑥 ∈ ℕ0 ↦ {𝑦 ∣ ∃𝑗 ∈ 𝐼 ((( deg1 ‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))})) |
44 | 43 | fneq1d 5895 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → ((𝑆‘𝐼) Fn ℕ0 ↔ (𝑥 ∈ ℕ0
↦ {𝑦 ∣
∃𝑗 ∈ 𝐼 ((( deg1
‘𝑅)‘𝑗) ≤ 𝑥 ∧ 𝑦 = ((coe1‘𝑗)‘𝑥))}) Fn
ℕ0)) |
45 | 11, 44 | mpbird 246 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝑆‘𝐼) Fn ℕ0) |
46 | | hbtlem7.t |
. . . . 5
⊢ 𝑇 = (LIdeal‘𝑅) |
47 | 15, 18, 12, 46 | hbtlem2 36713 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑥 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑥) ∈ 𝑇) |
48 | 47 | 3expa 1257 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ 𝑥 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑥) ∈ 𝑇) |
49 | 48 | ralrimiva 2949 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → ∀𝑥 ∈ ℕ0 ((𝑆‘𝐼)‘𝑥) ∈ 𝑇) |
50 | | ffnfv 6295 |
. 2
⊢ ((𝑆‘𝐼):ℕ0⟶𝑇 ↔ ((𝑆‘𝐼) Fn ℕ0 ∧ ∀𝑥 ∈ ℕ0
((𝑆‘𝐼)‘𝑥) ∈ 𝑇)) |
51 | 45, 49, 50 | sylanbrc 695 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝑆‘𝐼):ℕ0⟶𝑇) |