zart0

Description: The Zariski topology is T_0 . Corollary 1.1.8 of EGA p. 81. (Contributed by Thierry Arnoux, 16-Jun-2024)

	Ref	Expression
Hypotheses	zartop.1	$⊢ S = Spec (R)$
	zartop.2	$⊢ J = TopOpen (S)$
Assertion	zart0	$⊢ R \in CRing \to J \in Kol2$

Proof

Step	Hyp	Ref	Expression
1		zartop.1	$⊢ S = Spec (R)$
2		zartop.2	$⊢ J = TopOpen (S)$
3	1 2	zartop	$⊢ R \in CRing \to J \in Top$
4		sseq2	$⊢ j = x \to (x \subseteq j \leftrightarrow x \subseteq x)$
5		simpr	$⊢ (R \in CRing \land x \in PrmIdeal (R)) \to x \in PrmIdeal (R)$
6		ssidd	$⊢ (R \in CRing \land x \in PrmIdeal (R)) \to x \subseteq x$
7	4 5 6	elrabd	$⊢ (R \in CRing \land x \in PrmIdeal (R)) \to x \in \{j \in PrmIdeal (R) \| x \subseteq j\}$
8	7	ad2antrr	$⊢ (((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \land \forall d \in ran (k \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| k \subseteq j\}) (x \in d \leftrightarrow y \in d)) \to x \in \{j \in PrmIdeal (R) \| x \subseteq j\}$
9		sseq1	$⊢ k = i \to (k \subseteq j \leftrightarrow i \subseteq j)$
10	9	rabbidv	$⊢ k = i \to \{j \in PrmIdeal (R) \| k \subseteq j\} = \{j \in PrmIdeal (R) \| i \subseteq j\}$
11	10	cbvmptv	$⊢ (k \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| k \subseteq j\}) = (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| i \subseteq j\})$
12		crngring	$⊢ R \in CRing \to R \in Ring$
13	12	ad2antrr	$⊢ ((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \to R \in Ring$
14		simplr	$⊢ ((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \to x \in PrmIdeal (R)$
15		prmidlidl	$⊢ (R \in Ring \land x \in PrmIdeal (R)) \to x \in LIdeal (R)$
16	13 14 15	syl2anc	$⊢ ((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \to x \in LIdeal (R)$
17		fvex	$⊢ PrmIdeal (R) \in V$
18	17	rabex	$⊢ \{j \in PrmIdeal (R) \| x \subseteq j\} \in V$
19	18	a1i	$⊢ ((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \to \{j \in PrmIdeal (R) \| x \subseteq j\} \in V$
20		sseq1	$⊢ i = x \to (i \subseteq j \leftrightarrow x \subseteq j)$
21	20	rabbidv	$⊢ i = x \to \{j \in PrmIdeal (R) \| i \subseteq j\} = \{j \in PrmIdeal (R) \| x \subseteq j\}$
22	21	eqcomd	$⊢ i = x \to \{j \in PrmIdeal (R) \| x \subseteq j\} = \{j \in PrmIdeal (R) \| i \subseteq j\}$
23	22	adantl	$⊢ (((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \land i = x) \to \{j \in PrmIdeal (R) \| x \subseteq j\} = \{j \in PrmIdeal (R) \| i \subseteq j\}$
24	11 16 19 23	elrnmptdv	$⊢ ((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \to \{j \in PrmIdeal (R) \| x \subseteq j\} \in ran (k \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| k \subseteq j\})$
25		simpr	$⊢ (((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \land d = \{j \in PrmIdeal (R) \| x \subseteq j\}) \to d = \{j \in PrmIdeal (R) \| x \subseteq j\}$
26	25	eleq2d	$⊢ (((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \land d = \{j \in PrmIdeal (R) \| x \subseteq j\}) \to (x \in d \leftrightarrow x \in \{j \in PrmIdeal (R) \| x \subseteq j\})$
27	25	eleq2d	$⊢ (((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \land d = \{j \in PrmIdeal (R) \| x \subseteq j\}) \to (y \in d \leftrightarrow y \in \{j \in PrmIdeal (R) \| x \subseteq j\})$
28	26 27	bibi12d	$⊢ (((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \land d = \{j \in PrmIdeal (R) \| x \subseteq j\}) \to ((x \in d \leftrightarrow y \in d) \leftrightarrow (x \in \{j \in PrmIdeal (R) \| x \subseteq j\} \leftrightarrow y \in \{j \in PrmIdeal (R) \| x \subseteq j\}))$
29	24 28	rspcdv	$⊢ ((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \to (\forall d \in ran (k \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| k \subseteq j\}) (x \in d \leftrightarrow y \in d) \to (x \in \{j \in PrmIdeal (R) \| x \subseteq j\} \leftrightarrow y \in \{j \in PrmIdeal (R) \| x \subseteq j\}))$
30	29	imp	$⊢ (((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \land \forall d \in ran (k \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| k \subseteq j\}) (x \in d \leftrightarrow y \in d)) \to (x \in \{j \in PrmIdeal (R) \| x \subseteq j\} \leftrightarrow y \in \{j \in PrmIdeal (R) \| x \subseteq j\})$
31	8 30	mpbid	$⊢ (((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \land \forall d \in ran (k \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| k \subseteq j\}) (x \in d \leftrightarrow y \in d)) \to y \in \{j \in PrmIdeal (R) \| x \subseteq j\}$
32		sseq2	$⊢ j = y \to (x \subseteq j \leftrightarrow x \subseteq y)$
33	32	elrab	$⊢ y \in \{j \in PrmIdeal (R) \| x \subseteq j\} \leftrightarrow (y \in PrmIdeal (R) \land x \subseteq y)$
34	33	simprbi	$⊢ y \in \{j \in PrmIdeal (R) \| x \subseteq j\} \to x \subseteq y$
35	31 34	syl	$⊢ (((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \land \forall d \in ran (k \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| k \subseteq j\}) (x \in d \leftrightarrow y \in d)) \to x \subseteq y$
36		sseq2	$⊢ j = y \to (y \subseteq j \leftrightarrow y \subseteq y)$
37		simpr	$⊢ (R \in CRing \land y \in PrmIdeal (R)) \to y \in PrmIdeal (R)$
38		ssidd	$⊢ (R \in CRing \land y \in PrmIdeal (R)) \to y \subseteq y$
39	36 37 38	elrabd	$⊢ (R \in CRing \land y \in PrmIdeal (R)) \to y \in \{j \in PrmIdeal (R) \| y \subseteq j\}$
40	39	ad4ant13	$⊢ (((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \land \forall d \in ran (k \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| k \subseteq j\}) (x \in d \leftrightarrow y \in d)) \to y \in \{j \in PrmIdeal (R) \| y \subseteq j\}$
41		simpr	$⊢ ((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \to y \in PrmIdeal (R)$
42		prmidlidl	$⊢ (R \in Ring \land y \in PrmIdeal (R)) \to y \in LIdeal (R)$
43	13 41 42	syl2anc	$⊢ ((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \to y \in LIdeal (R)$
44	17	rabex	$⊢ \{j \in PrmIdeal (R) \| y \subseteq j\} \in V$
45	44	a1i	$⊢ ((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \to \{j \in PrmIdeal (R) \| y \subseteq j\} \in V$
46		sseq1	$⊢ i = y \to (i \subseteq j \leftrightarrow y \subseteq j)$
47	46	rabbidv	$⊢ i = y \to \{j \in PrmIdeal (R) \| i \subseteq j\} = \{j \in PrmIdeal (R) \| y \subseteq j\}$
48	47	eqcomd	$⊢ i = y \to \{j \in PrmIdeal (R) \| y \subseteq j\} = \{j \in PrmIdeal (R) \| i \subseteq j\}$
49	48	adantl	$⊢ (((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \land i = y) \to \{j \in PrmIdeal (R) \| y \subseteq j\} = \{j \in PrmIdeal (R) \| i \subseteq j\}$
50	11 43 45 49	elrnmptdv	$⊢ ((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \to \{j \in PrmIdeal (R) \| y \subseteq j\} \in ran (k \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| k \subseteq j\})$
51		simpr	$⊢ (((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \land d = \{j \in PrmIdeal (R) \| y \subseteq j\}) \to d = \{j \in PrmIdeal (R) \| y \subseteq j\}$
52	51	eleq2d	$⊢ (((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \land d = \{j \in PrmIdeal (R) \| y \subseteq j\}) \to (x \in d \leftrightarrow x \in \{j \in PrmIdeal (R) \| y \subseteq j\})$
53	51	eleq2d	$⊢ (((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \land d = \{j \in PrmIdeal (R) \| y \subseteq j\}) \to (y \in d \leftrightarrow y \in \{j \in PrmIdeal (R) \| y \subseteq j\})$
54	52 53	bibi12d	$⊢ (((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \land d = \{j \in PrmIdeal (R) \| y \subseteq j\}) \to ((x \in d \leftrightarrow y \in d) \leftrightarrow (x \in \{j \in PrmIdeal (R) \| y \subseteq j\} \leftrightarrow y \in \{j \in PrmIdeal (R) \| y \subseteq j\}))$
55	50 54	rspcdv	$⊢ ((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \to (\forall d \in ran (k \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| k \subseteq j\}) (x \in d \leftrightarrow y \in d) \to (x \in \{j \in PrmIdeal (R) \| y \subseteq j\} \leftrightarrow y \in \{j \in PrmIdeal (R) \| y \subseteq j\}))$
56	55	imp	$⊢ (((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \land \forall d \in ran (k \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| k \subseteq j\}) (x \in d \leftrightarrow y \in d)) \to (x \in \{j \in PrmIdeal (R) \| y \subseteq j\} \leftrightarrow y \in \{j \in PrmIdeal (R) \| y \subseteq j\})$
57	40 56	mpbird	$⊢ (((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \land \forall d \in ran (k \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| k \subseteq j\}) (x \in d \leftrightarrow y \in d)) \to x \in \{j \in PrmIdeal (R) \| y \subseteq j\}$
58		sseq2	$⊢ j = x \to (y \subseteq j \leftrightarrow y \subseteq x)$
59	58	elrab	$⊢ x \in \{j \in PrmIdeal (R) \| y \subseteq j\} \leftrightarrow (x \in PrmIdeal (R) \land y \subseteq x)$
60	59	simprbi	$⊢ x \in \{j \in PrmIdeal (R) \| y \subseteq j\} \to y \subseteq x$
61	57 60	syl	$⊢ (((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \land \forall d \in ran (k \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| k \subseteq j\}) (x \in d \leftrightarrow y \in d)) \to y \subseteq x$
62	35 61	eqssd	$⊢ (((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \land \forall d \in ran (k \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| k \subseteq j\}) (x \in d \leftrightarrow y \in d)) \to x = y$
63	62	ex	$⊢ ((R \in CRing \land x \in PrmIdeal (R)) \land y \in PrmIdeal (R)) \to (\forall d \in ran (k \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| k \subseteq j\}) (x \in d \leftrightarrow y \in d) \to x = y)$
64	63	anasss	$⊢ (R \in CRing \land (x \in PrmIdeal (R) \land y \in PrmIdeal (R))) \to (\forall d \in ran (k \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| k \subseteq j\}) (x \in d \leftrightarrow y \in d) \to x = y)$
65	64	ralrimivva	$⊢ R \in CRing \to \forall x \in PrmIdeal (R) \forall y \in PrmIdeal (R) (\forall d \in ran (k \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| k \subseteq j\}) (x \in d \leftrightarrow y \in d) \to x = y)$
66	3 65	jca	$⊢ R \in CRing \to (J \in Top \land \forall x \in PrmIdeal (R) \forall y \in PrmIdeal (R) (\forall d \in ran (k \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| k \subseteq j\}) (x \in d \leftrightarrow y \in d) \to x = y))$
67		eqid	$⊢ PrmIdeal (R) = PrmIdeal (R)$
68	1 2 67	zartopon	$⊢ R \in CRing \to J \in TopOn (PrmIdeal (R))$
69		toponuni	$⊢ J \in TopOn (PrmIdeal (R)) \to PrmIdeal (R) = ⋃ J$
70	68 69	syl	$⊢ R \in CRing \to PrmIdeal (R) = ⋃ J$
71	1 2 67 11	zartopn	$⊢ R \in CRing \to (J \in TopOn (PrmIdeal (R)) \land ran (k \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| k \subseteq j\}) = Clsd (J))$
72	71	simprd	$⊢ R \in CRing \to ran (k \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| k \subseteq j\}) = Clsd (J)$
73	70 72	ist0cld	$⊢ R \in CRing \to (J \in Kol2 \leftrightarrow (J \in Top \land \forall x \in PrmIdeal (R) \forall y \in PrmIdeal (R) (\forall d \in ran (k \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| k \subseteq j\}) (x \in d \leftrightarrow y \in d) \to x = y)))$
74	66 73	mpbird	$⊢ R \in CRing \to J \in Kol2$

Metamath Proof Explorer

Theorem zart0

Proof