Metamath Proof Explorer

Theorem zartopn

Description: The Zariski topology is a topology, and its closed sets are images by V of the ideals of R . (Contributed by Thierry Arnoux, 16-Jun-2024)

Ref Expression
Hypotheses zartop.1 No typesetting found for |- S = ( Spec ` R ) with typecode |-
zartop.2 ⊢ J = TopOpen ⁡ S
zarcls.1 No typesetting found for |- P = ( PrmIdeal ` R ) with typecode |-
zarcls.2 ⊢ V = i ∈ LIdeal ⁡ R ⟼ j ∈ P | i ⊆ j
Assertion zartopn ⊢ R ∈ CRing → J ∈ TopOn ⁡ P ∧ ran ⁡ V = Clsd ⁡ J

Proof

Step Hyp Ref Expression
1 zartop.1 Could not format S = ( Spec ` R ) : No typesetting found for |- S = ( Spec ` R ) with typecode |-
2 zartop.2 ⊢ J = TopOpen ⁡ S
3 zarcls.1 Could not format P = ( PrmIdeal ` R ) : No typesetting found for |- P = ( PrmIdeal ` R ) with typecode |-
4 zarcls.2 ⊢ V = i ∈ LIdeal ⁡ R ⟼ j ∈ P | i ⊆ j
5 ssrab2 ⊢ j ∈ P | i ⊆ j ⊆ P
6 3 fvexi ⊢ P ∈ V
7 6 elpw2 ⊢ j ∈ P | i ⊆ j ∈ 𝒫 P ↔ j ∈ P | i ⊆ j ⊆ P
8 5 7 mpbir ⊢ j ∈ P | i ⊆ j ∈ 𝒫 P
9 8 rgenw ⊢ ∀ i ∈ LIdeal ⁡ R j ∈ P | i ⊆ j ∈ 𝒫 P
10 4 rnmptss ⊢ ∀ i ∈ LIdeal ⁡ R j ∈ P | i ⊆ j ∈ 𝒫 P → ran ⁡ V ⊆ 𝒫 P
11 9 10 ax-mp ⊢ ran ⁡ V ⊆ 𝒫 P
12 11 a1i ⊢ R ∈ CRing → ran ⁡ V ⊆ 𝒫 P
13 crngring ⊢ R ∈ CRing → R ∈ Ring
14 3 rabeqi Could not format { j e. P | i C_ j } = { j e. ( PrmIdeal ` R ) | i C_ j } : No typesetting found for |- { j e. P | i C_ j } = { j e. ( PrmIdeal ` R ) | i C_ j } with typecode |-
15 14 mpteq2i Could not format ( i e. ( LIdeal ` R ) |-> { j e. P | i C_ j } ) = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) : No typesetting found for |- ( i e. ( LIdeal ` R ) |-> { j e. P | i C_ j } ) = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) with typecode |-
16 4 15 eqtri Could not format V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) : No typesetting found for |- V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) with typecode |-
17 eqid ⊢ 0 R = 0 R
18 16 3 17 zarcls0 ⊢ R ∈ Ring → V ⁡ 0 R = P
19 4 funmpt2 ⊢ Fun ⁡ V
20 eqid ⊢ LIdeal ⁡ R = LIdeal ⁡ R
21 20 17 lidl0 ⊢ R ∈ Ring → 0 R ∈ LIdeal ⁡ R
22 6 rabex ⊢ j ∈ P | i ⊆ j ∈ V
23 22 4 dmmpti ⊢ dom ⁡ V = LIdeal ⁡ R
24 21 23 eleqtrrdi ⊢ R ∈ Ring → 0 R ∈ dom ⁡ V
25 fvelrn ⊢ Fun ⁡ V ∧ 0 R ∈ dom ⁡ V → V ⁡ 0 R ∈ ran ⁡ V
26 19 24 25 sylancr ⊢ R ∈ Ring → V ⁡ 0 R ∈ ran ⁡ V
27 18 26 eqeltrrd ⊢ R ∈ Ring → P ∈ ran ⁡ V
28 13 27 syl ⊢ R ∈ CRing → P ∈ ran ⁡ V
29 16 zarclsint ⊢ R ∈ CRing ∧ z ⊆ ran ⁡ V ∧ z ≠ ∅ → ⋂ z ∈ ran ⁡ V
30 12 28 29 ismred ⊢ R ∈ CRing → ran ⁡ V ∈ Moore ⁡ P
31 eqid ⊢ Base R = Base R
32 23 31 lidl1 ⊢ R ∈ Ring → Base R ∈ dom ⁡ V
33 13 32 syl ⊢ R ∈ CRing → Base R ∈ dom ⁡ V
34 33 23 eleqtrdi ⊢ R ∈ CRing → Base R ∈ LIdeal ⁡ R
35 16 31 zarcls1 ⊢ R ∈ CRing ∧ Base R ∈ LIdeal ⁡ R → V ⁡ Base R = ∅ ↔ Base R = Base R
36 31 35 mpbiri ⊢ R ∈ CRing ∧ Base R ∈ LIdeal ⁡ R → V ⁡ Base R = ∅
37 34 36 mpdan ⊢ R ∈ CRing → V ⁡ Base R = ∅
38 19 a1i ⊢ R ∈ CRing → Fun ⁡ V
39 fvelrn ⊢ Fun ⁡ V ∧ Base R ∈ dom ⁡ V → V ⁡ Base R ∈ ran ⁡ V
40 38 33 39 syl2anc ⊢ R ∈ CRing → V ⁡ Base R ∈ ran ⁡ V
41 37 40 eqeltrrd ⊢ R ∈ CRing → ∅ ∈ ran ⁡ V
42 16 zarclsun ⊢ R ∈ CRing ∧ x ∈ ran ⁡ V ∧ y ∈ ran ⁡ V → x ∪ y ∈ ran ⁡ V
43 eqid ⊢ s ∈ 𝒫 P | P ∖ s ∈ ran ⁡ V = s ∈ 𝒫 P | P ∖ s ∈ ran ⁡ V
44 30 41 42 43 mretopd ⊢ R ∈ CRing → s ∈ 𝒫 P | P ∖ s ∈ ran ⁡ V ∈ TopOn ⁡ P ∧ ran ⁡ V = Clsd ⁡ s ∈ 𝒫 P | P ∖ s ∈ ran ⁡ V
45 1 2 3 4 zarcls ⊢ R ∈ Ring → J = s ∈ 𝒫 P | P ∖ s ∈ ran ⁡ V
46 13 45 syl ⊢ R ∈ CRing → J = s ∈ 𝒫 P | P ∖ s ∈ ran ⁡ V
47 46 eleq1d ⊢ R ∈ CRing → J ∈ TopOn ⁡ P ↔ s ∈ 𝒫 P | P ∖ s ∈ ran ⁡ V ∈ TopOn ⁡ P
48 46 fveq2d ⊢ R ∈ CRing → Clsd ⁡ J = Clsd ⁡ s ∈ 𝒫 P | P ∖ s ∈ ran ⁡ V
49 48 eqeq2d ⊢ R ∈ CRing → ran ⁡ V = Clsd ⁡ J ↔ ran ⁡ V = Clsd ⁡ s ∈ 𝒫 P | P ∖ s ∈ ran ⁡ V
50 47 49 anbi12d ⊢ R ∈ CRing → J ∈ TopOn ⁡ P ∧ ran ⁡ V = Clsd ⁡ J ↔ s ∈ 𝒫 P | P ∖ s ∈ ran ⁡ V ∈ TopOn ⁡ P ∧ ran ⁡ V = Clsd ⁡ s ∈ 𝒫 P | P ∖ s ∈ ran ⁡ V
51 44 50 mpbird ⊢ R ∈ CRing → J ∈ TopOn ⁡ P ∧ ran ⁡ V = Clsd ⁡ J