Step | Hyp | Ref
| Expression |
1 | | zartop.1 |
. . . 4
⊢ 𝑆 = (Spec‘𝑅) |
2 | | zartop.2 |
. . . 4
⊢ 𝐽 = (TopOpen‘𝑆) |
3 | 1, 2 | zartop 31332 |
. . 3
⊢ (𝑅 ∈ CRing → 𝐽 ∈ Top) |
4 | | zarmxt1.1 |
. . . 4
⊢ 𝑀 = (MaxIdeal‘𝑅) |
5 | 4 | fvexi 6665 |
. . 3
⊢ 𝑀 ∈ V |
6 | | zarmxt1.2 |
. . . 4
⊢ 𝑇 = (𝐽 ↾t 𝑀) |
7 | | resttop 21845 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ V) → (𝐽 ↾t 𝑀) ∈ Top) |
8 | 6, 7 | eqeltrid 2855 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ V) → 𝑇 ∈ Top) |
9 | 3, 5, 8 | sylancl 590 |
. 2
⊢ (𝑅 ∈ CRing → 𝑇 ∈ Top) |
10 | | eqid 2759 |
. . . . . . . . . . 11
⊢
(LSSum‘(mulGrp‘𝑅)) = (LSSum‘(mulGrp‘𝑅)) |
11 | 10 | mxidlprm 31146 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) → 𝑚 ∈ (PrmIdeal‘𝑅)) |
12 | 11 | ex 417 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → (𝑚 ∈ (MaxIdeal‘𝑅) → 𝑚 ∈ (PrmIdeal‘𝑅))) |
13 | 12 | ssrdv 3894 |
. . . . . . . 8
⊢ (𝑅 ∈ CRing →
(MaxIdeal‘𝑅) ⊆
(PrmIdeal‘𝑅)) |
14 | 13 | adantr 485 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ (MaxIdeal‘𝑅)
⊆ (PrmIdeal‘𝑅)) |
15 | | eqid 2759 |
. . . . . . 7
⊢
(PrmIdeal‘𝑅) =
(PrmIdeal‘𝑅) |
16 | 14, 4, 15 | 3sstr4g 3933 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ 𝑀 ⊆
(PrmIdeal‘𝑅)) |
17 | | sseq2 3914 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑙 → (𝑖 ⊆ 𝑗 ↔ 𝑖 ⊆ 𝑙)) |
18 | 17 | cbvrabv 3402 |
. . . . . . . . . . . 12
⊢ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} = {𝑙 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑙} |
19 | | sseq1 3913 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑘 → (𝑖 ⊆ 𝑙 ↔ 𝑘 ⊆ 𝑙)) |
20 | 19 | rabbidv 3390 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑘 → {𝑙 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑙} = {𝑙 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑙}) |
21 | 18, 20 | syl5eq 2806 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑘 → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} = {𝑙 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑙}) |
22 | 21 | cbvmptv 5128 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) = (𝑘 ∈ (LIdeal‘𝑅) ↦ {𝑙 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑙}) |
23 | 1, 2, 15, 22 | zartopn 31331 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → (𝐽 ∈
(TopOn‘(PrmIdeal‘𝑅)) ∧ ran (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) = (Clsd‘𝐽))) |
24 | 23 | adantr 485 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ (𝐽 ∈
(TopOn‘(PrmIdeal‘𝑅)) ∧ ran (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) = (Clsd‘𝐽))) |
25 | 24 | simpld 499 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ 𝐽 ∈
(TopOn‘(PrmIdeal‘𝑅))) |
26 | | toponuni 21599 |
. . . . . . 7
⊢ (𝐽 ∈
(TopOn‘(PrmIdeal‘𝑅)) → (PrmIdeal‘𝑅) = ∪ 𝐽) |
27 | 25, 26 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ (PrmIdeal‘𝑅) =
∪ 𝐽) |
28 | 16, 27 | sseqtrd 3928 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ 𝑀 ⊆ ∪ 𝐽) |
29 | | simpl 487 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ 𝑅 ∈
CRing) |
30 | 29 | crngringd 19363 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ 𝑅 ∈
Ring) |
31 | | simpr 489 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ 𝑚 ∈ ∪ 𝑇) |
32 | 6 | unieqi 4804 |
. . . . . . . . . . . 12
⊢ ∪ 𝑇 =
∪ (𝐽 ↾t 𝑀) |
33 | 31, 32 | eleqtrdi 2861 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ 𝑚 ∈ ∪ (𝐽
↾t 𝑀)) |
34 | 3 | adantr 485 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ 𝐽 ∈
Top) |
35 | | eqid 2759 |
. . . . . . . . . . . . 13
⊢ ∪ 𝐽 =
∪ 𝐽 |
36 | 35 | restuni 21847 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ 𝑀 ⊆ ∪ 𝐽)
→ 𝑀 = ∪ (𝐽
↾t 𝑀)) |
37 | 34, 28, 36 | syl2anc 588 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ 𝑀 = ∪ (𝐽
↾t 𝑀)) |
38 | 33, 37 | eleqtrrd 2854 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ 𝑚 ∈ 𝑀) |
39 | 38, 4 | eleqtrdi 2861 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ 𝑚 ∈
(MaxIdeal‘𝑅)) |
40 | | eqid 2759 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
41 | 40 | mxidlidl 31141 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) → 𝑚 ∈ (LIdeal‘𝑅)) |
42 | 30, 39, 41 | syl2anc 588 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ 𝑚 ∈
(LIdeal‘𝑅)) |
43 | | eqid 2759 |
. . . . . . . . . 10
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
44 | 22, 43 | zarclssn 31329 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ (LIdeal‘𝑅)) → ({𝑚} = ((𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})‘𝑚) ↔ 𝑚 ∈ (MaxIdeal‘𝑅))) |
45 | 44 | biimpar 482 |
. . . . . . . 8
⊢ (((𝑅 ∈ CRing ∧ 𝑚 ∈ (LIdeal‘𝑅)) ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) → {𝑚} = ((𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})‘𝑚)) |
46 | 29, 42, 39, 45 | syl21anc 837 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ {𝑚} = ((𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})‘𝑚)) |
47 | 22 | funmpt2 6367 |
. . . . . . . 8
⊢ Fun
(𝑖 ∈
(LIdeal‘𝑅) ↦
{𝑗 ∈
(PrmIdeal‘𝑅) ∣
𝑖 ⊆ 𝑗}) |
48 | | fvex 6664 |
. . . . . . . . . . 11
⊢
(PrmIdeal‘𝑅)
∈ V |
49 | 48 | rabex 5195 |
. . . . . . . . . 10
⊢ {𝑙 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑙} ∈ V |
50 | 49, 22 | dmmpti 6468 |
. . . . . . . . 9
⊢ dom
(𝑖 ∈
(LIdeal‘𝑅) ↦
{𝑗 ∈
(PrmIdeal‘𝑅) ∣
𝑖 ⊆ 𝑗}) = (LIdeal‘𝑅) |
51 | 42, 50 | eleqtrrdi 2862 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ 𝑚 ∈ dom (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})) |
52 | | fvelrn 6828 |
. . . . . . . 8
⊢ ((Fun
(𝑖 ∈
(LIdeal‘𝑅) ↦
{𝑗 ∈
(PrmIdeal‘𝑅) ∣
𝑖 ⊆ 𝑗}) ∧ 𝑚 ∈ dom (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})) → ((𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})‘𝑚) ∈ ran (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})) |
53 | 47, 51, 52 | sylancr 591 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ ((𝑖 ∈
(LIdeal‘𝑅) ↦
{𝑗 ∈
(PrmIdeal‘𝑅) ∣
𝑖 ⊆ 𝑗})‘𝑚) ∈ ran (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})) |
54 | 46, 53 | eqeltrd 2851 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ {𝑚} ∈ ran
(𝑖 ∈
(LIdeal‘𝑅) ↦
{𝑗 ∈
(PrmIdeal‘𝑅) ∣
𝑖 ⊆ 𝑗})) |
55 | 24 | simprd 500 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ ran (𝑖 ∈
(LIdeal‘𝑅) ↦
{𝑗 ∈
(PrmIdeal‘𝑅) ∣
𝑖 ⊆ 𝑗}) = (Clsd‘𝐽)) |
56 | 54, 55 | eleqtrd 2853 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ {𝑚} ∈
(Clsd‘𝐽)) |
57 | 38 | snssd 4692 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ {𝑚} ⊆ 𝑀) |
58 | 35 | restcldi 21858 |
. . . . 5
⊢ ((𝑀 ⊆ ∪ 𝐽
∧ {𝑚} ∈
(Clsd‘𝐽) ∧ {𝑚} ⊆ 𝑀) → {𝑚} ∈ (Clsd‘(𝐽 ↾t 𝑀))) |
59 | 28, 56, 57, 58 | syl3anc 1369 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ {𝑚} ∈
(Clsd‘(𝐽
↾t 𝑀))) |
60 | 6 | fveq2i 6654 |
. . . 4
⊢
(Clsd‘𝑇) =
(Clsd‘(𝐽
↾t 𝑀)) |
61 | 59, 60 | eleqtrrdi 2862 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ ∪ 𝑇)
→ {𝑚} ∈
(Clsd‘𝑇)) |
62 | 61 | ralrimiva 3111 |
. 2
⊢ (𝑅 ∈ CRing →
∀𝑚 ∈ ∪ 𝑇{𝑚} ∈ (Clsd‘𝑇)) |
63 | | eqid 2759 |
. . 3
⊢ ∪ 𝑇 =
∪ 𝑇 |
64 | 63 | ist1 22006 |
. 2
⊢ (𝑇 ∈ Fre ↔ (𝑇 ∈ Top ∧ ∀𝑚 ∈ ∪ 𝑇{𝑚} ∈ (Clsd‘𝑇))) |
65 | 9, 62, 64 | sylanbrc 587 |
1
⊢ (𝑅 ∈ CRing → 𝑇 ∈ Fre) |