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 \in LIdeal (R) ⟼ \{j \in P \| i \subseteq j\})$
Assertion	zartopn	$⊢ R \in CRing \to (J \in TopOn (P) \land 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 \in LIdeal (R) ⟼ \{j \in P \| i \subseteq j\})$
5		ssrab2	$⊢ \{j \in P \| i \subseteq j\} \subseteq P$
6	3	fvexi	$⊢ P \in V$
7	6	elpw2	$⊢ \{j \in P \| i \subseteq j\} \in 𝒫 P \leftrightarrow \{j \in P \| i \subseteq j\} \subseteq P$
8	5 7	mpbir	$⊢ \{j \in P \| i \subseteq j\} \in 𝒫 P$
9	8	rgenw	$⊢ \forall i \in LIdeal (R) \{j \in P \| i \subseteq j\} \in 𝒫 P$
10	4	rnmptss	$⊢ \forall i \in LIdeal (R) \{j \in P \| i \subseteq j\} \in 𝒫 P \to ran V \subseteq 𝒫 P$
11	9 10	ax-mp	$⊢ ran V \subseteq 𝒫 P$
12	11	a1i	$⊢ R \in CRing \to ran V \subseteq 𝒫 P$
13		crngring	$⊢ R \in CRing \to R \in 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 \in Ring \to V (\{0_{R}\}) = P$
19	4	funmpt2	$⊢ Fun V$
20		eqid	$⊢ LIdeal (R) = LIdeal (R)$
21	20 17	lidl0	$⊢ R \in Ring \to \{0_{R}\} \in LIdeal (R)$
22	6	rabex	$⊢ \{j \in P \| i \subseteq j\} \in V$
23	22 4	dmmpti	$⊢ dom V = LIdeal (R)$
24	21 23	eleqtrrdi	$⊢ R \in Ring \to \{0_{R}\} \in dom V$
25		fvelrn	$⊢ (Fun V \land \{0_{R}\} \in dom V) \to V (\{0_{R}\}) \in ran V$
26	19 24 25	sylancr	$⊢ R \in Ring \to V (\{0_{R}\}) \in ran V$
27	18 26	eqeltrrd	$⊢ R \in Ring \to P \in ran V$
28	13 27	syl	$⊢ R \in CRing \to P \in ran V$
29	16	zarclsint	$⊢ (R \in CRing \land z \subseteq ran V \land z \neq \emptyset) \to ⋂ z \in ran V$
30	12 28 29	ismred	$⊢ R \in CRing \to ran V \in Moore (P)$
31		eqid	$⊢ {Base}_{R} = {Base}_{R}$
32	23 31	lidl1	$⊢ R \in Ring \to {Base}_{R} \in dom V$
33	13 32	syl	$⊢ R \in CRing \to {Base}_{R} \in dom V$
34	33 23	eleqtrdi	$⊢ R \in CRing \to {Base}_{R} \in LIdeal (R)$
35	16 31	zarcls1	$⊢ (R \in CRing \land {Base}_{R} \in LIdeal (R)) \to (V ({Base}_{R}) = \emptyset \leftrightarrow {Base}_{R} = {Base}_{R})$
36	31 35	mpbiri	$⊢ (R \in CRing \land {Base}_{R} \in LIdeal (R)) \to V ({Base}_{R}) = \emptyset$
37	34 36	mpdan	$⊢ R \in CRing \to V ({Base}_{R}) = \emptyset$
38	19	a1i	$⊢ R \in CRing \to Fun V$
39		fvelrn	$⊢ (Fun V \land {Base}_{R} \in dom V) \to V ({Base}_{R}) \in ran V$
40	38 33 39	syl2anc	$⊢ R \in CRing \to V ({Base}_{R}) \in ran V$
41	37 40	eqeltrrd	$⊢ R \in CRing \to \emptyset \in ran V$
42	16	zarclsun	$⊢ (R \in CRing \land x \in ran V \land y \in ran V) \to x \cup y \in ran V$
43		eqid	$⊢ \{s \in 𝒫 P \| P ∖ s \in ran V\} = \{s \in 𝒫 P \| P ∖ s \in ran V\}$
44	30 41 42 43	mretopd	$⊢ R \in CRing \to (\{s \in 𝒫 P \| P ∖ s \in ran V\} \in TopOn (P) \land ran V = Clsd (\{s \in 𝒫 P \| P ∖ s \in ran V\}))$
45	1 2 3 4	zarcls	$⊢ R \in Ring \to J = \{s \in 𝒫 P \| P ∖ s \in ran V\}$
46	13 45	syl	$⊢ R \in CRing \to J = \{s \in 𝒫 P \| P ∖ s \in ran V\}$
47	46	eleq1d	$⊢ R \in CRing \to (J \in TopOn (P) \leftrightarrow \{s \in 𝒫 P \| P ∖ s \in ran V\} \in TopOn (P))$
48	46	fveq2d	$⊢ R \in CRing \to Clsd (J) = Clsd (\{s \in 𝒫 P \| P ∖ s \in ran V\})$
49	48	eqeq2d	$⊢ R \in CRing \to (ran V = Clsd (J) \leftrightarrow ran V = Clsd (\{s \in 𝒫 P \| P ∖ s \in ran V\}))$
50	47 49	anbi12d	$⊢ R \in CRing \to ((J \in TopOn (P) \land ran V = Clsd (J)) \leftrightarrow (\{s \in 𝒫 P \| P ∖ s \in ran V\} \in TopOn (P) \land ran V = Clsd (\{s \in 𝒫 P \| P ∖ s \in ran V\})))$
51	44 50	mpbird	$⊢ R \in CRing \to (J \in TopOn (P) \land ran V = Clsd (J))$

Metamath Proof Explorer

Theorem zartopn

Proof