![]() |
Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > zartopn | Structured version Visualization version GIF version |
Description: The Zariski topology is a topology, and its closed sets are images by 𝑉 of the ideals of 𝑅. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
Ref | Expression |
---|---|
zartop.1 | ⊢ 𝑆 = (Spec‘𝑅) |
zartop.2 | ⊢ 𝐽 = (TopOpen‘𝑆) |
zarcls.1 | ⊢ 𝑃 = (PrmIdeal‘𝑅) |
zarcls.2 | ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗}) |
Ref | Expression |
---|---|
zartopn | ⊢ (𝑅 ∈ CRing → (𝐽 ∈ (TopOn‘𝑃) ∧ ran 𝑉 = (Clsd‘𝐽))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssrab2 3980 | . . . . . . . 8 ⊢ {𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗} ⊆ 𝑃 | |
2 | zarcls.1 | . . . . . . . . . 10 ⊢ 𝑃 = (PrmIdeal‘𝑅) | |
3 | 2 | fvexi 6665 | . . . . . . . . 9 ⊢ 𝑃 ∈ V |
4 | 3 | elpw2 5208 | . . . . . . . 8 ⊢ ({𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗} ∈ 𝒫 𝑃 ↔ {𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗} ⊆ 𝑃) |
5 | 1, 4 | mpbir 234 | . . . . . . 7 ⊢ {𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗} ∈ 𝒫 𝑃 |
6 | 5 | rgenw 3080 | . . . . . 6 ⊢ ∀𝑖 ∈ (LIdeal‘𝑅){𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗} ∈ 𝒫 𝑃 |
7 | zarcls.2 | . . . . . . 7 ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗}) | |
8 | 7 | rnmptss 6870 | . . . . . 6 ⊢ (∀𝑖 ∈ (LIdeal‘𝑅){𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗} ∈ 𝒫 𝑃 → ran 𝑉 ⊆ 𝒫 𝑃) |
9 | 6, 8 | ax-mp 5 | . . . . 5 ⊢ ran 𝑉 ⊆ 𝒫 𝑃 |
10 | 9 | a1i 11 | . . . 4 ⊢ (𝑅 ∈ CRing → ran 𝑉 ⊆ 𝒫 𝑃) |
11 | crngring 19362 | . . . . 5 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) | |
12 | 2 | rabeqi 3392 | . . . . . . . . 9 ⊢ {𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗} = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} |
13 | 12 | mpteq2i 5117 | . . . . . . . 8 ⊢ (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗}) = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) |
14 | 7, 13 | eqtri 2782 | . . . . . . 7 ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) |
15 | eqid 2759 | . . . . . . 7 ⊢ (0g‘𝑅) = (0g‘𝑅) | |
16 | 14, 2, 15 | zarcls0 31324 | . . . . . 6 ⊢ (𝑅 ∈ Ring → (𝑉‘{(0g‘𝑅)}) = 𝑃) |
17 | 7 | funmpt2 6367 | . . . . . . 7 ⊢ Fun 𝑉 |
18 | eqid 2759 | . . . . . . . . 9 ⊢ (LIdeal‘𝑅) = (LIdeal‘𝑅) | |
19 | 18, 15 | lidl0 20045 | . . . . . . . 8 ⊢ (𝑅 ∈ Ring → {(0g‘𝑅)} ∈ (LIdeal‘𝑅)) |
20 | 3 | rabex 5195 | . . . . . . . . 9 ⊢ {𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗} ∈ V |
21 | 20, 7 | dmmpti 6468 | . . . . . . . 8 ⊢ dom 𝑉 = (LIdeal‘𝑅) |
22 | 19, 21 | eleqtrrdi 2862 | . . . . . . 7 ⊢ (𝑅 ∈ Ring → {(0g‘𝑅)} ∈ dom 𝑉) |
23 | fvelrn 6828 | . . . . . . 7 ⊢ ((Fun 𝑉 ∧ {(0g‘𝑅)} ∈ dom 𝑉) → (𝑉‘{(0g‘𝑅)}) ∈ ran 𝑉) | |
24 | 17, 22, 23 | sylancr 591 | . . . . . 6 ⊢ (𝑅 ∈ Ring → (𝑉‘{(0g‘𝑅)}) ∈ ran 𝑉) |
25 | 16, 24 | eqeltrrd 2852 | . . . . 5 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ ran 𝑉) |
26 | 11, 25 | syl 17 | . . . 4 ⊢ (𝑅 ∈ CRing → 𝑃 ∈ ran 𝑉) |
27 | 14 | zarclsint 31328 | . . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝑧 ⊆ ran 𝑉 ∧ 𝑧 ≠ ∅) → ∩ 𝑧 ∈ ran 𝑉) |
28 | 10, 26, 27 | ismred 16916 | . . 3 ⊢ (𝑅 ∈ CRing → ran 𝑉 ∈ (Moore‘𝑃)) |
29 | eqid 2759 | . . . . . . . 8 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
30 | 21, 29 | lidl1 20046 | . . . . . . 7 ⊢ (𝑅 ∈ Ring → (Base‘𝑅) ∈ dom 𝑉) |
31 | 11, 30 | syl 17 | . . . . . 6 ⊢ (𝑅 ∈ CRing → (Base‘𝑅) ∈ dom 𝑉) |
32 | 31, 21 | eleqtrdi 2861 | . . . . 5 ⊢ (𝑅 ∈ CRing → (Base‘𝑅) ∈ (LIdeal‘𝑅)) |
33 | 14, 29 | zarcls1 31325 | . . . . . 6 ⊢ ((𝑅 ∈ CRing ∧ (Base‘𝑅) ∈ (LIdeal‘𝑅)) → ((𝑉‘(Base‘𝑅)) = ∅ ↔ (Base‘𝑅) = (Base‘𝑅))) |
34 | 29, 33 | mpbiri 261 | . . . . 5 ⊢ ((𝑅 ∈ CRing ∧ (Base‘𝑅) ∈ (LIdeal‘𝑅)) → (𝑉‘(Base‘𝑅)) = ∅) |
35 | 32, 34 | mpdan 687 | . . . 4 ⊢ (𝑅 ∈ CRing → (𝑉‘(Base‘𝑅)) = ∅) |
36 | 17 | a1i 11 | . . . . 5 ⊢ (𝑅 ∈ CRing → Fun 𝑉) |
37 | fvelrn 6828 | . . . . 5 ⊢ ((Fun 𝑉 ∧ (Base‘𝑅) ∈ dom 𝑉) → (𝑉‘(Base‘𝑅)) ∈ ran 𝑉) | |
38 | 36, 31, 37 | syl2anc 588 | . . . 4 ⊢ (𝑅 ∈ CRing → (𝑉‘(Base‘𝑅)) ∈ ran 𝑉) |
39 | 35, 38 | eqeltrrd 2852 | . . 3 ⊢ (𝑅 ∈ CRing → ∅ ∈ ran 𝑉) |
40 | 14 | zarclsun 31326 | . . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝑥 ∈ ran 𝑉 ∧ 𝑦 ∈ ran 𝑉) → (𝑥 ∪ 𝑦) ∈ ran 𝑉) |
41 | eqid 2759 | . . 3 ⊢ {𝑠 ∈ 𝒫 𝑃 ∣ (𝑃 ∖ 𝑠) ∈ ran 𝑉} = {𝑠 ∈ 𝒫 𝑃 ∣ (𝑃 ∖ 𝑠) ∈ ran 𝑉} | |
42 | 28, 39, 40, 41 | mretopd 21777 | . 2 ⊢ (𝑅 ∈ CRing → ({𝑠 ∈ 𝒫 𝑃 ∣ (𝑃 ∖ 𝑠) ∈ ran 𝑉} ∈ (TopOn‘𝑃) ∧ ran 𝑉 = (Clsd‘{𝑠 ∈ 𝒫 𝑃 ∣ (𝑃 ∖ 𝑠) ∈ ran 𝑉}))) |
43 | zartop.1 | . . . . . 6 ⊢ 𝑆 = (Spec‘𝑅) | |
44 | zartop.2 | . . . . . 6 ⊢ 𝐽 = (TopOpen‘𝑆) | |
45 | 43, 44, 2, 7 | zarcls 31330 | . . . . 5 ⊢ (𝑅 ∈ Ring → 𝐽 = {𝑠 ∈ 𝒫 𝑃 ∣ (𝑃 ∖ 𝑠) ∈ ran 𝑉}) |
46 | 11, 45 | syl 17 | . . . 4 ⊢ (𝑅 ∈ CRing → 𝐽 = {𝑠 ∈ 𝒫 𝑃 ∣ (𝑃 ∖ 𝑠) ∈ ran 𝑉}) |
47 | 46 | eleq1d 2835 | . . 3 ⊢ (𝑅 ∈ CRing → (𝐽 ∈ (TopOn‘𝑃) ↔ {𝑠 ∈ 𝒫 𝑃 ∣ (𝑃 ∖ 𝑠) ∈ ran 𝑉} ∈ (TopOn‘𝑃))) |
48 | 46 | fveq2d 6655 | . . . 4 ⊢ (𝑅 ∈ CRing → (Clsd‘𝐽) = (Clsd‘{𝑠 ∈ 𝒫 𝑃 ∣ (𝑃 ∖ 𝑠) ∈ ran 𝑉})) |
49 | 48 | eqeq2d 2770 | . . 3 ⊢ (𝑅 ∈ CRing → (ran 𝑉 = (Clsd‘𝐽) ↔ ran 𝑉 = (Clsd‘{𝑠 ∈ 𝒫 𝑃 ∣ (𝑃 ∖ 𝑠) ∈ ran 𝑉}))) |
50 | 47, 49 | anbi12d 634 | . 2 ⊢ (𝑅 ∈ CRing → ((𝐽 ∈ (TopOn‘𝑃) ∧ ran 𝑉 = (Clsd‘𝐽)) ↔ ({𝑠 ∈ 𝒫 𝑃 ∣ (𝑃 ∖ 𝑠) ∈ ran 𝑉} ∈ (TopOn‘𝑃) ∧ ran 𝑉 = (Clsd‘{𝑠 ∈ 𝒫 𝑃 ∣ (𝑃 ∖ 𝑠) ∈ ran 𝑉})))) |
51 | 42, 50 | mpbird 260 | 1 ⊢ (𝑅 ∈ CRing → (𝐽 ∈ (TopOn‘𝑃) ∧ ran 𝑉 = (Clsd‘𝐽))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 400 = wceq 1539 ∈ wcel 2112 ∀wral 3068 {crab 3072 ∖ cdif 3851 ⊆ wss 3854 ∅c0 4221 𝒫 cpw 4487 {csn 4515 ↦ cmpt 5105 dom cdm 5517 ran crn 5518 Fun wfun 6322 ‘cfv 6328 Basecbs 16526 TopOpenctopn 16738 0gc0g 16756 Ringcrg 19350 CRingccrg 19351 LIdealclidl 19995 TopOnctopon 21595 Clsdccld 21701 PrmIdealcprmidl 31116 Speccrspec 31318 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-rep 5149 ax-sep 5162 ax-nul 5169 ax-pow 5227 ax-pr 5291 ax-un 7452 ax-ac2 9908 ax-cnex 10616 ax-resscn 10617 ax-1cn 10618 ax-icn 10619 ax-addcl 10620 ax-addrcl 10621 ax-mulcl 10622 ax-mulrcl 10623 ax-mulcom 10624 ax-addass 10625 ax-mulass 10626 ax-distr 10627 ax-i2m1 10628 ax-1ne0 10629 ax-1rid 10630 ax-rnegex 10631 ax-rrecex 10632 ax-cnre 10633 ax-pre-lttri 10634 ax-pre-lttrn 10635 ax-pre-ltadd 10636 ax-pre-mulgt0 10637 |
This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2899 df-ne 2950 df-nel 3054 df-ral 3073 df-rex 3074 df-reu 3075 df-rmo 3076 df-rab 3077 df-v 3409 df-sbc 3694 df-csb 3802 df-dif 3857 df-un 3859 df-in 3861 df-ss 3871 df-pss 3873 df-nul 4222 df-if 4414 df-pw 4489 df-sn 4516 df-pr 4518 df-tp 4520 df-op 4522 df-uni 4792 df-int 4832 df-iun 4878 df-iin 4879 df-br 5026 df-opab 5088 df-mpt 5106 df-tr 5132 df-id 5423 df-eprel 5428 df-po 5436 df-so 5437 df-fr 5476 df-se 5477 df-we 5478 df-xp 5523 df-rel 5524 df-cnv 5525 df-co 5526 df-dm 5527 df-rn 5528 df-res 5529 df-ima 5530 df-pred 6119 df-ord 6165 df-on 6166 df-lim 6167 df-suc 6168 df-iota 6287 df-fun 6330 df-fn 6331 df-f 6332 df-f1 6333 df-fo 6334 df-f1o 6335 df-fv 6336 df-isom 6337 df-riota 7101 df-ov 7146 df-oprab 7147 df-mpo 7148 df-rpss 7440 df-om 7573 df-1st 7686 df-2nd 7687 df-wrecs 7950 df-recs 8011 df-rdg 8049 df-1o 8105 df-oadd 8109 df-er 8292 df-en 8521 df-dom 8522 df-sdom 8523 df-fin 8524 df-dju 9348 df-card 9386 df-ac 9561 df-pnf 10700 df-mnf 10701 df-xr 10702 df-ltxr 10703 df-le 10704 df-sub 10895 df-neg 10896 df-nn 11660 df-2 11722 df-3 11723 df-4 11724 df-5 11725 df-6 11726 df-7 11727 df-8 11728 df-9 11729 df-n0 11920 df-z 12006 df-dec 12123 df-uz 12268 df-fz 12925 df-struct 16528 df-ndx 16529 df-slot 16530 df-base 16532 df-sets 16533 df-ress 16534 df-plusg 16621 df-mulr 16622 df-sca 16624 df-vsca 16625 df-ip 16626 df-tset 16627 df-ple 16628 df-rest 16739 df-topn 16740 df-0g 16758 df-mre 16900 df-mgm 17903 df-sgrp 17952 df-mnd 17963 df-submnd 18008 df-grp 18157 df-minusg 18158 df-sbg 18159 df-subg 18328 df-cntz 18499 df-lsm 18813 df-cmn 18960 df-abl 18961 df-mgp 19293 df-ur 19305 df-ring 19352 df-cring 19353 df-subrg 19586 df-lmod 19689 df-lss 19757 df-lsp 19797 df-sra 19997 df-rgmod 19998 df-lidl 19999 df-rsp 20000 df-lpidl 20069 df-top 21579 df-topon 21596 df-cld 21704 df-prmidl 31117 df-mxidl 31138 df-idlsrg 31152 df-rspec 31319 |
This theorem is referenced by: zartop 31332 zartopon 31333 zart0 31335 zarmxt1 31336 zarcmplem 31337 rhmpreimacn 31341 |
Copyright terms: Public domain | W3C validator |